coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] specialize a subset of the parameters of a hypothesis

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] specialize a subset of the parameters of a hypothesis
Date: Wed, 23 Dec 2015 16:36:24 +0100
Authentication-results: mail2-smtp-roc.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-wm0-f42.google.com
Ironport-phdr: 9a23:s/lf8xPmkq79hRMyKSkl6mtUPXoX/o7sNwtQ0KIMzox0KPryrarrMEGX3/hxlliBBdydsKIazbKO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU15z//tvx0qOQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9ZLuh5dsPM59sNGTb6yP+FhFeQZX3waNDUe49Sjnh3eR0Pb7XwFF24SjxBgAg7f7Ri8UI2n4QXgse8o4CiXJ9f7BZszRC6+7qp2AEvQiSodLTN/22bKkNBxgb9zqxSoolpx2diHM8muKPNic/aFLpshTm1bU5MUDnQZDw==

Hi,

[specialize] is kind of useful but it needs a list of concrete terms
for a *prefix* of list of premisses of a hypothesis.

AFAIK you cannot give only, say, 3rd and 5th arguments. Sometime this
would be useful (because the hypothesis has independent premisses and
no particular order in the hyps is better than another).

Is there something to do so? I have a Ltac piece of code which does
roughly this in a naive way, but it is limited to one argument at a
time.

Idealy I would like to write:

generalize H with (x:=0) (3:=H2)(5:=H6).

Is this creatively hackable in ltac :) ?

Best regards,
Pierre

[Coq-Club] specialize a subset of the parameters of a hypothesis, Pierre Courtieu, 12/23/2015
- Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Abhishek Anand, 12/23/2015
  - Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Gregory Malecha, 12/23/2015