4

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.

mlg556
  • 419
  • 3
  • 13

1 Answers1

2

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • 1
    Thank you! By mostly trial and error I have found that also " Ltac mt H H0 := let H1 := fresh "H" in match type of H with | ?A -> ?B => assert (~A) ; [intro H1 |] ; [contradiction H | ] end. " works. – mlg556 Oct 22 '18 at 20:07
  • 1
    No problem :) I started with a solution much like the one you mentioned, but I personally find that composition of `notQ` and `PtoQ` is a bit easier to follow. And an anonymous function makes it impossible to forget about the need of a fresh variable. – Anton Trunov Oct 22 '18 at 20:11
  • I have just found that this doesn't work in the less obvious case where the implication is "P -> notQ" and the hypothesis is "Q". Do you have any idea how to make it more general ? – mlg556 Oct 22 '18 at 21:08
  • I would not call that case completely obvious, because in case of `P -> ~Q` you would need to use `~ ~ Q`. Note that `Q` and `~ ~ Q` are not equivalent in the constructivist setting of Coq. But for this particular case `Ltac mt' PtoQ notQ notP := match type of PtoQ with | ?P -> _ => assert (~ P) as notP by tauto end.` should do the job – Anton Trunov Oct 22 '18 at 21:26
  • How would I "enforce" this equivalence ? The tactic returns `~ ~ Q` in the context which I cannot use with my other tactics. – mlg556 Oct 22 '18 at 21:30
  • (1) You need the `classical` axiom from [Coq.Logic.Classical_Prop](https://coq.inria.fr/library/Coq.Logic.Classical_Prop.html) or an equivalent one. (2) Which tactic do you mean? Can you give a concrete example with `~ ~ Q` as the result? – Anton Trunov Oct 22 '18 at 21:37
  • Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/182296/discussion-between-mlg556-and-anton-trunov). – mlg556 Oct 22 '18 at 21:47