Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
8
questions with no upvoted or accepted answers
12
votes
0
answers
147
views
How do Coq's bidirectionality hints (`&`) affect type checking?
I have used Coq's bidirectionality hints (placement of & in a call to Arguments) to some effect, mostly by trial and error. ...
- 497
6
votes
0
answers
108
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 ...
- 1,721
5
votes
0
answers
86
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
67
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.
- 41
4
votes
0
answers
49
views
Tactic unification vs evarconv in Coq
I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a ...
- 497
3
votes
0
answers
81
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
55
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:
...
2
votes
0
answers
46
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....
- 21