coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Names of bound variables of existing lemma changes

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Names of bound variables of existing lemma changes
Date: Wed, 4 May 2016 18:38:01 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f50.google.com
Ironport-phdr: 9a23:lXGIwxKh+JtqWdsUwdmcpTZWNBhigK39O0sv0rFitYgULfvxwZ3uMQTl6Ol3ixeRBMOAu6MC07Cd4vGocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC3oLvjavjqtX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjOTL0uQznqxKB2UgPphTpPYyY4/XvNh4p7i79BvBOsujRwxofVZMeeM/8oLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=

I see.

+1!

2016-05-04 16:29 GMT+02:00 Ralf Jung
<jung AT mpi-sws.org>:
> Hi,
>
>> It is possible actually:
>>
>> Lemma foo n (P Q : Prop) : n = O -> Q -> P -> Q.
>> Proof.
>> intros H H0 H1.
>> auto.
>> Qed.
>>
>> Print Implicit foo. (* no implicits*)
>>
>>
>> Lemma trying : False -> False.
>> Proof.
>> apply foo with (P:=False) (n:=0) .
>> Undo.
>> Fail apply foo with (P:=False). (* fails because n should be given
>> if Q is given *)
>> eapply foo with (P:=False). (* OK *)
>>
>> Qed.
>
> It is possible for apply, but this is an Ltac thing, not a Gallina term
> -- so I only can use this with those tactics that gave been specifically
> prepared to do so.
>
> Kind regards,
> Ralf

[Coq-Club] Names of bound variables of existing lemma changes, Ralf Jung, 05/04/2016
- Re: [Coq-Club] Names of bound variables of existing lemma changes, Beta Ziliani, 05/04/2016
- Re: [Coq-Club] Names of bound variables of existing lemma changes, Hugo Herbelin, 05/04/2016
  - Re: [Coq-Club] Names of bound variables of existing lemma changes, Ralf Jung, 05/06/2016
    - Re: [Coq-Club] Names of bound variables of existing lemma changes, Hugo Herbelin, 05/06/2016
- Re: [Coq-Club] Names of bound variables of existing lemma changes, Pierre Courtieu, 05/04/2016
  - Re: [Coq-Club] Names of bound variables of existing lemma changes, Ralf Jung, 05/04/2016
    - Re: [Coq-Club] Names of bound variables of existing lemma changes, Pierre Courtieu, 05/04/2016
- <Possible follow-up(s)>
- Re: [Coq-Club] Names of bound variables of existing lemma changes, Beta Ziliani, 05/04/2016