Questions tagged [tactic]
A tactic is a command or instruction for constructing a formal proof by applying a common proof technique. For questions about high-level techniques for constructing proofs, use the tag (strategy).
4
questions with no upvoted or accepted answers
5
votes
0
answers
163
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 265
4
votes
0
answers
64
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
92
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
152
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 ...
- 224