Questions tagged [coq]
Coq is a formal proof management system, semi-interactive theorem prover and functional programming language. Coq is used for software verification, the formalization of programming languages, the formalization of mathematical theorems, teaching, and more. Due to the interactive nature of Coq, we recommend questions to link to executable examples at https://x80.org/collacoq/ if deemed appropriate.
2,953
questions
1
vote
0
answers
40
views
How to match implication without prior intros?
I am trying to write a tactic to check if my goal is an implication without having to introduce anything beforehand.
Furthermore I would like this tactic to be compatible with any amount of variables ...
- 21
2
votes
2
answers
64
views
Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?
I want to define a mutable dictionary that can return all of its keys in its domain. Keys don't have to be ordered. I searched in the coq library doc on the internet and didn't seem to find anything ...
- 79
1
vote
1
answer
72
views
Constructing proof terms inside a recursive function
Just starting with Coq, trying to write a list insertion function that will return either the new list, or if the provided index was illegal, a proof thereof using sumor. I'm fine with the recursion, ...
- 117
1
vote
1
answer
49
views
Coq notation defined inside a module expecting type without module prefix
I'm writing a compiler and its proof for a toy language, and I have files L1, L2, C, and P, where L1 and L2 contain the abstract syntax and operational semantics of languages l1 and l2, C containing ...
- 79
0
votes
2
answers
72
views
How can I prove that theorem in coq: (x | a) -> (x | b) -> x <= (gcd a b)?
I have this realization of greatest common divisor:
Fixpoint gcd_ (m n d : nat) : nat :=
match d with
| 0 => if (m =? 0) then n else m
| S k => if (m mod S k =? 0) && (n mod S k =? 0) ...
0
votes
1
answer
58
views
Beta-reduction after delta-reduction in unfold tactic
According to the coq manual, the unfold tactic performs delta reduction on a definition, followed by several other reductions, including beta-reduction.
It seems that sometimes, to trigger beta-...
- 97
-4
votes
1
answer
335
views
Can a dependently typed language be Turing complete? [closed]
It seems as though dependently typed languages are often not Turing complete. Why can we not allow every function to have general recursion (which would make the language Turing complete), instead of ...
0
votes
2
answers
40
views
Convert list to vector in coq
I'm pretty new to using coq and I'm a bit confused about vectors. I want to convert a list into a vector with the same content. I'm trying pattern matching, but it keeps throwing errors about the ...
- 113
0
votes
1
answer
55
views
Defining mutually recursive types in Coq?
Suppose I have types A,B,C,D,E,F. One of the constructors of A takes an argument with type F; a constructor of B requires A, a constructor of D requires arguments of types C and A, E requires D and F ...
- 79
1
vote
1
answer
39
views
How to mix sections with hints in Coq?
I am writing something heavily involving typeclasses and I would like to utilize hints to ease proving local lemmas as well as exported theorems.
For instance, consider
Class MyClass (A : Type) :=
...
- 6,859
0
votes
3
answers
87
views
Lemma about a graph in Coq
I need to prove a Lemma in Coq, about a connected graph with certain properties:
the vertices of the graph are of type V:Type, and there is a function f: V -> nat which associates a natural number ...
- 97
0
votes
1
answer
117
views
Error: Cannot find a physical path bound to logical path Strands. in coq
I have coq file and was working on it for days but now the file giving me following error:
Error: Cannot find a physical path bound to logical path Strands.
also the required packages are as under:
...
- 11
-1
votes
2
answers
92
views
How to prove that forall n m, n <= m -> m <= n -> n = m
Theorem le_trans: forall n m o, n <= m -> m <= o -> n <= o.
Proof.
intros n m o Lnm Lmo.
generalize dependent Lnm.
generalize dependent n.
induction Lmo.
- intros. apply Lnm.
- ...
0
votes
1
answer
72
views
Is there an intuitionistic proof of `(A -> B \/ C) -> (A -> B) \/ (A -> C)`?
Following is a useful lemma in classical propositional logic.
(A -> B \/ C) <-> (A -> B) \/ (A -> C).
The backward direction is easily proved. But I could not find an intuitionistic ...
0
votes
2
answers
97
views
Eliminating impossible branches in Coq dependent pattern matching
I'm having troubles with understanding pattern matching on dependent types. Let's say we have following code:
Variant Op := op1 | op2.
Variant Res : Op -> Set :=
| r1 : Res op1
| r2 : Res op2
| rb ...
