Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "named" goals with refine

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "named" goals with refine


Chronological Thread 
  • From: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • To: AUGER Cédric <sedrikov AT gmail.com>
  • Cc: Dmitry Grebeniuk <gdsfh1 AT gmail.com>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] "named" goals with refine
  • Date: Wed, 16 Jan 2013 15:20:29 +0100

Guillaume, Cédric, that looks like a very useful trick that I hadn't
seen employed before. Like the (Case "foo") macros of Software
Foundations, those hacks merit to become more well-known among Coq
users.

Would any of you (or both together) care to write a self-contained
document presenting it, that we could point to beginners having the
same kind of questions? Just posting it to the list would be fine, or
if you have a blog/website/whatever it's also fine.

On Wed, Jan 16, 2013 at 1:29 PM, AUGER Cédric
<sedrikov AT gmail.com>
wrote:
> Le Wed, 16 Jan 2013 11:06:06 +0200,
> Dmitry Grebeniuk
> <gdsfh1 AT gmail.com>
> a écrit :
>
>
>> So I want something like this pseudocode:
>>
>> Goal myrec.
>> refine ( {| n := 7 ; n_lt_10 := ?goal_nat? ; b := true ; b_tf :=
>> ?goal_bool? |} ).
>> for ?goal_nat? : omega.
>> for ?goal_bool? : apply bool_tf.
>> Qed.
>>
>> (of course I understand that solution may be not so pretty as
>> the pseudocode, but aesthetics is not a my target.)
>
> I think it would be a nice addition to extend the refine tactic with
> some syntax to call tactics like this:
>
> refine_with_tactics ( {| n := 7 ; n_lt_10 := <#omega#> ; b := true ;
> b_tf := <#apply bool_tf#> |}.
>
> So that the code between <# and #> could be solved by the provided
> proof script. My suggestion or Guillaume's one work, but having a
> plugin for that, so that it is internally managed would be better.
>
> I think I will fill a feature request.



Archive powered by MHonArc 2.6.18.

Top of Page