The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi,


On Mon, Jul 21, 2014 at 10:26 AM,  
<michael.soegtrop AT intel.com>
 wrote:
> 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.
>

Why would it work?  You're unifying ?a with [f n], for n local to H1,
and then wanting to unify it with [f m].  What you want is:

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

Unifying [?a n] with [f n] results in defining ?a := f, therefore
successfully unifying [?a m] with [f m].

Hope it helps,
Beta



> (* 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.