The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

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.