Skip to main content

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
Filter by
Sorted by
Tagged with
5 votes
0 answers

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
Tempestas Ludi's user avatar
4 votes
0 answers

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 ...
Vladimir Prigodsky's user avatar
3 votes
0 answers

Where is the discriminate tactic defined in Coq?

One can read the Coq documentation about discriminate tactic here. Were is this tactic actually defined?
Jacob woolcutt's user avatar
2 votes
1 answer

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 ...
8bc3 457f's user avatar
  • 224