The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq users,

I have another question on ltac matching. Please have a look at the samples
below. My main question is why ?a doesn't match with the 2nd hypothesis in the
second sample NOK1 as it does in the first sample OK1. I assumed that n
remains unbound in the first unification of ?a, so that ?a stiil matches with
the second hyopthesis with a specific value for n (m).

What does work is OK2, where I first match with another free variable ?c and
sort out things later, but when I have several hypothesis, the search effort
increases exponentially with the number of hypothesis.

Another thing I don't understand is why NOK2 doesn't work. The only thing I
changed is the form of the assert.

Thanks & best regards,

Michael


Parameter f g : nat -> Prop.

(* If the quantization applies to both hyopthesis, matching variable ?a twice
works *)

Lemma TestOK1: forall n, (f(n) -> g(n)) -> f(n) -> g(n).
Proof.
  intros n Ha Hb.
  match goal with
    H1 : ?a -> ?b, H2 : ?a |- _ => idtac H1 H2; assert( b ) by ( apply ( H1
H2 ) )
  end.

(* If the quantizations are separate, it doesn't work. Why is n not left
unbound in ?a ? *)

Lemma TestNOK1: ( forall n, (f(n) -> g(n)) ) -> forall m, f(m) -> g(m).
Proof.
  intros Ha m Hb.
  match goal with
    H1 : forall n, ?a -> ?b, H2 : ?a |- _ => idtac H1 H2
  end.

(* Matching by a different variable ?c and checking if it matches later works,
   but this can be inefficient, if several hypothesis need to be matched *)

Lemma TestOK2: ( forall n, (f(n) -> g(n)) ) -> forall m, f(m) -> g(m).
Proof.
  intros Ha m Hb.
  match goal with
    H1 : forall n, ?a -> ?b, H2 : ?c |- _ => idtac H1 H2; assert( AH:= H1 _
H2 )
  end.

(* Also why does assert( AH:= H1 _ H2 ) in OK2 work, but not an assert by: *)

Lemma TestNOK2: ( forall n, (f(n) -> g(n)) ) -> forall m, f(m) -> g(m).
Proof.
  intros Ha m Hb.
  match goal with
    H1 : forall n, ?a -> ?b, H2 : ?c |- _ => idtac H1 H2; assert( b ) by
( apply (H1 _ H2) )
  end.