(** Copyright 2006, 2007, 2012, Ralph Matthes, IRIT, CNRS & Univ. de Toulouse *)
(** This is companion material to the article "A datastructure for Iterated
      Powers", presented at the conference MPC 2006. *) 
(** It has been tested with Coq V8.4 pl1 - just coqide/coqc with no options. *)

(** If execution time seems too high, consider commenting out the lemmas
    that use the vernacular command [Time], in order of decreasing urgency for 
-towerBsh4OK
-linBshOK
-mkBsh3OK
-mkTriBsh3_3ListOK 

Those lemmas only appear in the appendix and hence go beyond the
material in the MPC article. *)


Require Import List.

Set Implicit Arguments.

(** the universe of all monotypes *)
Definition k0 := Set.

(** the type of all type transformations *)
Definition k1 := k0 -> k0.

 (* needed because of sort polymorphism *)
Definition listk1 (A:k0) : k0 := list A. 

(** the identity type transformation *)  
Definition Id : k1 := fun X => X.

(** iterating X n times *)
Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
  match k with 0 => Id
             |  S k' => fun A => X (Pow X k' A)
  end.

(** polymorphic identity *)
Definition id : forall (A:k0), A -> A := fun A x => x.

Section Bsh3.

(** * Introduction: 3-Bushes over Ternary Trees *)

(** 3-bushes and their constructors *)
Variable Bsh3 : k1.
Variable bnil3 : forall (A:k0), Bsh3 A.
Variable bcons3: forall (A:k0), A -> Pow (Bsh3) 3 A -> Bsh3 A.

(** ternary unlabelled finite trees *)
Inductive Tri : k0 := L:Tri | N:Tri->Tri->Tri->Tri. 


Definition mkTriBsh3' : nat -> forall (A:k0), (Tri->A) -> Bsh3 A :=
  fun m A f =>
      (fix F (n:nat)(A:k0)(f:Tri->A) {struct n} : Bsh3 A :=
         match n with 0 => bnil3 _
                     | S m => bcons3 (f L) (F m (Bsh3(Bsh3 A)) (fun t1 => F m (Bsh3 A)
                                            (fun t2 => (F m A (fun t3 => f(N t1 t2 t3))))))
	          end) m A f.
(** the third argument runs the fastest *)

Definition mkTriBsh3 (m:nat) := mkTriBsh3' m (id(A:=Tri)).

Definition mkTriBsh3_3 := Eval compute in mkTriBsh3 3.

(*
Print mkTriBsh3_3.
*)

End Bsh3.

(*
Print mkTriBsh3_3.
*)
  
(** the pure kind of rank 2 *)
Definition k2 := k1 -> k1.

Definition less_k1 (X G:k1) : Type := 
      forall (A B:k0), (A->B) -> X A -> G B.   

Infix "<_k1"  := less_k1 (at level 60).

Definition sub_k1 (X G:k1) : Type :=
     forall A:k0, X A -> G A.

Infix "c_k1" := sub_k1 (at level 60).

(** Refined monotonicity for [k2] *)
Definition mon2  (F:k2) : Type := 
    forall (X G:k1), X <_k1 G -> F X <_k1 F G.

(** ** Refined Conventional Iteration *)
Module Type It_Eq_k1_Type.

  Parameter mu_k1: k2 -> k1.
  Parameter in_k1 : forall F:k2, F(mu_k1 F) c_k1 mu_k1 F.
  Parameter  It_Eq_k1 : forall (G:k1)(F:k2), 
    mon2 F -> F G c_k1 G  -> mu_k1 F <_k1  G.
  Axiom It_Eq_k1_Reduction : forall (G:k1)(F:k2)
   (m:mon2 F)(s:F G c_k1 G)(A:k0)(B:k0) (f:A -> B)(t:F (mu_k1 F) A), 
   It_Eq_k1 m s f (in_k1 _ _ t) = s _ (m _ _ (It_Eq_k1 m s) _ _ f t).

End  It_Eq_k1_Type. 

(** flattening lists, taken from [List.v] in the library *)
Definition flatten : forall (A:k0), list(list A) -> list A := 
  fun A => flat_map (id(A:=list A)).

(** the usual rules for flatten hold in the strong form that both sides
     have the same normal form: *)

Lemma flattenNil : forall (A:k0), flatten(A:=A) nil = nil. 
Proof.
  reflexivity.
Qed.

Lemma flattenCons: forall (A:k0)(a:list A)(l:list(list A)), 
  flatten (a::l) = a ++ flatten l.   
(** ([++] is the usual list append) *)
Proof.
  reflexivity.
Qed.

(** composition *)
Definition comp (A B C:k0)(g:B->C)(f:A-> B) : A-> C := fun x => g (f x).

Infix "o" := comp (at level 90).

(** map is functorial; first law *)
Fact mapid: forall (A:k0)(l:list A), map (id(A:=A)) l = l.
Proof.
  intros.
  induction l.
  reflexivity. 
  simpl.
  apply (f_equal (fun x => a :: x)).
  rewrite IHl.
  reflexivity.
Qed.

(** map is functorial; second law *)
Lemma mapcomp: forall (A B C:k0)(g:B->C)(f:A->B)(l:list A),
            map (g o f) l = map g (map f l).
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  apply (f_equal (fun x=> g(f a) :: x)).
  rewrite IHl.
  reflexivity.
Qed.

(** map only depends on the extension of its first argument 
      (clearly, one could restrict to the x's that occur in l) *)
Lemma mapExt: forall (A B:k0)(f g:A->B)(l:list A),
           (forall x, f x = g x) -> map f l = map g l.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite (H a).
  apply (f_equal (fun x => g a :: x)).
  rewrite IHl.
  reflexivity.
Qed.

(** a preparation for the naturality lemma *)
Lemma mapappend: forall (A B:k0)(f:A->B)(l1 l2:list A),
      map f (l1++l2) = map f l1 ++ map f l2.
Proof.
  intros.
  generalize l2.
  clear l2.
  induction l1.
  intro.  
  reflexivity.
  intro.
  simpl.
  apply (f_equal (fun x=> f a :: x)).
  rewrite IHl1.
  reflexivity.
Qed.

(** naturality of flatten in the categorical sense *)
Lemma mapflatten : forall (A B:k0)(f:A->B)(l:list (list A)),
       flatten(map(map f) l) = map f (flatten l).
Proof.
  intros.
  induction l.
  reflexivity.
  simpl. 
  rewrite IHl.
  unfold id.
  rewrite <- mapappend.
  reflexivity.
Qed.


(** ** Implementation *)
(** we just take a parameter M of this module type *)
Module Bsh3Mod(M:It_Eq_k1_Type).

(** implementation of the 3-bushes *)
Definition BshF3 : k2 :=
   fun X A => (unit + A * (X (X (X A))))%type.

Definition Bsh3 : k1 := M.mu_k1 BshF3.

Definition bnil3 : forall (A:k0), Bsh3 A :=
	fun A => M.in_k1 _  _ (inl _ tt : BshF3 Bsh3 A).

Definition bcons3 : forall (A:k0), A -> Pow Bsh3 3 A -> Bsh3 A :=
	fun A a b =>  M.in_k1 _  _ (inr _ (a, b) : BshF3 Bsh3 A).

Definition bshf3: mon2 BshF3.
Proof.
  do 2 red.
  intros G1 G2 e A B f r.
  elim r.
  intro.
  red. 
  exact (inl _ a). 
  intros [a r'].
  red.  
  apply inr.
  split.
  exact (f a).
  apply (e (G1(G1 A))).
  apply (e (G1 A)).
  apply e.
  assumption.
  assumption.
Defined.



(** turning 3-bushes into lists, first the more general function *)
Definition toListBsh3' : Bsh3 <_k1 listk1.
Proof.
  refine(M.It_Eq_k1 bshf3 (fun A t => _)).
  case t.
  intro.
  exact nil.
  intros [a b].
  apply (cons a).
  exact (flatten(flatten b)).
Defined.


Lemma toListBsh3'Red1 : forall (A B:k0)(f:A->B), 
         toListBsh3' f (bnil3 _) = nil.
Proof.
  intros.
  unfold toListBsh3'.
  unfold bnil3.  
  rewrite M.It_Eq_k1_Reduction.
  reflexivity.
Qed.

Lemma toListBsh3'Red2 : let toL:=toListBsh3' in 
  forall (A B:k0)(f:A->B)(a:A)(b:Pow Bsh3 3 A), 
      toL _ _ f (bcons3 a b) = f a :: flatten(flatten(toL _ _ (toL _ _ (toL _ _ f))b)).
Proof. 
  intros.
  unfold toL at 1.
  unfold toListBsh3'.
  unfold bcons3.  
  rewrite M.It_Eq_k1_Reduction.
  reflexivity.
Qed.


Definition toListBsh3 : Bsh3 c_k1 listk1  :=
  fun A => toListBsh3' (id(A:=A)).

(** the example list *)
Definition mkTriBsh3_3List := toListBsh3(mkTriBsh3_3 Bsh3 bnil3 bcons3).

Lemma mkTriBsh3_3ListOK : mkTriBsh3_3List =
L
:: N L L L
   :: N L L (N L L L)
      :: N L (N L L L) L
         :: N L (N L L L) (N L L L)
            :: N (N L L L) L L
               :: N (N L L L) L (N L L L)
                  :: N (N L L L) (N L L L) L
                     :: N (N L L L) (N L L L) (N L L L) :: nil.
Proof.   
  unfold mkTriBsh3_3List.
  unfold toListBsh3.
  unfold mkTriBsh3_3.
  Time repeat ((rewrite toListBsh3'Red1||rewrite toListBsh3'Red2)).  
(*  unfold flatten.
     simpl. *)
  reflexivity. 
Qed. 

(** the brute-force alternative to the above proof:   
[ compute.
  Time repeat rewrite M.It_Eq_k1_Reduction.
  reflexivity.
Qed.]
*)

Fixpoint Iter(A:Type)(a:A)(s:A->A)(m:nat){struct m}:A :=
  match m with 0 => a
              | S m' => s (Iter a s m')
  end.

Definition aB(A:k0)(f:Tri->A): Bsh3 A := bnil3 A.
Definition sB(v:forall A:k0,(Tri->A)->Bsh3 A)(A:k0)(f:Tri->A): Bsh3 A :=
  bcons3 (f L) 
      (v _ (fun t1 => v _ (fun t2 => (v _ (fun t3 => f(N t1 t2 t3)))))).

Lemma mkTriBsh3'ext : forall (m:nat)(A:k0)(f f':Tri->A),
   (forall x, f x=f' x) -> mkTriBsh3' Bsh3 bnil3 bcons3 m f = 
                                 mkTriBsh3' Bsh3 bnil3 bcons3 m f'.
Proof.
  intro m.
  induction m.
  reflexivity.
  intros.
  simpl.
  rewrite H.
  apply (f_equal (fun x=> bcons3 (f' L) x)).
  simpl.  
  apply IHm. 
  intro.
  apply IHm.
  intro.
  apply IHm.
  intro.
  apply H.
Qed.

Lemma aBsBOk : forall (m:nat)(A:k0)(f:Tri->A),
     mkTriBsh3' Bsh3 bnil3 bcons3 m f = Iter aB sB m A f.
Proof.
  intro m.
  induction m.
  reflexivity.
  intros.
  simpl.
  unfold sB at 1.
  apply (f_equal (fun x=> bcons3 (f L) x)).
  replace (mkTriBsh3' Bsh3 bnil3 bcons3 m
  (fun t1 : Tri =>
   mkTriBsh3' Bsh3 bnil3 bcons3 m
     (fun t2 : Tri =>
      mkTriBsh3' Bsh3 bnil3 bcons3 m (fun t3 : Tri => f (N t1 t2 t3))))) with 
  (mkTriBsh3' Bsh3 bnil3 bcons3 m(fun t1 : Tri =>
   Iter aB sB m (Bsh3 A)
     (fun t2 : Tri => Iter aB sB m A (fun t3 : Tri => f (N t1 t2 t3))))).
  rewrite IHm.
  reflexivity.
  apply mkTriBsh3'ext.
  intro.
  replace (Iter aB sB m (Bsh3 A)
  (fun t2 : Tri => Iter aB sB m A (fun t3 : Tri => f (N x t2 t3)))) with 
  (mkTriBsh3' Bsh3 bnil3 bcons3 m
  (fun t2 : Tri =>  Iter aB sB m A (fun t3 : Tri => f (N x t2 t3)))). 
  apply mkTriBsh3'ext.
  intro.
  rewrite IHm.
  reflexivity.
  rewrite IHm.
  reflexivity.
Qed.     

Definition aL : list Tri := nil (A:=Tri).
Definition sL(l:list Tri) : list Tri :=
  L::flatten(flatten(map(fun t1=>map(fun t2=>map(fun t3=>N t1 t2 t3) l) l) l)).


Definition mkTriList : nat -> list Tri := Iter aL sL.

Eval compute in (mkTriList 3).


Lemma fusion: forall (A A':Type)(a:A)(a':A')(s:A->A)(s':A'->A')(f:A->A'),
  a' = f a -> (forall x:A, s'(f x) = f(s x))  -> forall m:nat, f(Iter a s m) = Iter a' s' m.
Proof.
  intros.
  induction m.
  simpl.
  apply sym_eq.  
  assumption.
  simpl.
  rewrite <- IHm.
  apply sym_eq.
  apply H0.
Qed.

Definition mkTriListMap(m:nat)(A:k0)(f:Tri->A) : list A := map f (mkTriList m).  

Definition map' (l:list Tri)(A:k0)(f:Tri -> A) : list A := map f l.

Definition aM(A:k0)(f:Tri->A): list A := nil (A:=A).

Definition sM(v: forall A:k0,(Tri -> A) -> list A)(A:k0)(f:Tri->A) : list A :=
   f L::flatten(flatten(v _ (fun t1 => v _ (fun t2=> v _ (fun t3 =>f(N t1 t2 t3)))))).

Lemma sMext : forall (v v':forall A:k0,(Tri -> A) -> list A), 
     (forall (A:k0)(f f':Tri->A), (forall x, f x = f' x) -> v _ f = v _ f') -> 
     (forall (A:k0)(f:Tri->A), v _ f = v' _ f) -> 
     forall (A:k0)(f:Tri->A), sM v f = sM v' f.
Proof.
  intros.
  unfold sM.
  apply (f_equal (fun x => f L::flatten(flatten x))).
  replace (v (list (list A))
  (fun t1 : Tri =>
   v (list A) (fun t2 : Tri => v A (fun t3 : Tri => f (N t1 t2 t3)))))
  with 
  (v (list (list A))
  (fun t1 : Tri =>
   v' (list A) (fun t2 : Tri => v' A (fun t3 : Tri => f (N t1 t2 t3))))).
  apply H0.
  apply H.
  intro.
  replace (v (list A) (fun t2 : Tri => v A (fun t3 : Tri => f (N x t2 t3))))
  with (v (list A) (fun t2 : Tri => v' A (fun t3 : Tri => f (N x t2 t3)))).
  apply sym_eq. 
  apply H0.
  apply H.
  intro.
  apply sym_eq.
  apply H0.
Qed.

Lemma sMOk : forall (A:k0)(f:Tri -> A)(l:list Tri), 
      sM (fun A f => map f l) f = map f (sL l).
Proof.
  intros.
  unfold sL.
  simpl map.
  unfold sM.
  rewrite <- mapflatten. 
  rewrite <- mapflatten. 
  apply (f_equal (fun x => f L::flatten (flatten x))).
  rewrite <- mapcomp.
  unfold comp.
  apply mapExt.  
  intro.
  rewrite <- mapcomp.
  unfold comp.
  apply mapExt.
  intro.
  rewrite <- mapcomp.
  unfold comp.
  reflexivity.
Qed.

 
Lemma IteraMsMext : forall (m:nat)(A:k0)(f f':Tri->A),
  (forall x, f x = f' x) -> Iter aM sM m _ f = Iter aM sM m _ f'.
Proof.
  intro m.
  induction m.
  reflexivity.
  intros.
  simpl.
  unfold sM at 1 3.
  rewrite H.
  apply (f_equal (fun x => f' L::flatten (flatten x))).  
  apply IHm.
  intro.
  apply IHm.
  intro.
  apply IHm.
  intro.
  apply H.
Qed.

Lemma mapCons : forall (A B:k0)(f:A->B)(a:A)(l:list A), map f (a::l) = f a :: map f l.
Proof.
  reflexivity.
Qed.

Lemma mkTriListMapOk: forall (m:nat)(A:k0)(f:Tri->A), 
  mkTriListMap m f = Iter aM sM m _ f.
Proof.
  intro m.
  induction m.
  reflexivity.
  intros.
  unfold mkTriListMap.
  simpl.
  rewrite <- mapCons.
  fold (sL (Iter aL sL m)).
  rewrite <- sMOk.
  apply sMext.
  intros.
  apply mapExt.
  assumption. 
  apply IHm.
Qed.
(** Note that a direct application of the fusion rule is impossible since we only
     have our assumptions fulfilled pointwise. *)


Lemma mkTriBsh3'Ok : forall (m:nat)(A B:k0)(f:Tri->A)(g:A->B),
  toListBsh3' g (mkTriBsh3' Bsh3 bnil3 bcons3 m f) = Iter aM sM m _ (g o f).
Proof.
  intro m.
  induction m.
  intros.
  simpl.
  rewrite toListBsh3'Red1. 
  reflexivity. 
(** S m *)
  intros.
  simpl.
  rewrite toListBsh3'Red2.
  unfold comp at 1.
  unfold sM at 1.
  apply (f_equal (fun x => g(f L) :: flatten(flatten x))).
  rewrite IHm.
  unfold comp at 1.
  apply IteraMsMext.
  intro.
  rewrite IHm.
  unfold comp at 1.
  apply IteraMsMext.
  intro.
  rewrite IHm. 
  reflexivity. 
Qed.   

End Bsh3Mod.

(** * n-Bushes *)
Module BshnMod(M:It_Eq_k1_Type).

Module M3 := Bsh3Mod M.

Section Bshn.

(** the fixed parameter n *)
Variable n:nat.

(** n-bushes *)
Definition BshF : k2 :=
   fun X A => (unit + A * Pow X n A)%type.

Definition Bsh : k1 := M.mu_k1 BshF.

(** first constructor *)
Definition bnil  : forall (A:k0), Bsh A :=
	fun A => M.in_k1 _  _ (inl _ tt : BshF Bsh A).

(** second constructor *)  
Definition bcons : forall (A:k0), A -> Pow Bsh n A -> Bsh A :=
	fun A a b =>  M.in_k1 _  _ (inr _ (a, b) : BshF Bsh A).

(** ** From n-Bushes to Lists *)

(** k times iterated flattening *)
Fixpoint flat (k:nat) : forall (A:k0), Pow listk1 k A -> list A :=
  match k return forall (A:k0), Pow listk1 k A -> list A
       with 0 => fun _ a => a::nil
      |   S k' => fun _ l => flatten (map (flat k' _) l)
    end. 

Fixpoint POW  (k:nat)(X G:k1)(i:X<_k1 G){struct k} : Pow X k<_k1 Pow G k :=
  match k return Pow X k<_k1 Pow G k
      with 0 => fun _ _ f  => f 
     |  S k' => fun _ _ f  => i _ _ (POW k' i f) 
   end.

Definition bshf: mon2 BshF.
Proof.
  do 2 red.
  intros X G i A B f t.
  elim t.
  intro u.
  red. 
  exact (inl _ u). 
  intros [a b].
  red.  
  apply inr.
  split.
  exact (f a).
  exact (POW n i f b).
Defined.


Definition toListBsh' : Bsh <_k1 listk1 := M.It_Eq_k1 bshf
  (fun (A : k0) (t : BshF listk1 A) =>
   match t with
   | inl _ => nil (A:=A)
   | inr p => let (a, b) := p in a :: flat n A b
   end).

(** for comparison: how it would be defined interactively *)
Definition toListBsh'interactive : Bsh <_k1 listk1.
Proof.
  refine(M.It_Eq_k1 bshf (fun A t => _)).
  case t.
  intro.
  exact nil.
  intros [a b].
  apply (cons a).
  exact (flat n _ b).
Defined.


Lemma toListBsh'Red1 : forall (A B:k0)(f:A->B), 
         toListBsh' f (bnil _) = nil.
Proof.
  intros.
  unfold toListBsh'.
  unfold bnil.  
  rewrite M.It_Eq_k1_Reduction.
  reflexivity.
Qed.

Lemma toListBsh'Red2 : forall (A B:k0)(f:A->B)(a:A)(b:Pow Bsh n A), 
      toListBsh' f (bcons a b) = f a :: flat n _ (POW n toListBsh' f b).
Proof.
  intros.
  unfold toListBsh' at 1.
  unfold bcons.  
  rewrite M.It_Eq_k1_Reduction.
  reflexivity.
Qed.

(** our interpretation of n-bushes as lists *)
Definition toListBsh : Bsh c_k1 listk1 := fun _ => toListBsh' (id(A:=_)).




(** * Programming the n-Bushes *)


Require Vector.

(* Print Vector.t. *)

(*
Check @Vector.hd : forall (A : Set) (n : nat), Vector.t A (S n) -> A.
Check @Vector.tl : forall (A : Set) (n : nat), Vector.t A (S n) -> Vector.t A n.
*)

Inductive Tree: k0 := L' : Tree | N' : Vector.t Tree n -> Tree.
Definition vec (k:nat) := Vector.t Tree k.
Definition vnil : vec 0 := Vector.nil Tree.
Definition vcons (t:Tree)(k:nat) : vec k -> vec (S k) := Vector.cons Tree t k.

Fixpoint LL(l:list Tree)(k:nat){struct k} : (vec k->Tree) -> Pow listk1 k Tree :=
  match k return  (vec k->Tree) -> Pow listk1 k Tree
       with 0 => fun f => f vnil
       |  S k' => fun f => map (fun t => LL l (f o (vcons t (k:=k')))) l
  end.


Definition aLn : list Tree := nil (A:=Tree).
Definition sLn (l:list Tree) : list Tree :=  L'::flat n _ (LL l N').

Definition mkTriListn : nat -> list Tree := M3.Iter aLn sLn.

Fixpoint BB (v:forall A:k0, (Tree ->A) -> Bsh A)(k:nat)(A:k0){struct k}: 
   (vec k -> A) -> Pow Bsh k A :=
  match k return (vec k -> A) -> Pow Bsh k A 
       with 0 => fun f => f vnil
       | S k' =>  fun f => v (Pow Bsh k' A)(fun t => BB v (f o (vcons t (k:=k'))))
  end.

Definition aBn (A:k0)(f:Tree -> A) : Bsh A := bnil _.
Definition sBn (v:forall A:k0, (Tree ->A) -> Bsh A)(A:k0)(f:Tree -> A) : Bsh A :=
    bcons (f L') (BB v (f o N')).

Definition mkTreeBsh': nat -> forall A:k0, (Tree -> A) -> Bsh A :=
  M3.Iter aBn sBn.

Definition mkTreeBsh (m:nat) : Bsh Tree :=
   mkTreeBsh' m (fun x=>x).

Definition T (m:nat) : Prop := forall (A B:k0)(f:Tree->A)(g:A->B), 
   toListBsh' g (mkTreeBsh' m f) = map (g o f) (mkTriListn m).
Definition P (m k:nat) : Prop := forall (A B : k0) (f0:vec k->Tree)
    (f : Tree -> A) (g : A -> B),
    flat k B (POW k toListBsh' g (BB (mkTreeBsh' m) (f o f0))) =
    map (g o f) (flat k Tree (LL (mkTriListn m) f0)).

(** the more concrete statement is a corollary to T *)
Lemma ThmImpTheorem : forall (m:nat), T m ->
             toListBsh (mkTreeBsh m) = mkTriListn m.
Proof.
  intros.
  unfold toListBsh.
  unfold mkTreeBsh.
  rewrite H.
  unfold comp.
  change (fun x : Tree => id x) with (id(A:=Tree)).
  exact (mapid _).
Qed.  

Lemma ThmImpProp : forall (m:nat), T m -> forall (k:nat), P m k.
Proof.
  intros m Tm k.
  induction k.
  red.  
  reflexivity.
  red.
  intros.
  simpl.
(* rewrite (Tm _ _ (fun t : Tree => BB (mkTreeBsh' m) ((f o f0) o (vcons t (k:=k))))
     (POW k toListBsh' g)). *)
  rewrite Tm.
  rewrite <- mapcomp.
  unfold comp at 1 2.
  replace (map
     (fun x : Tree =>
      flat k B
        (POW k toListBsh' g
           (BB (mkTreeBsh' m)
              ((f o f0) o (vcons  x (k:=k))))))
     (mkTriListn m)) with (map
     (fun x : Tree => map (g o f) (flat k Tree (LL (mkTriListn m) (f0 o (vcons x (k:=k)))))
      )
     (mkTriListn m)).
Focus 2.
  apply mapExt.
  intro.
  change ((f o f0) o (vcons x (k:=k))) with 
  (f o (f0 o (vcons x (k:=k)))).
  rewrite IHk.
  reflexivity.
(** back *)
  rewrite <- mapcomp.
  rewrite <- mapflatten.
  rewrite <- mapcomp.
  reflexivity.
Qed.


Lemma Main : forall m, T m.
Proof.
  induction m.
  red.
  intros.
  unfold mkTreeBsh'.
  simpl.
  unfold aBn.  
  rewrite toListBsh'Red1.
  reflexivity.
(** S m *)
  red.
  intros.
  unfold mkTreeBsh'.
  simpl.
  unfold sBn.
  rewrite toListBsh'Red2.
  unfold comp at 3.
  apply (f_equal (fun x => g(f L'):: x)).
  apply (ThmImpProp IHm).
Qed.

End Bshn.

Definition N'alt(t1 t2 t3:Tree 3): Tree 3 :=
  N' (vcons t1 (vcons t2 (vcons t3 (vnil 3)))).

Lemma sLn3Ok : sLn (n:=3) = fun l:list (Tree 3) =>
  L' 3:: flat 3 _ (map (fun t1 => map (fun t2 => map (fun t3 => N'alt t1 t2 t3)l)l)l).
Proof.
  reflexivity.
Qed.
 
Lemma sBn3Ok : sBn (n:=3) = fun (v:forall A : k0, (Tree 3 -> A) -> Bsh 3 A)
       (A:k0)(f:Tree 3-> A) => 
   bcons 3 (f (L' 3))(v _ (fun t1 => v _ (fun t2 => v _ (fun t3 => f(N'alt t1 t2 t3))))).
Proof.
  reflexivity.
Qed.

(** * A P P E N D I X *)

(** ** Towerbushes *)

Section Tower.
Require Import Plus.
Require Import Mult.
(** This development has been described in the first submitted version of the MPC '06
      article. Here, we define elements of Bsh n nat that contain precisely the elements
      0, 1,..., powerplus m n -1. This is the number of n-ary trees of height less than m,
      but here we directly work with natural numbers.
 *)

Variable n:nat.

(** the crucial auxiliary function for defining towerbushes *)
Fixpoint FF (F:forall (A:k0), (nat -> A) -> Bsh n A)(k:nat){struct k} :
                 forall (A:k0),(nat->A)->nat->nat-> Pow (Bsh n) k A :=
  match k return forall (A:k0),(nat->A)->nat->nat-> Pow (Bsh n) k A
     with 0 => fun _ f t off => f (S off)
     | S k' => fun _ f t off => F _ (fun x => FF F k' f t (off * t + x))
    end.

(** exponentiation x^k *)
Fixpoint pow (k:nat)(x:nat) {struct k} : nat :=
   match k with 0 => 1
              |  S k' => x * pow k' x
   end.

(** iterated exponentiation with exponent n plus 1 *)
Fixpoint powerplus (m:nat) : nat :=
   match m with 0 => 0
              |  S m' => S (pow n (powerplus m'))
   end.

Notation "# m" := (powerplus m) (at level 0, m at level 0).

(** the desired function, first more generally with a function 
    argument f that changes during the recursion in FF *)
Fixpoint towerBsh' (m:nat) : forall (A:k0), (nat -> A) -> Bsh n A :=
  match m return forall (A:k0), (nat -> A) -> Bsh n A with
     |  0     => fun _ _ => bnil n _
     | S m' => fun _ f => bcons n (f 0) 
                (FF (towerBsh' m') n f (# m') 0)
     end.

(** the n-bush with [# m] elements, from 0 onwards numbered *)
Definition towerBsh (m:nat) : Bsh n nat := towerBsh' m (id(A:=_)).

(** ** Verification *)
(** list of i numbers from x onwards *) 
Fixpoint count (x i:nat){struct i} : list nat :=
  match i with 0 => nil
             |  S i' => x::count (S x) i' end.

(** list of first i numbers *)
Definition first (i:nat) := count 0 i.

(** a simple observation *)
Fact appendCount : forall (a b c:nat),
   (count a b) ++ (count (a+b) c) = count a (b+c).
Proof.
  intros.
  generalize a.
  clear a.
  induction b.
  intro a.
  rewrite plus_0_r.
  reflexivity.
  (** S b *)
  intro a.
  simpl.
  apply (f_equal (fun x => a :: x)).
  rewrite <- IHb.
  apply (f_equal (fun x => count(S a)b ++ x)).
  rewrite plus_Snm_nSm. 
  reflexivity.
Qed.

(** the crucial combinatorial lemma for the verification *)
Lemma flattenCount : forall (a b c d:nat), 
  flatten(map (fun x => count (a+x*b) b) (count c d)) = count (a+c*b)(b*d).
Proof.
  intros.
  generalize c.
  clear c.
  induction d.
  intro.
  simpl.
  rewrite mult_0_r.
  reflexivity.
  (** S d *)
  intro.
  simpl.
  rewrite IHd.
  rewrite <- mult_n_Sm.
  rewrite (plus_comm (b*d) b).
  rewrite <- appendCount.
  apply (f_equal (fun x => count(a+c*b)b ++ x)).
  simpl.
  rewrite <- plus_assoc.
  rewrite (plus_comm (c*b) b).
  reflexivity.
Qed.

(** Here, we parallel the proof structure for mkTreeBsh'. *)

(** the theorem as a definition of a statement *)
Definition T' (m:nat) : Prop := forall (A B:k0)(f:nat->A)(g:A->B), 
   toListBsh' g (towerBsh' m f) = map (g o f) (first (# m)).

(** the more concrete statement is a corollary to T' *)
Lemma ThmImpTheorem' : forall (m:nat), T' m ->
             toListBsh (towerBsh m) = first (# m).
Proof.
  intros.
  unfold toListBsh.
  unfold towerBsh.
  rewrite H. 
  unfold id.
  unfold comp. 
  rewrite (mapid(A:=nat)).
  reflexivity. 
Qed.

(** the proposition as a definition of a statement *)
Definition P' (m k:nat) : Prop := 
   forall (A B:k0)(f:nat->A)(g:A->B)(off:nat),
     flat k _ (POW k (toListBsh'(n:=n)) g (FF (towerBsh' m) k f (# m) off)) = 
     map (g o f) (let num := pow k (# m) in count (S(off*num)) num).


(** at stage m, the theorem implies the proposition *)
Lemma ThmImpProp' : forall (m:nat), T' m -> forall (k:nat), P' m k.
Proof.
  intros m Tm k.
  induction k.
  (** 0 *)
  red.
  intros.
  simpl.
  apply (f_equal (fun x => x :: nil(A:=B))).
  rewrite mult_1_r.
  reflexivity.
  (** S k *)
  red.
  intros.
  simpl.
  rewrite Tm.
  rewrite <- mapcomp.
  unfold comp at 1 2.
  simpl. 
  replace (map
     (fun x : nat =>
      flat k B (POW k (toListBsh'(n:=n)) g (FF (towerBsh' m) k f #m (off * #m + x))))
     (first #m))
  with (map
     (fun x : nat => map (g o f) 
         (let num := pow k (# m) in 
    count (S((off * (# m) + x)*num)) num))(first (# m))).
(** first justify the replacement *)  
  Focus 2.
  apply mapExt.
  intro.
  simpl.
  rewrite IHk.
  apply (f_equal(map(g o f))).
  reflexivity.
(** back to the main proof *)
  change (fun x : nat =>
      map (g o f)
        (let num := pow k (# m) in
         count (S ((off * (# m) + x) * num)) num)) 
  with ((map (g o f)) o (fun x : nat =>let num := pow k (# m) in
         count (S ((off * (# m) + x) * num)) num)).
  rewrite mapcomp.
  rewrite mapflatten.
  apply (f_equal(map(g o f))).
  unfold first.
  replace (map
    (fun x : nat =>
       count (S ((off * (# m) + x) * (pow k (# m)))) 
      (pow k (# m)) )
          (count 0 (# m))) with
    (map
      (fun x : nat =>
         count (S (off * (# m * (pow k (# m)))) +
                x * (pow k (# m))) (pow k (# m)) )
          (count 0 (# m))).
  rewrite flattenCount.
  (** How can the remainder be automatized? *)
  apply (f_equal2 count).
  rewrite (mult_comm (# m)(pow k (# m))).
  simpl.
  apply (f_equal S).
  rewrite plus_0_r.
  reflexivity.
  rewrite mult_comm.
  reflexivity.
(** justification of the replacement *)
  apply mapExt.
  intro.
  apply (f_equal2 count).
  simpl.
  apply (f_equal S).
  rewrite mult_plus_distr_r.
  apply (f_equal (fun y => y + x * pow k #m)).
  rewrite mult_assoc.
  reflexivity.
  reflexivity.
Qed.

Theorem Main' : forall (m:nat), T' m.
Proof.
  intro.
  induction m.
  (** 0 *)
  red.
  intros.
  simpl.
  rewrite toListBsh'Red1.
  reflexivity.
  (** S m *)
  red.
  intros.
  simpl.
  rewrite toListBsh'Red2.
  apply (f_equal (fun x => g(f 0) :: x)).
  exact (ThmImpProp' IHm n f g 0).
Qed.

End Tower.

(* Check Main. *)


(** ** On the Definition of [flat 3] *)

(** We argue that, extensionally, toListBsh3' is the same as the instance of
     toListBsh' for n:=3 *)

(** flattening singletons *)
Lemma flattensingl : forall (A:k0)(l: list A), 
        flatten (map (fun a => a::nil) l) = l.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  reflexivity.
Qed. 

Lemma flat1OK: forall (A:k0)(l:list A),
         flat 1 _ l = l.
Proof.
  intros.
  simpl.
  rewrite flattensingl.
  reflexivity.
Qed.

Lemma flat2OK: forall (A:k0)(l:list(list A)),
         flat 2 _ l = flatten l.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite flattensingl.
  unfold Id.
  apply (f_equal (fun x => flatten(A:=A)(a :: x))).
  replace (map (fun l0 : listk1 A => flatten (map (fun a0 : A => a0 :: nil) l0)) l)
  with (map (fun l0 : list A => l0) l).
  rewrite (mapid(A:=list A)).
  reflexivity.
  apply mapExt.
  intro.
  rewrite flattensingl.
  reflexivity.
Qed.

(** a simple preparation *)
Lemma flattenappend: forall (A:k0)(l1 l2:list(list A)),
        flatten(l1 ++ l2) = flatten l1 ++ flatten l2.
Proof.
  intros.
  induction l1.
  reflexivity.
  (** [a::l1] *)
  simpl.
  rewrite IHl1. 
  apply sym_eq.  
  apply app_ass. 
Qed.



Infix "o" := comp (at level 90).

Definition flat3 (A:k0) : Pow listk1 3 A -> list A := 
       flatten(A:=A) o flatten(A:=list A).

(** the crucial observation *)
Lemma flat3OK: forall (A:k0)(l:Pow listk1 3 A),
         flat 3 _ l = flat3 l.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  unfold Id.
  unfold flat3.
  unfold comp.  
  unfold listk1.
  rewrite flattenCons.
  rewrite flattenappend. 
  apply (f_equal2(app(A:=A))).
  replace (map (fun l0 : list A => flatten (map (fun a0 : A => a0 :: nil) l0)) a)
  with  (map (fun l0 : list A => l0) a).
  rewrite (mapid(A:=list A)).
  reflexivity.
Focus 2.
  simpl in IHl.
  unfold Id in IHl.
  assumption.
(** justifying the replacement: *)
  apply mapExt.
  intro.
  rewrite flattensingl.
  reflexivity.
Qed.


(** Hence, the arguments to M.It_Eq_k1 for toListBsh3' and for toListBsh' 3
are extensionally equal and we expect that those two functions will be 
extensionally equal as well. *) 

(** ** Testing towerBsh' *)

Section Testing.

(** the n-bush with [#n m] elements, taken from the list l, with
      the default element if there are not sufficiently many elements in l *)
Definition mkBsh (n m:nat)(A:k0)(default:A)(l:list A) : Bsh n A :=
    towerBsh' n m (fun x => nth x l default).


Lemma mkBsh3OK: toListBsh(mkBsh 3 3 99 (first 6))= first 6 ++ 99::99::99::nil.
Proof.  
  unfold first at 1.
  unfold mkBsh.
  simpl.
  unfold toListBsh.
Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)).  
  reflexivity.      
Qed.   


Lemma towerBsh4OK: forall (g:nat->nat), 
   toListBsh' g (towerBsh 4 3) = map g (first (powerplus 4 3)).
Proof.
  intro.
  unfold towerBsh.
  simpl.
  Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)).  
  reflexivity. 
Qed.
(* Admitted. *)
(** We could have saved time in not saving the proof with [Qed.] but using [Admitted.] instead. *)

(** the following is not carried out in order to save time: [ 
Lemma tower_bsh5finalOK: forall (g:nat->nat), 
   toListBsh' g (towerBsh 5 3) = map g (first (powerplus 5 3)).
Proof.
  intro.
  unfold towerBsh.
  simpl.
  Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)). ]
*)
(** an idea of the time consumption on a 2005 laptop: [Finished transaction in 539. secs (532.88u,1.12s)] *)   
(** [ reflexivity. ]
*)

End Testing.

(** ** n-Bushes with i Elements for any i *) 
Section LinearBushes.
(** We show that one can easily get elements of Bsh n with a given number 
      of data entries. *)

(** singletons in Pow (Bsh n) k A for n>0 *)
Fixpoint sg (n k:nat)(A:k0)(a:A){struct k} : Pow (Bsh (S n)) k A :=
     match k return Pow (Bsh (S n)) k A with 
              | 0 => a
              | S k' => bcons (S n) (sg n k' a) (bnil _ _)
          end.

(** function for constructing bushes with k elements *)
Fixpoint linBsh (n x i:nat)(A:k0)(f:nat->A) {struct i} : Bsh (S n) A :=
	  match i  with
	    | 0  => bnil (S n) _
            | S i' => bcons (S n) (f x) (linBsh n (S x) i' ((sg n n (A:=_)) o f))
	  end.


(** testing: *)
Variable ft : nat -> nat.
Lemma  linBshOK : toListBsh (linBsh 3 7 5 ft) = map ft  (count 7 5).
Proof.
  simpl.
  unfold comp.
  unfold toListBsh.
Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)).
(** On a 2010 laptop: Finished transaction in 6. secs (5.344334u,0.s)  *) 
  reflexivity.
Qed.

Section Verification.

Variable n:nat. (** n is just a parameter of the whole verification *)

Definition linBshThm (i:nat) : Prop :=
    forall(x:nat)(A B:k0)(f:nat->A)(g:A->B),
      toListBsh' g (linBsh n x i f) = map (g o f) (count x i).

(** the auxiliary proposition where the eta-expansions of f is needed *)
Definition linBshProp (i k:nat) : Prop :=
    forall(x:nat)(A B:k0)(f:nat->A)(g:A->B),
       flat (S k) _ (POW (S k) (toListBsh' (n:=S n)) g (linBsh n x i ((sg n k (A:=_)) o f))) 
                   =     toListBsh' g (linBsh n x i (fun y => f y)).

(** some preparation *)
Lemma linBshPrep : forall (k:nat)(A B:k0)(f:A->B)(a:A),
     flat k _ (POW k (toListBsh' (n:=S n)) f (sg n k a)) =  f a::nil.
Proof.
  intros.
  induction k.
  reflexivity.
  simpl.
  fold Pow.
  rewrite toListBsh'Red2.
  simpl.
  rewrite IHk.
  simpl.
  rewrite toListBsh'Red1.
  reflexivity.
Qed.


(** the crucial lemma for the later induction step *)
Lemma linBshThmImpProp : forall (i:nat), 
        linBshThm i -> forall (k: nat), linBshProp i k. 
Proof.
  intros.
  destruct k.
  red.
  intros.
  simpl.
  rewrite flattensingl.
  reflexivity.
  (** S k *)
  red.
  intros.
  set (k':=S k).
  unfold POW.
  fold POW.
  unfold flat.
  fold flat.
  rewrite H.
  rewrite <- mapcomp.
  unfold comp.
  replace (map
     (fun x0 : nat =>
      flat k' B (POW k' (toListBsh' (n:=S n)) g (sg n k' (f x0))))
     (count x i)) with
   (map (fun x:nat => g(f x)::nil)(count x i)).
Focus 2.
  apply mapExt.
  intro.
  rewrite linBshPrep.
  reflexivity.
  change (fun x : nat => g (f x) :: nil) with ((fun x => x::nil) o (g o f)).
  rewrite mapcomp.
  rewrite flattensingl.
  rewrite H.
  reflexivity.
Qed.

Lemma linBshMain : forall (i:nat), linBshThm i.
Proof.
  red.
  intro.
  induction i.
  intros.
  simpl.
  rewrite toListBsh'Red1.
  reflexivity.
  (** S i *)
  fold (linBshThm i) in IHi.
  intros.  
  simpl.
  rewrite toListBsh'Red2.
  apply (f_equal (fun y => g(f x) :: y)).
  rewrite (linBshThmImpProp IHi). 
  apply (IHi (S x) _ _ (fun y : nat => f y) g).
Qed.

(** Hence, linBsh n x i f contains i elements. *)

End Verification.
End LinearBushes.

End BshnMod.


(** #<b># Acknowledgement: #</b># 

The student project of Dulma Rodriguez with me at LMU Munich (and still
during my first months in Toulouse) brought
up the questions that led to this work. I am especially thankful to
her for the programs that compute a powerlist of height n with
elements 1,...,2^n, the linear 2-bush (with an arbitrary finite number
of elements) and the 2-bushes with a number of entries that iterates
squares. My efforts to verify them led me to the present programs.
The whole student project, carried out also in Coq, can be found at
#<a href="http://www.tcs.ifi.lmu.de/~rodrigue/project.html"
><tt>#http://www.tcs.ifi.lmu.de/~rodrigue/project.html#</tt></a>#.
I also made use of some of the code lines.

*)