coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Names of bound variables of existing lemma changes
Date: Wed, 4 May 2016 16:29:26 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:ntYfJxXNpwsGFxTBrC8UCwBYoJvV8LGtZVwlr6E/grcLSJyIuqrYZhaOt8tkgFKBZ4jH8fUM07OQ6PCxHzRaqsne+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVO18D22X1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDqBNMDUDn8Rf1FsPzry31nu9l2WyBItawSqo7D2fxp5x3QQPl3X9UfwUy93va35R9

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, 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