The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

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.