All Questions
4
questions with no upvoted or accepted answers
5
votes
0
answers
164
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
4
votes
0
answers
65
views
Using CoqHammer from Ltac2
As it seems most likely to me, due to the special way arguments are evaluated in CoqHammer tactics (I tried to read the source code in OCaml but unfortunately I didn't understand much of it), it is ...
3
votes
0
answers
93
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?
2
votes
1
answer
154
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...