The Coq mailing list

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

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 Recdef Program List.

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

(** Needed since Program ignores boolean case splits *)
Lemma propertyP (G : graph) : {property G = true} + {property G = false}.
Proof. case (property G); firstorder. Qed.

Module FixedWidth.

Function foo (G : graph) {measure size G} : nat := 
  if (property G) then foo (dec1 G) else 4.
Proof.
  intros. now apply dec1_lt. 
Qed.

Program Fixpoint bar (G : graph) {measure (size G)} : nat := 
  if (property G) then bar (dec1 G) else 4.
Next Obligation. 
intros. apply dec1_lt. (* missing assumption [property G] *) 
Abort.
Admitted. (* Is there a way to abort a Program definition? *)

Program Fixpoint bar' (G : graph) {measure (size G)} : nat := 
  if (propertyP G) then bar' (dec1 G) else 4.
Next Obligation.
now apply dec1_lt.
Qed.

End FixedWidth.

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 propertyP G 
  then fold_right (fun H m => Nat.max (foo H) m) 0 (decompose G)
  else 4.
Next Obligation.
(* missing [In H (decompose G)] *)
Admitted.

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.