Modus Ponens and Modus Tollens in Coq

Question

I would like to have Ltac tactics for these simple inference rules.

In Modus Ponens, if I have H:P->Qand H1:P, Ltac mp H H1 will add Qto the context as H2 : Q.

In Modus Tollens, if I have H:P->Qand H1:~Q, then Ltac mt H H1 will add H2:~Pto the context.

I have written one for the modus ponens, but it does not work in the complicated cases where the precedent is also an implication.

Ltac mp H0 H1 := let H := fresh "H" in apply H0 in H1 as H.

Edit : I have found the answer to Modus Ponens in another seemingly unrelated question (Rewrite hypothesis in Coq, keeping implication), where a "dumbed-down" version of applyis made with generalize.

Ltac mp H H0 := let H1 := fresh "H" in generalize (H H0); intros H1.

I would still appreciate an answer for Modus Tollens, though.

Anton Trunov Anton Trunov · Accepted Answer · 2018-10-22T19:25:31

Here is one solution:

Ltac mt PtoQ notQ notP :=
  match type of PtoQ with
  | ?P -> _ => pose proof ((fun p => notQ (PtoQ p)) : ~ P) as notP
  end.

This tactic asks the user for the two input hypothesis and for an explicit name of the output hypothesis. I use type of PtoQ construction to extract the type P from the input implication and then provide an explicit term (fun p => notQ (PtoQ p) of type P -> False, which is definitionally equal to ~ P. The explicit type ascription : ~ P is used to make the context look prettier, without it Coq would show the output hypothesis's type as P -> False.

Incidentally, I would use something like this to implement the modus ponens tactic:

Ltac mp PtoQ P Q := 
  pose proof (PtoQ P) as Q.

Here, again PtoQ and P parameters are the names of the input hypotheses and Q is the name to be added to the context.

Modus Ponens and Modus Tollens in Coq

1 Answers