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
Filter by
Sorted by
Tagged with
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. ...
user avatar
  • 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 ...
user avatar
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: ...
user avatar
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.
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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: ...
user avatar
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....
user avatar