Menu
In studying Coq proofs of other authors, I often encounter a tactic, lets say "inv eq Heq" or "intro_b". I want to understand such tactics.
How can I find if it is a Coq tactic or a Tactic Notation defined somewhere in my current project?
Second, is there a way to find its definition?
I used SearchAbout, Search, Locate and Print but could not find answers to the above questions.
704
Tactics specify how to transform the proof state of an incomplete proof to eventually generate a complete proof. Proofs can be developed in two basic ways: In forward reasoning, the proof begins by proving simple statements that are then combined to prove the theorem statement as the last step of the proof.
contradiction. If there is a hypothesis that is equivalent to False or two contradictory hypotheses in the context, you can use the contradiction tactic to prove any goal.
All that you need is to provide the witness first: Inductive A := X | Y . Definition P (a: A) : bool := match a with X => true | Y => false end. Theorem test : exists a: A, P a = true.
assert (HA := l1 H). assert (HB := l2 H). You can also do something like assert (H' := H). to explicitly copy H into H' , although you can usually resort to a more direct way for getting what you want. Save this answer.
You should be able to use
Print Ltac <tacticname>.
to print the code of a user-defined tactic (according to the documentation).
To find where it is defined... I guess you're going to need grep unfortunately, Locate does not work for tactics names it seems.
102
As mentioned before, Print Ltac ... prints the code of a user-defined tactic.
To locate a user-defined tactic (i.e. to know where its defined), use Locate Ltac .... It gives you the fully qualified name. Then use Locate Library to find the corresponding file.
44
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
