The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

>threads through the size bound

Essentially you have to do that in some way to prove that the function 
terminates. Using bounded recursion + proving the fixpoint equation on 
the resulting function can be seen as doing that. Function and Program 
are not smart enough to do it.

If you had a version of decompose like [decomp : forall G : Graph, {G' : 
Graph | size G' < size G}] then you can change the Program definition a 
bit, then it works. See attached file (the way decomp is defined may not 
be the smartest possibility but it was easy to do from your axioms).

Gaëtan Gilbert

On 27/06/2017 14:51, 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.

Require Import Program List.

Parameter graph : Type.
Parameter size : graph -> nat.
Parameter property : graph -> bool.
Parameter decompose : graph -> list graph.
Hypothesis decomp_lt : forall G H, In H (decompose G) -> size H < size G.

Fixpoint map_sig_In {A:Type} (l : list A) : list {x : A | In x l}.
Proof.
destruct l as [|x l].
- exact nil.
- simpl. refine (_ :: _).
  + exists x;left;reflexivity.
  + refine (map _ (map_sig_In A l)).
    intros y;exists (proj1_sig y);right;exact (proj2_sig y).
Defined.

Definition decomp : forall G, list {G' : graph | size G' < size G}.
Proof.
intros G.
refine (map _ (map_sig_In (decompose G))).
intros [G' Hsize];exists G'.
apply decomp_lt. exact Hsize.
Defined.

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 Fixpoint foo (G : graph) {measure (size G)} : nat :=
  if property G
  then fold_right (fun G' m => Nat.max (foo (proj1_sig G')) m) 0 (decomp G)
  else 4.
Check foo.