The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

> refine shelves goals which appear in the type of other goals, this is probably what is happening.

Thank you. That makes sense. And thanks all for unshelve refine and simpl refine. They solved the problem.

Kevin

On Wed, Nov 29, 2017 at 4:44 PM, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

>one at the end, for a proof that a certain cross-field constraint is satisfied.

refine shelves goals which appear in the type of other goals, this is probably what is happening.

You can use "unshelve refine" as others said, or "simple refine" https://coq.inria.fr/distrib/current/refman/tactics.html#hevea_tactic8
> simple refine term
> This tactic behaves like refine, but it does not shelve any subgoal. It does not perform any beta-reduction either.

Gaëtan Gilbert

On 29/11/2017 21:57, Kevin Sullivan 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 <http://io_compression_codecs.mk>  false "aCodecClassName" _)
     (io_file_buffer_size.mk <http://io_file_buffer_size.mk>            false 128%Z _)
     (io_map_index_interval.mk <http://io_map_index_interval.mk>      false 128%Z _)
     (io_fake_bool.mk <http://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.