Dear Beta,
> I'm not sure I understand your point, since [apply] and [match] use the same unification algorithm.
my point is that when I use apply, I don’t have to care about universal quantification. Coq automatically finds proper values for quantified variables. An Ltac
match does not do this, the quantification has to match exactly there. But you are right, too much automation can be a pain, at least if you cannot switch it off. It was easy to solve my problem with your hints.
Best regards,
Michael
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr]
On Behalf Of Beta Ziliani
Sent: Tuesday, July 22, 2014 9:03 AM
To: Coq Club
Subject: RE: [Coq-Club] Ltac match on quantified hypothesis
On Jul 21, 2014 12:38 PM, "Soegtrop, Michael" <michael.soegtrop AT intel.com> wrote:
Dear Beta,
yes, this does help!
I was assuming that what you did explicitly would be done implicitly by the unifier, that is: keep the forall n outside of the unification and add it as argument to the results. I think it is not that unreasonable to expect this, since Coq is also quite smart
about handling quantification in unification with apply. So why shouldn't it be smart with match as well?
I'm not sure I understand your point, since [apply] and [match] use the same unification algorithm.
In any case, with Matthieu Sozeau we argued at the Coq workshop that, actually, it's best for the unification algorithm to *not* be that smart. If the algorithm tries hard to interpret what's in the mind of the proof developer, it becomes slow and unpredictable.
The first thing I tried was actually like below, expecting that H1 would be set to (Ha m).
Lemma TestNOK1: ( forall n, (f(n) -> g(n)) ) -> forall m, f(m) -> g(m).
Proof.
intros Ha m Hb.
match goal with
H1 :?a -> ?b, H2 : ?a |- _ => idtac H1 H2
end.
Thanks & best regards,
Michael
-----Original Message-----
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Beta Ziliani
Sent: Monday, July 21, 2014 10:38 AM
To: Coq Club
Subject: Re: [Coq-Club] Ltac match on quantified hypothesis
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.
|
