coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] making a proof done with assert transparent

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] making a proof done with assert transparent
Date: Mon, 12 Oct 2015 14:54:18 +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-wi0-f179.google.com
Ironport-phdr: 9a23:TsEY5RNwbMRqM5wEXFEl6mtUPXoX/o7sNwtQ0KIMzox0KPv+rarrMEGX3/hxlliBBdydsKIYzbqM+P29EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35jxh7r5psCbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzoShLHzX8BWC1CmR1RRgPB8RvSX5HrsyK8uPAriweAOsijdbE5Qy6vp4xsVQX0iSoaf2oB8WzNkME2p6VGug6gqgFXyIjdZcebLqwtLevmYdoGSD8ZDY5qXCtbD9b5NtNXAg==

Actually Unshelve is documented in v8.5 (which is not on coq web
site). It is a command, not a tactic.

For the record "swap" can be used to change the ordering of goals:

eval(foo : bar).
Unshelve.
all:swap 1 2.

But I guess other solutions with only tactics are better.

P.

2015-10-12 14:10 GMT+02:00 Daniel de Rauglaudre
<daniel.de_rauglaudre AT inria.fr>:
> Ah, Unshelve, ok. Seems not to be in the documentation. I see it works
> but if I want to prove it immediately, I must use "Focus" after.
>
> Otherwise, the solution with refine given here seems to work also.
> But both solutions are not clear for the reader. An "assert" with
> option "transparent" would be good :-)
>
> On Mon, Oct 12, 2015 at 01:49:58PM +0200, Pierre Courtieu wrote:
>> Hi Daniel, I think "Unshelve." is what your are looking for.
>
> --
> Daniel de Rauglaudre
> http://pauillac.inria.fr/~ddr/

[Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
  - Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015
    - Re: [Coq-Club] making a proof done with assert transparent, Pierre Courtieu, 10/12/2015
      - RE: [Coq-Club] making a proof done with assert transparent, Soegtrop, Michael, 10/12/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Jason Gross, 10/12/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
        
        Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/13/2015
        Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/13/2015
- Re: [Coq-Club] making a proof done with assert transparent, Ilmārs Cīrulis, 10/12/2015
- Re: [Coq-Club] making a proof done with assert transparent, Pierre-Marie Pédrot, 10/12/2015
  - Re: [Coq-Club] making a proof done with assert transparent, Daniel de Rauglaudre, 10/12/2015