Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
13
questions with no upvoted or accepted answers
6
votes
0
answers
69
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
113
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,422
5
votes
0
answers
49
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 ...
- 161
5
votes
0
answers
119
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 ...
- 161
5
votes
0
answers
82
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
97
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
4
votes
0
answers
69
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:
...
3
votes
0
answers
20
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 ...
- 31
3
votes
0
answers
61
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
98
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
54
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
1
vote
0
answers
21
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:
<...
- 161
0
votes
0
answers
47
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