Coq match on Hypothesis passed to Ltac tactic

Question

I'm new to Coq, currently on the IndProp chapter of Software Foundations. I'm curious about learning to write my own simple tactics to automate certain kinds of reasoning, but unfortunately the official documentation is a bit impenetrable to me as a beginner.

I'd like to write a tactic that applies in the following scenario:

The current goal is False
There is a hypothesis of the form P \/ False

Based on the following lemma, we should be able to replace the current goal with ~P in this scenario:

Lemma orfalse_lemma : forall P : Prop,
  P \/ False -> ~P -> False.
Proof.
  intros P [H|H] HP.
  - apply HP. apply H.
  - apply H.
Qed.

We can use the lemma manually with the desired effect:

Example ex_orfalse_1 :
  (1 <> 2) \/ False -> (False).
Proof.
  intros H. apply (orfalse_lemma (1 <> 2)). apply H.
  (* goal:  ~ (1 <> 2) *)
Admitted.

I want to automate this, so I wrote a simple tactic to apply the lemma when the goal and context match this scenario:

Ltac orfalse :=
  match goal with
    | [H : ?P \/ False |- False ] => apply (orfalse_lemma P) ; [> apply H | ]
    | _                           => fail "expected goal to be False"
  end.

It works as expected. However, when there are multiple hypotheses matching the pattern, we don't have the option to choose between them:

Example ex_orfalse_1 :
  (1 <> 2) \/ False -> (False).
Proof.
  intros H. orfalse.
  (* goal:  ~ (1 <> 2) *)
Admitted.

Example ex_orfalse_2 :
  (false <> true) \/ False -> (1 <> 2) \/ False -> (False).
Proof.
  intros H1 H2. orfalse.
  (* goal:  ~ (1 <> 2) *)
  (* what if we want the goal to be ~ (false <> true) instead? *)
Admitted.

I assumed fixing this problem would be as simple as just passing the desired hypothesis to the orfalse tactic as an argument:

Ltac orfalse H :=
  match goal with
    | [|- False ] =>  match H with
                      | ?P \/ False => apply (orfalse_lemma ?P) ; [> apply H | ]
                      | _  => fail "expected disjunction with false"
                      end
    | _ => fail "expected goal to be False"
  end.

However, using it in a proof fails:

Example ex_orfalse_2 :
  (false <> true) \/ False -> (1 <> 2) \/ False -> (False).
Proof.
  intros H1 H2. orfalse H1.
  (* Tactic failure: expected goal to be False. *)
Admitted.

If I replace the first case of the nested match with just ?P and return idtac ?P, it just prints the name of the hypothesis I pass in (e.g. H1 or H2), so my guess is that the match happens on the identifier itself and not on the hypothesis.

So, my question is: If I pass the name of a hypothesis to a tactic, how do I correctly match on the structure of that hypothesis? Thanks!

M Soegtrop M Soegtrop · Accepted Answer · 2021-07-14T13:10:04

welcome to Coq!

There are two minor issues with your tactic. First you must not match the value of H - which either would be a proof term or the value of H is simply H and cannot be further evaluated - you must match the type of H. Then when using match variables, no ? is required. This works:

Lemma orfalse_lemma : forall P : Prop,
  P \/ False -> ~P -> False.
Proof.
  intros P [H|H] HP.
  - apply HP. apply H.
  - apply H.
Qed.

Ltac orfalse H :=
  match goal with
    | [ |- False ] => match type of H with
                      | ?P \/ False => apply (orfalse_lemma P) ; [> apply H | ]
                      | _  => fail "expected disjunction with false"
                      end
    | _ => fail "expected goal to be False"
  end.

Example ex_orfalse_2 :
  (false <> true) \/ False -> (1 <> 2) \/ False -> (False).
Proof.
  intros H1 H2. orfalse H1.
Admitted.

Coq match on Hypothesis passed to Ltac tactic

1 Answers