The Coq mailing list

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

Ah, thank you for that. I will try. --Kevin

On Wed, Nov 29, 2017 at 4:26 PM, Tej Chajed <tchajed AT mit.edu> wrote:

Yes, there's also an unshelve in Ltac, so you can do unshelve refine (...). Sorry that wasn't clear.

​

On Wed, Nov 29, 2017 at 3:22 PM, Kevin Sullivan <sullivan.kevinj AT gmail.com> 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.