The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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.