The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Hi,

   Perhaps it’s not a direct answer to your question, bit did you try to use mutual inductive types ?

   You can easily define flatten with structural induction (see below). It is also possible to work with the list type, and define your own induction principles.

   

  Best regards,

  Pierre

Inductive arb : Type :=

| A : nat -> arb

| B : nat -> arbs  -> arb

with arbs : Type :=

  anil : arbs

| acons : nat -> arb -> arbs -> arbs.

Scheme arb_rect2 := Induction for arb Sort Type

  with   arbs_rect2 := Induction for arbs Sort Type.

Fixpoint flatten (a : arb) : list nat :=

  match a with

  | A n => [n]

  | B n l => n :: flattens l

  end

with flattens l : list nat

       :=

         match l with

           anil => nil

         | acons  p a l =>  (p::flatten a) ++ flattens l

         end.

Compute flatten (B 7 (acons 8 (A 3) anil)).

Le 14 sept. 2020 à 09:28, Tj Barclay <tjbarclay AT ku.edu> a écrit :

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