Search code examples
coqcoq-tacticltac

Conditional Proof Tactic in Coq

I believe the title is pretty self explanatory : https://en.wikipedia.org/wiki/Conditional_proof

I would like to have a tactic where I assume a proposition and proceed to find another one, if succeeded, then I have found that the first proposition implies the second one and this is put as an hypothesis in the context.

So for example Ltac cp P Q creates a subgoal Qand puts Pin the context. If I can indeed reach the subgoal Q, then the subgoal is discharged and P->Q is added to the context. How can I achieve this ?

Edit: It is clear that while proving assert (P->Q). intro. does the job, but I cannot combine them into a Ltac tactic, it gives an error of No focused proof (No proof-editing in progress).

Solution

  • To define new tactics, you need to compose them with ;.

    Ltac cp P Q := assert (P -> Q); [ intro | ].
  (* Use intro in the first subgoal of assert *)