The Coq mailing list

[Anton Trunov <anton.a.trunov AT gmail.com>]

Hi Christian,

Actually, [Program] provides “*_eq” lemmas, but apparently you have to use 
[match … with]:

Program Fixpoint bar (G : graph) {measure (size G)} : nat := 
  match (property G) with true => bar (dec1 G) | false => 4 end.
Next Obligation.
  now apply dec1_lt.
Defined.

From the manual (§24.1.1) "the if construct is not treated specially by 
PROGRAM so boolean tests in the code are not automatically reflected in the 
obligations”.

—
best regards,
Anton Trunov

> On 28 Jun 2017, at 19:23, Christian Doczkal 
> <christian.doczkal AT ens-lyon.fr>
>  wrote:
> 
> Hi,
> 
> Thanks for the replies, I had tried something along these lines as well,
> albeit not too hard. Your solution (and that of Gaetan) however require
> quite a bit of dependent programming.
> 
> Further, even on this simple example the definition generated this way
> does not look like I want to prove anything about it and, as far as I
> can tell, Program does not provide anything corresponding to Function's
> "*_eq" lemmas. Fully specifying he behavior using sigma-tyoes is also
> not realistic in my case.
> 
> I guess that means I'll use bounded recursion.
> 
> Cheers,
> Christian
> 
> On 28/06/17 14:09, Frédéric Besson wrote:
>> Hi Christian,
>> 
>> I am far from having a definite opinion.
>> Yet, you can guide Program Fixpoint to get stronger proof obligations.
>> For instance, here is what you could do:
>> 
>> 
>> Require Import Program.Tactics.
>> Require Import Program.Wf.
>> Require Import List.
>> 
>> Variable graph : Type.
>> Variable size : graph -> nat.
>> Variable propertyP : graph -> bool.
>> Variable decompose : forall (g:graph), 
>>  list {g':graph| size g' < size g}.
>> 
>> Program Fixpoint foo' (G : graph) {measure (size G)} : nat :=
>>  if propertyP G
>>  then fold_right (fun H m => Nat.max H m) 0 (map (fun gp => foo'
>> (proj1_sig gp)) (decompose G))
>>  else 4.
>> Next Obligation.
>>  apply measure_wf.
>>  apply PeanoNat.Nat.lt_wf_0.
>> Defined.
>> 
>> 
>> PS: I also often lean towards bounded recursion.
>> --
>> Frédéric
>> 
>> 
>> 
>> On Tue, 2017-06-27 at 14:51 +0200, Christian Doczkal wrote:
>>> Hello,
>>> 
>>> I need to define a rather complicated non-structurally recursive
>>> function and I would like to gather some input as to which way i
>>> should
>>> proceed.
>>> 
>>> I know of the following facilities/techniques to define non-
>>> structurally
>>> recursive functions:
>>> 
>>> - Program Fixpoint
>>> - The Function command
>>> - Using Coq.Init.Wf.Fix
>>> - Using an extra Argument of type nat bounding the recursion depth
>>> 
>>> I will need variable-width recursion (i.e., mapping the function over
>>> lists of smaller arguments). This is not supported by Function.
>>> Indeed
>>> the following fails as expected (self contained file attached):
>>> 
>>> Fail Function foo (G : graph) {measure size G} : nat :=
>>>  if property G
>>>  then fold_right (fun H m => Nat.max (foo H) m) 0 (decompose G)
>>>  else 4.
>>> 
>>> Program fares little better:
>>> 
>>> Program Fixpoint foo (G : graph) {measure (size G)} : nat :=
>>>  if propertyP G
>>>  then fold_right (fun H m => Nat.max (foo H) m) 0 (decompose G)
>>>  else 4.
>>> 
>>> Here I'm asked to prove "size H < size G" without knowing that H is
>>> from
>>> "decompose G". Trying to map before folding, I don't even get
>>> obligations:
>>> 
>>> Fail Program Fixpoint foo' (G : graph) {measure (size G)} : nat :=
>>>  if propertyP G
>>>  then fold_right (fun H m => Nat.max H m) 0 (map foo' (decompose G))
>>>  else 4.
>>> 
>>> I guess that meas that for Program all occurrences of the recursive
>>> function must also be fully applied? Is there a trick to use Program
>>> for
>>> variable-width recursion?
>>> 
>>> Otherwise I guess I'll have to use either use Wf.Fix (providing a
>>> variant of map that threads through the size bound) or use bounded
>>> recursion with an extra argument.
>>> 
>>> Are there any other facilities/techniques I should try or does anyone
>>> have experience with this kind of function definition? I'm leaning
>>> towards bounded recursion, since this seems to require minimal use of
>>> dependent types and should yield the smallest/cleanest definition
>>> (possibly at the cost a larger proof burden, i.e, to prove the
>>> fixpoint
>>> equation and the functional induction principle).
>>> 
>>> I'd be thankful for any type of input.
>>> 
>>> Regards,
>>> Christian
>>> 
>>> PS. Is there a way to Abort a Program Definition/Fixpoint etc. Using
>>> "Abort." on an obligation merely seems to shelf this obligation.