Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
19
questions with no upvoted or accepted answers
7
votes
0
answers
137
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 421
6
votes
0
answers
82
views
In VSCoq, how to issue an arbitrary Gallina query via the prompt?
I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way ...
6
votes
0
answers
115
views
How to write heavily indexed proofs?
I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow.
In my old approach terms were not indexed ...
- 2,628
5
votes
0
answers
56
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
- 169
5
votes
0
answers
136
views
How does one systematically traverse OCaml representations of Coq ASTs terms?
I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).
My main challenge is to figure out how to do this systematically because I ...
- 169
5
votes
0
answers
122
views
Unfolding expressions in Coq by one layer
Are there any ways to unfold an expression in Coq by a single layer?
I have only come up with this obvious solution:
...
5
votes
0
answers
85
views
Display style proofs using Coq
How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq?
PS: I'm rookie used coq.
- 51
5
votes
0
answers
111
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 225
3
votes
0
answers
73
views
Coq Typeclass on Functions Gets Confused by Equality
I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue:
...
- 171
3
votes
0
answers
26
views
.CoqMakefile.d required by CoqMakefile but not generated
I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2.
When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
- 96
3
votes
0
answers
68
views
Where is the discriminate tactic defined in Coq?
One can read the Coq documentation about discriminate tactic here.
Were is this tactic actually defined?
3
votes
0
answers
103
views
Recursive notations with forall quantifier
How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq?
A similar notation (but without quantifiers) appears here
...
3
votes
0
answers
60
views
SSReflect tuple constructor: why not use phantom?
I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
- 31
2
votes
0
answers
113
views
Cannot open pixbuf loader module file in Windows
I installed Coq from the 8.15 64-bit installation file in Windows. I ran coqide and got the error message:
...
- 21
1
vote
0
answers
62
views
How to reason about equality between different datatypes?
I am working on a verification project where the specification uses the following inductive datatype to represent bitvectors (MIT's bbv)
...
- 11
1
vote
0
answers
22
views
Why does TacArg accepts a value of CAst.t type when it should only accept values of types?
See the argument for TacArg:
| TacArg of ('t, 'dtrm, 'p, 'c, 'r, 'n, 'tacexpr, 'l) gen_tactic_arg
but the reply has a type CAst.t as an argument for TacArg:
<...
- 169
0
votes
1
answer
71
views
an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert
I apologize if this is not the right site to ask this, as the question is not about a proof assistant per se, but about a particular formalization.
In the semantics of the RTL intermediate language in ...
- 101
0
votes
0
answers
54
views
If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?
From $\mathbb{Q}$, the set of all rational numbers, I make some new structure $I$, and also make strict order and (equivalence) equality on $I$.
I want to use rewrite tactic for my defined relations (...
- 285
-2
votes
1
answer
131
views
How to write a summation in Coq
I have just started getting acquainted with Coq and I would like to write this sum on it:
$\sum_{p=1}^{n} \frac{\mathrm{d}^p}{\mathrm{d}x^p} f(x)$
This is what I have tried:
...
- 21