coq Questions
2
Solved
I'm building a recursive function that does a match on a list l. In the cons branch I need to use the information that l = cons a l' in order to prove that the recursive function terminates. Howeve...
3
I am working on the proof of the following theorem Sn_le_Sm__n_le_m in IndProp.v of Software Foundations (Vol 1: Logical Foundations).
Theorem Sn_le_Sm__n_le_m : ∀n m,
S n ≤ S m → n ≤ m.
Proof.
...
Thill asked 24/5, 2019 at 12:12
3
Solved
During a proof, I encountered an hypothesis H. I have lemmas: H -> A and H -> B.
How can I duplicate H in order to deduce two hypotheses A and B ?
edited:
More precisely, I have:
lemma l1...
Fissionable asked 7/12, 2014 at 15:34
0
I have a very long list of coq projects I want to automatically install with opam pin/install. I'd like to install them with opam because I am using this python tool (PyCoq) that uses opam pin/inst...
2
How does one switch to a specific version of Coq -- especially when managing Coq versions with Opam?
I am currently using the standard one I installed the standard way (probably through the website). But I want to use tcoq. I believe I have installed it correctly because I have a bin file and all ...
1
I understand what I believe is the essence of the official utilties doc https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project:
one creates a _CoqProject with arguments ...
Douma asked 11/6, 2022 at 17:8
2
I got a new machine (mac book m1, not sure if it matters) and I noticed I didn't have Coq:
(base) brandomiranda~ ❯ coqc -v
zsh: command not found: coqc
So I went to the instructions to download c...
Summit asked 14/2, 2022 at 20:20
2
Solved
When refineing a program, I tried to end proof by inversion on a False hypothesis when the goal was a Type. Here is a reduced version of the proof I tried to do.
Lemma strange1: forall T:Type, 0&g...
1
Solved
I have imported a Coq module which defines a coercion, but it does not fit my needs. Is there any way to remove or (locally) override it?
To be specific, say the module I imported defines a coerci...
4
Solved
Basically, I would like to prove that following result:
Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
forall n, P n.
that is the recurrence scheme...
Groan asked 5/10, 2013 at 16:41
2
Solved
In https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1 one can read:
Coq's standard library takes a very different approach to the real numbers: An axiomatic approach.
and one can find the following...
Miseno asked 22/10, 2021 at 22:39
1
Solved
I have the following two definitions that result in two different error messages.
The first definition is declined because of strict positivity and the second one because of a universe inconsistenc...
Whopper asked 15/5, 2019 at 7:15
2
I find my self (sort of) duplicating code because I want to the same tactics in the goal and in a hypothesis when they match. For example:
match goal with
| H : PATTERN |- _ => simpl in H; rewri...
Wampler asked 23/9, 2021 at 10:58
1
Solved
I've been working on a formalization for a process calculus in Coq (repository here), and constantly find myself trying to apply a function which fails because of equivalent, but syntactically diff...
Auriferous asked 17/9, 2021 at 20:20
1
Solved
I am trying to complete the series of exercises le_exercises from Logical Foundations' chapter on inductive propositions.
This series is mostly based on the inductive relation le, defined thusly:
I...
Edouard asked 5/9, 2021 at 14:27
4
Solved
[I am not sure this is appropriate for stack overflow, but there are many other Coq questions here so perhaps someone can help.]
I am working through the following from http://www.cis.upenn.edu/~b...
2
Solved
Is it possible to switch the current goal or subgoal to prove in Coq?
For example, I have a goal like this (from an eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s...
Anosmia asked 22/12, 2015 at 17:10
4
Solved
So this is one of the exercise I have been working from Software Foundations in which I have to prove that multipication is commutative. And this is my solution:
Theorem brack_help : forall n m p:...
Filings asked 13/1, 2016 at 4:39
1
Solved
Suppose I write the following lemma and proof in Coq:
Lemma foo : forall A, A -> A.
Proof.
- simpl.
- auto.
Qed.
The simpl here doesn't do anything, and this is a bad use of bullet points (-)...
Catechism asked 16/7, 2021 at 12:14
1
I've been trying to understand what Set is after encountering it in Adam Chlipala's book in addition to this great discussion in SO. His first example definition binary ops using Set:
Inductive bin...
Beluga asked 20/6, 2021 at 14:45
3
I'm new to Coq, working on set-theoretic proof writing.
I realized that parentheses are omitted, and it makes difficult for me to read the formula. For example,
1 subgoal
A, B : {set T}
H : B \su...
2
Solved
I know that one can extract Coq programs into Haskell and OCaml programs. Is there a way to do this with C?
I am imagining a library that models the C language. Maybe such a library would contain...
Sulfapyridine asked 23/10, 2017 at 21:3
3
Solved
One finds that Setoids are widely used in languages such as Agda, Coq, ... Indeed languages such as Lean have argued that they could help avoid "Setoid Hell". What is the reason for using...
1
Solved
Consider the situation described by the code below, wherein I have a "piecewise" function h behaving differently (like f, or like g) depending on some (decidable) property condition of it...
Landwaiter asked 22/7, 2020 at 4:57
2
Solved
When proving in Coq, it's nice to be able to prove one little piece at a time, and have Coq help keep track of the obligations.
Theorem ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B...
Luthuli asked 12/3, 2020 at 21:29
1 Next >
© 2022 - 2024 — McMap. All rights reserved.