The Coq mailing list

[Tj Barclay <tjbarclay AT ku.edu>]

Enclosed is an arbritrary example (Coq 8.11.2) of an attempt to show termination of a recursive function on the size of a nested-recursive datatype.

Is it possible for the obligation generated by the recursive call to 'flatten' inside the nested fix, 'flatten_list', to also generate hypotheses relating the matched list 'l' and the parameter 'arbs'? In particular,  that 'arbs' will always be a sublist of 'l' or that the matched pair '(_,a')' has the property 'In (_,a') l'.

(* Example Start *)

Require Import Coq.Program.Wf.
Require Import List.
Import ListNotations.

Unset Elimination Schemes.
Inductive Forall' (A : Type) (P' : A -> Type) : list A -> Type :=
| Forall_nil' : Forall' A P' []
| Forall_cons' : forall (x : A) (l : list A), P' x -> Forall' A P' l -> Forall' A P' (x :: l).

Inductive arb : Type :=
| A : nat -> arb
| B : nat -> list (nat * arb) -> arb.

Definition arb_rect_helper (P : arb -> Type) (p : nat * arb) : Type :=
  match p with
  | (x, y) => P y
  end.

Fixpoint arb_rect (P : arb -> Type)
         (H1 : forall (n : nat), P (A n))
         (H2 : forall (n : nat) (l : list (nat * arb)), Forall' (nat * arb) (arb_rect_helper P) l -> P (B n l))
         (a : arb) : P a :=
  match a return (P a) with
  | A n => H1 n
  | B n l => let fix loop (l : list (nat * arb)) :=
                 match l with
                 | [] => Forall_nil' (nat * arb) (arb_rect_helper P)
                 | (n',a')::l' => Forall_cons' (nat * arb) (arb_rect_helper P) (n',a') l' (arb_rect P H1 H2 a') (loop l')
                 end
             in
             H2 n l (loop l)
  end.

Definition arb_rec (P : arb -> Set) := arb_rect P.
Definition arb_ind (P : arb -> Prop) := arb_rect P.
Set Eliminate Schemes.

Fixpoint size_arb (a : arb) : nat :=
  match a with
  | A _ => 1
  | B _ l => 1 + (fix size_list (l : list (nat * arb)) : nat :=
                   match l with
                   | [] => 0
                   | (_,a')::l' => size_arb a' + size_list l'
                   end) l
  end.

(* Function in question *)

Program Fixpoint flatten (a : arb) {measure (size_arb a)}: list nat :=
  match a with
  | A n => [n]
  | B n l => n :: (fix flatten_list (arbs : list (nat * arb)) : list nat :=
                   match arbs with
                   | [] => []
                   | (n',a')::arbs' => n' :: (flatten a' ++ flatten_list arbs')
                end) l
  end.
Obligation 1.

(* Example End *)

Best,

TJ

--

TJ Barclay

Electrcial Engineering & Computer Science, University of Kansas

tjbarclay AT ku.edu

+1 316 259 2250