Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism)

Question

This question is about a project that I am doing, namely, to code Principia Mathematica in Coq. Principia has derived rules of inference, one of which is Syll:

∀ P Q R : Prop, P→Q, Q→R : P→R

I am trying to create an Ltac script that codifies the Syll inference form. The following MP tactic from (Chlipala 2019) works perfectly:

Ltac MP H1 H2 :=
  match goal with 
    | [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)
end.

Here I take it that the tactic on the right of "=>" specializes the application of H1 to H2. Now the correlated Syll tactic does not work:

Ltac Syll H1 H2 :=
  match goal with 
     | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- _ ] =>
        specialize Syll2_06 with ?P ?Q ?R;
        intros Syll2_06;
        apply Syll2_06;
        apply H1;
        apply H2
end.

The error that I get in applying it (in the example below) is:

No matching clauses for match.

I am not sure why this is the resulting error. Classical logic was imported, and I proved as a theorem Syll2_06, i.e., (P→Q)→((Q→R)→(P→R)). In fact, what is basically the Syll Ltac was applied in the proof of theorem Trans2_16 (see below). So I am unsure why turning the code into an Ltac script is not working.

Perhaps I am misunderstanding what Ltac match is doing, and what the tactic to the right of "=>" should be. But based on looking at the Coq manual, it may be that the left side of the tactic is the problem, perhaps because H1 isn't applicable to H2.

Further suggestions, particularly one that explains Ltac and/or my error in how I am thinking about it, would be very much appreciated.

Theorem Syll2_06 : ∀ P Q R : Prop,
  (P → Q) → ((Q → R) → (P → R)).
    
Ltac Syll H1 H2 :=
  match goal with 
     | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- _ ] =>
        specialize Syll2_06 with ?P ?Q ?R;
        intros Syll2_06;
        apply Syll2_06;
        apply H1;
        apply H2
end. 
    
Ltac MP H1 H2 :=
  match goal with 
    | [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)
end.

Theorem Trans2_16 : forall P Q : Prop,
  (P → Q) → (~Q → ~P).
Proof. intros P Q.
  specialize n2_12 with Q. intros n2_12a.
  specialize Syll2_05 with P Q (~~Q). intros Syll2_05a.
  specialize n2_03 with P (~Q). intros n2_03a.
  MP n2_12a Syll2_05a.
  specialize Syll2_06 with (P→Q)  (P→~~Q) (~Q→~P). intros Syll2_06a.
  apply Syll2_06a.
  apply Syll2_05a.
  apply n2_03a.
Qed.

Theorem Trans2_17 : forall P Q : Prop,
  (~Q -> ~P) -> (P -> Q).
Proof. intros P Q.
  specialize n2_03 with (~Q) P. intros n2_03a.
  specialize n2_14 with Q. intros n2_14a.
  specialize Syll2_05 with P (~~Q) Q. intros Syll2_05a.
  MP n2_14a Syll2_05a.
  Syll 2_03a Syll2_05a.
Qed.

Replace match with lazymatch. This commits to the first (only) matching branch without backtracking. The error is probably in what you wrote to the right of the => (just from a glance it looks far too complicated), but the message is being swallowed because the match tries to backtrack out of that branch into another and the failure to find that "another" is what is reported. By committing to the branch you get the "correct" error message. — HTNW
Why are you using specialize? (Specialize modifies the terms in you context (H1, H2...) ) Don't you want the tactic go solve the goal, i.e by applying a term? And you can also let Coq find the two assumptions that you need instead of having to specify them, which can be both good and bad. It saves you from having to invent arbitrary names for everything, but arguably makes it less easy for humans to follow the proof by reading the tactics. — larsr

larsr larsr · Accepted Answer · 2020-09-14T08:03:26

I am not certain how you want the tactic to work. If we start like this:

Variables P Q R S : Prop.

Goal (P -> Q) -> (S -> Q) -> (Q -> R) -> P -> R.
  intros A B C.

then the goal is:

  A : P -> Q
  B : S -> Q
  C : Q -> R
  ============================
  P -> R

What do you want Syll A C to do?

Should it solve the goal? Should it modify C to be R? Should it add a new term (i.e. named D) of type P -> R to the context?

For example, if you want a tactic to solve the goal, you can use apply:

Ltac Syll H1 H2 :=
  match goal with 
  | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- ?P -> ?R ] =>
    intros p; apply (H2 (H1 p))
  end.

If you want to add a new term to the context, you can construct it i.e. with assert:

Ltac Syll H1 H2 N:=
  match goal with 
  | [ H1 : ?P -> ?Q, H2 : ?Q -> ?R |- ?P -> ?R ] =>
    assert (N: P -> R) by (intros p; apply (H2 (H1 p)))
  end.

Also note that if Syll doesn't take H1 and H2 as arguments, Coq will by itself find which assumptions to use to construct the proof.

Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism)

1 Answers