The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi,

Having worked with rose trees (finite trees with unbounded branching)
quite a lot, I would give you the following feedback.

Do not use the inductive definition of Forall' (lifted to Type)
because you are going to need to duplicate a lot of the results
that already exist for Forall (Prop) anyway.

I would suggest using the non-inductive definition:

Forall' P l := forall x, In x l -> P x

This one is much easier to work with.

If you need the position information in "In x l" (which is
available in your inductive definition of Forall'), lift
"In" to Type, ie

In_t : forall X, X -> list X -> Type
In_t x nil := False
In_t x (y::l) := (x = y) + (In_t x l)

but my experience is that it is rarely needed to
have the position information.

Then write the dependent recursor "arb_rect" and prove
fixpoint equations (under some extensionality assumption)
using Fix_F from Wf, see below.

You can specialize the generalized recursor with
non-dependent output type as eg "arb_recursion"
and then fixpoint equations come w/o extensionality
assumptions.

Then you can systematically use the specialize
recursor "arb_recursion" for your definitions
and fixpoint equations are easily derived.

In your example, this would give the following, see below.

Best,

Dominique

-------------------------

Require Import Wf.
Require Import List.
Import ListNotations.

Set Implicit Arguments.

Unset Elimination Schemes.

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

Set Elimination Schemes.

Section arb_rect.

  Let R (x y : arb) :=
    match y with
      | A _ => False
      | B _ l => exists n, In (n,x) l
    end.

  Fixpoint Rwf x : Acc R x.
  Proof.
    destruct x as [ n | n l ].
    + constructor; inversion 1.
    + constructor; intros x (m & Hm).
      revert l Hm; refine (fix loop l := _).
      destruct l as [ | (k,y) l ].
      * intros [].
      * intros [ E | H ].
        - generalize (Rwf y).
          inversion E; trivial.
        - apply (loop l), H.
  Qed.

  Variables (P : arb -> Type)
            (H1 : forall (n : nat), P (A n))
            (H2 : forall (n : nat) (l : list (nat * arb)), (forall p, In
p l -> P (snd p)) -> P (B n l)).

  Definition arb_rect : forall a, P a.
  Proof.
    apply Fix with (1 := Rwf).
    intros [ n | n l ] H.
    + apply H1.
    + apply H2.
      intros (m,x) Hmx.
      apply H; exists m; trivial.
  Defined.

  Hypothesis H2_ext : forall n l f g, (forall p Hp, f p Hp = g p Hp) ->
H2 n l f = H2 n l g.

  Fact arb_rect_fix_1 n : arb_rect (A n) = H1 n.
  Proof.
    unfold arb_rect at 1.
    unfold Fix.
    now rewrite <- Fix_F_eq.
  Qed.

  Fact arb_rect_fix_2 n l : arb_rect (B n l) = H2 n l (fun p _ =>
arb_rect (snd p)).
  Proof.
    unfold arb_rect at 1.
    unfold Fix.
    rewrite <- Fix_F_eq.
    apply H2_ext.
    intros (m,b) H.
    Search Fix_F.
    apply Fix_F_inv.
    + red; apply Rwf.
    + intros []; auto.
      intros f g Hfg; apply H2_ext.
      intros [] ?; apply Hfg.
  Qed.

End arb_rect.

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

Section list_In_map.

  Variable (X Y : Type).

  Fixpoint list_In_map l : (forall x : X, In x l -> Y) -> list Y.
  Proof.
    refine (match l with
      | []   => fun _ => []
      | x::l => fun f => f x _ :: list_In_map l _
    end).
    + left; trivial.
    + intros x' ?; apply (f x'); right; trivial.
  Defined.

  Fact list_In_map_ext l f g :
         (forall x Hx, f x Hx = g x Hx)
      -> list_In_map l f = list_In_map l g.
  Proof.
    revert f g; induction l as [ | x l IHl ]; simpl; f_equal; auto.
    intros f g Hfg; rewrite Hfg; f_equal.
    apply IHl.
    intros; apply Hfg.
  Qed.

  Variable (f : X -> Y).

  Fact list_In_map_map l : list_In_map l (fun x _ => f x) = map f l.
  Proof. induction l; simpl; f_equal; auto. Qed.

End list_In_map.

Section arb_recursion.

  Variables (T : Type)
            (f1 : nat -> T)
            (f2 : nat -> list (nat*T) -> T).

  Definition arb_recursion : arb -> T.
  Proof.
    apply arb_rect.
    + apply f1.
    + intros n l Hl.
      apply (f2 n).
      apply (list_In_map l).
      intros p Hp; split.
      * apply (fst p).
      * apply (Hl _ Hp).
  Defined.

  Fact arb_recursion_fix_1 n : arb_recursion (A n) = f1 n.
  Proof.
    unfold arb_recursion.
    now rewrite arb_rect_fix_1.
  Qed.

  Fact arb_recursion_fix_2 n l : arb_recursion (B n l) = f2 n (map (fun
'(i,a) => (i,arb_recursion a)) l).
  Proof.
    unfold arb_recursion.
    rewrite arb_rect_fix_2.
    + f_equal.
      rewrite list_In_map_map.
      apply map_ext.
      intros []; simpl; auto.
    + intros; f_equal; apply list_In_map_ext.
      intros; f_equal; auto.
  Qed.

End arb_recursion.

Definition flatten : arb -> list nat.
Proof.
  apply arb_recursion.
  + intros n; exact [n].
  + intros n l; exact (n::flat_map (fun c => snd c) l).
Defined.

Fact flatten_fix_1 n : flatten (A n) = [n].
Proof. apply arb_recursion_fix_1. Qed.

Fact flatten_fix_2 n l : flatten (B n l) = n::flat_map (fun p => flatten
(snd p)) l.
Proof.
  unfold flatten at 1.
  rewrite arb_recursion_fix_2; f_equal.
  rewrite !flat_map_concat_map, map_map; f_equal.
  apply map_ext; intros []; auto.
Qed.

Le 14/09/2020 à 09:28, Tj Barclay 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 <http://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 <mailto:tjbarclay AT ku.edu>
> +1 316 259 2250