The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

There is also the `unshelve` tactical. You can write `unshelve t`; which 
will execute `t` and turn all shelved goals produced by `t` into 
unshelved goals.

On 2017-11-29 22:22, Kevin Sullivan wrote:
> Thank you. Yes, that is what I've done so far (see the proof script below).
> The concern is that "This is a bit inconvenient because Unshelve is a
> vernacular command, not Ltac, so it cannot be embedded in a scripts and
> automated," per this old post:
> http://coq-club.inria.narkive.com/PQalG3f4/how-to-solve-trivial-evars-automatically-so-that-they-don-t-get-shelved.
> --Kevin
>
> On Wed, Nov 29, 2017 at 4:09 PM, Tej Chajed 
> <tchajed AT mit.edu>
>  wrote:
>
> > I'm not entirely sure how things get shelved, but you can use the unshelve
> > tactical, which runs a tactic and turns any generated shelved goals into
> > subgoals.
> >
> > On Wed, Nov 29, 2017 at 2:57 PM, Kevin Sullivan 
> > <sullivan.kevinj AT gmail.com
> > > wrote:
> >
> > > Dear Colleagues:
> > >
> > > I hope to get a question across well enough without getting into too much
> > > detail that someone will see the answer without much effort. In the
> > > fragment of code below, I'm trying to instantiate a "core_config" record
> > > with four fields, where each field in turn is built by calling a function
> > > "mk" from a field-specific module, taking a bool, a value of some type
> > > (string, Z, bool), and, finally, a proof of a proposition about that value.
> > > As usual I don't want to have to write out proof objects, so I use refine.
> > > There are five holes in the value that I'm refining, one after each of the
> > > first four fields (for proofs that the values of the individual fields
> > > satisfy certain constraints), and one at the end, for a proof that a
> > > certain cross-field constraint is satisfied.
> > >
> > > The problem is that although there are five holes, I get only three
> > > subgoals, and once I discharge them, I'm left with two additional goals on
> > > the shelf. I don't understand why that's happening. I'm not (explicitly)
> > > introducing any meta-variables with "e" tactics. It's surely important
> > > though to know that the goals that are being put on the shelf are those for
> > > fields whose values are constrained by that final constraint (the last
> > > hole).
> > >
> > > What do I need to know about the conditions under which goals are put on
> > > the shelf? My aim is to provide a proof script for instances of this record
> > > type that runs automatically. Am I out of luck? Happy to provide more
> > > details if any are needed.
> > >
> > > Sorry for yet another newbie/occasional-user question.
> > >
> > > Kevin
> > >
> > > ====
> > >
> > > Definition a_core_config': core_config.
> > > Proof.
> > > refine (
> > >    mk_core_config
> > >      (io_compression_codecs.mk  false "aCodecClassName" _)
> > >      (io_file_buffer_size.mk            false 128%Z _)
> > >      (io_map_index_interval.mk     false 128%Z _)
> > >      (io_fake_bool.mk                     false false _)
> > >      _
> > > ); try (exact I).
> > > intro; inversion H.
> > > Unshelve.
> > > unfold io_file_buffer_size_desc.rType; omega.
> > > unfold io_fake_bool_desc.rType; exact I.
> > > Qed.