(** BushPred.v Version 2.0.1 December 2012 *)
(** does not need impredicative Set, runs under V8.4, tested with 8.4pl1 *)

(** Copyright  Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse *)

(** illustrates how LNMItPred.v allows to treat the example of bushes *)

(** this is code that conforms to the description in the article
    "An induction principle for nested datatypes in intensional type theory"
    by the author, to appear in the Journal of Functional Programming *)

Set Implicit Arguments.

Require Import LNMItPred.

(** Some preparations for lists *)
Require Import List.

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

Lemma listEFct: EFct listk1.
  apply (mkEFct (X:=fun (A:Set) => list A)(m:=map)); red; intros.
  apply map_ext; assumption.
  induction x.
  reflexivity.
  simpl.
  rewrite IHx.
  reflexivity.
  rewrite map_map.
  reflexivity.
Defined.
(* this definition has been made just for systematic reasons and will not be used *) 

(*
Print flat_map.
yields
flat_map = 
fun A B : Type =>
fix flat_map (f : A -> list B) (l : list A) {struct l} : list B :=
  match l with
  | nil => nil (A:=B)
  | x :: t => f x ++ flat_map f t
  end
     : forall A B : Type, (A -> list B) -> list A -> list B
*)

Lemma flat_mapsingleton (A:k0)(l:list A): flat_map (fun a => a::nil) l = l.
Proof.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  reflexivity.
Qed. 
(** not necessary in the sequel *)

Lemma flat_map_app (A B:k0)(f: A -> list B)(l1 l2:list A): 
  flat_map f (l1++l2) = flat_map f l1 ++ flat_map f l2.
Proof.
  intros.
  induction l1.
  reflexivity.
  simpl.
  rewrite IHl1.
  rewrite app_ass.
  reflexivity.
Qed.
(** not necessary in the sequel *)

Lemma flat_mapext (A B:Set)(f g:A -> list B)(l:list A): 
   (forall a, f a = g a) -> flat_map f l = flat_map g l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite H.
  rewrite IHl.
  reflexivity.
Qed.

Lemma flat_mapext_refined (A B:Set)(f g:A -> list B)(l:list A): 
   (forall a, In a l -> f a = g a) -> flat_map f l = flat_map g l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite H.
  rewrite IHl.
  reflexivity.
  intros.
  apply H.
  simpl; right; assumption.
  simpl; left; reflexivity.
Qed.

(** interaction of flat_map with map *)
Lemma flat_mapLaw1 (A B C:k0)(f: A -> B)(g:B -> list C)(l: list A): 
  flat_map g (map f l) = flat_map (g o f) l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite IHl.
  reflexivity.
Qed.  

(* an instructive instance *)
Lemma flat_mapLaw1Inst (A B:Set)(f: A -> list B)(l: list A): 
  flat_map (id(A:=list B)) (map f l) = flat_map f l.
Proof.
  intros.
  rewrite flat_mapLaw1.
  apply flat_mapext.
  reflexivity.
Qed.


 Lemma flat_mapLaw2: forall (A B C : Set) (f : A -> list B) (g : B -> C) (l : list A),
  map g (flat_map f l) = flat_map (map g o f) l.
Proof.
  intros.
  induction l; intros; simpl.
  reflexivity.
  rewrite map_app.
  rewrite IHl.
  reflexivity.
Qed.  

(** we use moncomp from LNMItPred.v *)
Lemma flat_mapNAT (X:k1)(mX: mon X)(h:X c_k1 listk1)(n: NAT h mX map): 
  NAT(Y:=listk1) (fun A=> flat_map (h A)) (moncomp(X:=listk1) map mX) map.
Proof.  
  red.
  intros.
  unfold moncomp.
  transitivity (flat_map (map f o h A) t).
  rewrite flat_mapLaw1.
  apply (flat_mapext(B:=B) (h B o mX A B f) (map f o h A) t).
  intro.
  unfold comp.
  unfold NAT in n.
  exact (n A B f a).
(* the second part *)
  apply sym_eq.
  exact (flat_mapLaw2 (h A) f t).
Qed.

Lemma flat_mapMonad3: forall (A B C : Set) (f : A -> list B) (g : B -> list C) (l : list A),
  flat_map g (flat_map f l) = flat_map ((flat_map g) o f) l.
Proof.
  induction l; intros.
  reflexivity.
  simpl.
  rewrite flat_map_app.
  rewrite IHl.
  reflexivity.
Qed.


Definition natCont (A:k0) := (A -> nat) -> nat.

(** the following definitions and lemmas are not needed for the sequel: *)
Definition natCont_mon: mon natCont.
Proof.
  red.
  unfold natCont.
  intros.
  exact (H0 (H1 o H)).
Defined.

Definition eta_natCont: forall (A:k0), A -> natCont A.
Proof.
  red.
  intros A a g.
  exact (g a).
Defined.

Definition bind_natCont: forall (A B : k0), (A -> natCont B) -> natCont A -> natCont B.
Proof.
  unfold natCont.
  intros A B f c g.
  apply c.
  intro a.
  exact (f a g).
Defined.
  
Lemma natCont_monad1_pointwise: forall (A B:k0)(f:A -> natCont B)(a:A)(g:B->nat), 
   bind_natCont f (eta_natCont a) g = f a g.
Proof.
  reflexivity.
Qed.

Lemma natCont_monad2_pointwise_weak: forall (A:k0)(c:natCont A)(g:A->nat), 
  bind_natCont (eta_natCont(A:=A)) c g = c (fun a : A => g a) . 
Proof.
  reflexivity.
Qed.

Lemma natCont_monad3_pointwise: forall (A B C:k0)(f:A->natCont B)(g:B->natCont C)
  (c:natCont A)(h:C->nat),
    bind_natCont g (bind_natCont f c) h = bind_natCont ((bind_natCont g) o f) c h.
Proof.
  reflexivity.
(* more perspicuous is:
  intros.
  unfold bind_natCont.
  unfold comp.
  reflexivity.
*)
Qed.
  
(** end of digression *)  
  

(* the following definition will be later be a tool to relate sizeDirect and sizeIndirect *)
Definition listToValue: listk1 c_k1 natCont.
Proof.
  red.
  intros A l.
  induction l; red; intro f.
  exact 0.
  exact (f a + IHl f).
Defined.

Lemma listToValueExt (A:k0)(l: list A)(f g:A->nat):
  (forall a, f a = g a) -> listToValue l f = listToValue l g.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  rewrite H.
  reflexivity.
Qed.

(* not necessary in the sequel: *)
Lemma listToValueNAT (A B:k0)(f:A->B)(g:B->nat)(l:list A):
  listToValue (map f l) g =  listToValue l (g o f).
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  reflexivity.
Qed.


Lemma listToValueAppend (A:k0)(l l':list A)(f:A->nat):
  listToValue (l++l') f = listToValue l f + listToValue l' f.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  rewrite Plus.plus_assoc.
  reflexivity.
Qed.
  

Lemma listToValueFlat_map(A B:k0)(l: list A)(g: A -> list B)(f: B->nat):
  listToValue (flat_map g l) f  = listToValue l (fun a => listToValue (g a) f).
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite listToValueAppend.
  rewrite IHl.
  reflexivity.
Qed.

(** the previous lemma is a pointwise ("f-wise") version of the "bind part" of the statement that 
     listToValue is a monad morphism between the monads for list and natCont: *)
Lemma listToValueMonadMorphism_bind_pointwise: forall (A B:k0)(l: list A)(g: A -> list B)(f: B->nat),
  listToValue (flat_map g l) f  = bind_natCont  (listToValue(A:=B) o g) (listToValue l) f.
Proof.
  intros.
  unfold bind_natCont .
  unfold comp.
  apply listToValueFlat_map.
Qed.

Lemma listToValueMonadMorphism_eta_pointwise: forall (A:k0)(a:A)(g:A->nat),
  listToValue (a::nil) g = eta_natCont a g.
Proof.
  intros.
  simpl.
  unfold eta_natCont.
  auto.
Qed.
(** the previous two lemmas will not be used in the sequel *)


Lemma listSize (A:k0)(l:list A): length l = listToValue l (fun _=>  1).
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  reflexivity.
Qed.


(** the preparations are done *)

Open Scope type_scope. (* asterisk is interpreted as product of types *)

Definition BushF(X:k1)(A:Set) :=  unit + A  * X (X A).

Definition bushpEFct : pEFct BushF.
Proof.
  unfold BushF.
  apply sumpEFct.
  apply constpEFct.
  apply constEFct.
  apply prodpEFct.
  apply constpEFct.
  apply idEFct.
  apply comppEFct.
  apply idpEFct.
  apply idpEFct_eta.
Defined.

Lemma bushpEFctmon (X:k1)(ef: EFct X): 
  m (bushpEFct ef) = 
    fun (A B : Set) (f : A -> B) (t : BushF X A) =>
       match t with
       | inl u => inl (B * X (X B)) u
       | inr p =>
           inr unit (let (a, b) := p in (f a, m ef (m ef  f) b))
       end.
Proof.
  intros.
  simpl.
  unfold idpEFct.
  unfold idpEFct_eta.
  induction ef.
  simpl.
  reflexivity.
Qed.
(** this lemma will not be needed in the sequel *)


Module Type BUSH := LNMIt_Type with Definition F:=BushF
                                                with Definition FpEFct := bushpEFct.


(** we base this on a hypothetical implementation of BUSH *)
Module Bush (BushBase:BUSH).

Module BushM := LNMItDef BushBase.

Definition Bush : k1 := BushBase.mu2.

Definition bnil : forall (A:k0), Bush A :=
	fun A => BushM.InCan  (inl _ tt : BushF Bush A).

Definition bcons : forall (A:k0), A -> Bush (Bush A) -> Bush A :=
	fun A a b =>  BushM.InCan (inr _ (a, b) : BushF Bush A).

(* the two general constructors *)
Definition bnil_(A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2): Bush A :=
    BushBase.In ef n  (inl _ tt : BushF G A).

Definition bcons_(A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): Bush A :=
    BushBase.In ef n  (inr _ (a,b) : BushF G A).

Lemma bnilbnil_ (A:k0): bnil A = bnil_ A
   BushM.mapmu2EFct (j:= fun _ x => x)(fun _ _ _ _ => refl_equal _).
Proof.
  reflexivity.
Qed.

Lemma bconsbcons_  (A:k0)(a:A)(b:Bush(Bush A)):
            bcons a b = bcons_  
   BushM.mapmu2EFct (j:= fun _ x => x)(fun _ _ _ _ => refl_equal _) a b.
Proof.
  reflexivity.
Qed.


Definition bush : mon Bush := BushBase.mapmu2.

(* bush's behaviour for the general constructors *)
Lemma bush_bnil_ (A B:k0)(f:A->B)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2): bush f (bnil_  A ef n) = bnil_ B ef n.
Proof.
  intros.
  unfold bush.
  unfold bnil_.
  rewrite BushBase.mapmu2Red.
  unfold BushBase.FpEFct.
  reflexivity.
Qed.

Lemma bush_bcons_ (A B:k0)(f:A->B)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): 
            bush f (bcons_  ef n a b) = bcons_ ef n (f a) (m ef (m ef f) b).
Proof.
  intros.
  unfold bush.
  unfold bcons_.
  rewrite BushBase.mapmu2Red.
  unfold BushBase.FpEFct.
  simpl.
  unfold idpEFct.
  induction ef. (* is really needed here *)
  reflexivity.
Qed.

(* now for the canonical constructors *)
Lemma bush_bnil (A B:k0)(f:A->B): bush f (bnil A) = bnil B.
Proof.
  intros.
  rewrite bnilbnil_.
  rewrite bush_bnil_.
  reflexivity.
Qed.

Lemma bush_bcons (A B:k0)(f:A->B)(a:A)(b:Bush(Bush A)): 
        bush f (bcons a b) = bcons (f a) (bush (bush f) b).
Proof.
  intros.
  rewrite bconsbcons_.
  rewrite bush_bcons_.
  reflexivity.
Qed.


(* bushes into lists, just with plain Mendler iteration *)
Definition BushToList : Bush c_k1 listk1. 
Proof.
  refine (BushBase.MIt (fun (X:k1)(it: X c_k1 listk1)(A:Set)(t:BushF X A) => _)).
  destruct t as [u|(a,b)].
  exact (nil(A:=A)).
  exact (a::flat_map(it A)(it (X A) b)).
Defined.

(* the behaviour of BushToList for the canonical constructors *)
Lemma BushToList_bnil (A:k0): BushToList (bnil A) = nil(A:=A).
Proof.
  unfold BushToList.
  unfold bnil.
  rewrite BushM.MItRedCan.
  reflexivity.
Qed.

Lemma BushToList_bcons (A:k0)(a:A)(b:Bush (Bush A)): 
  BushToList (bcons a b) = a::flat_map(BushToList(A:=A))(BushToList b).
Proof.
  intros.
  unfold BushToList at 1.
  unfold bcons.
  rewrite BushM.MItRedCan.
  reflexivity.
Qed.
  
(* the more general cases *)
Lemma BushToList_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2): BushToList (bnil_  A ef n) = nil(A:=A).
Proof.
  intros.
  unfold BushToList.
  unfold bnil_.
  rewrite BushBase.MItRed.
  reflexivity.
Qed.

Lemma BushToList_bcons_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
   (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): 
       BushToList (bcons_ ef n a b) = 
                 a::flat_map ((BushToList(A:=A)) o (j A)) (BushToList (j _ b)).
Proof.
  intros.
  unfold BushToList at 1.
  unfold bcons_.
  rewrite BushBase.MItRed.
  reflexivity.
Qed.


Lemma BushToListNAT: NAT BushToList bush map.
Proof.
  unfold BushToList.
  apply BushM.MItNAT.
  red.
  intros.
  destruct t as [u|(a,b)]; simpl.
  reflexivity.
  f_equal.
  clear a.
  unfold moncomp.
  red in H.
  set (nflat:=flat_mapNAT H).
  unfold NAT in nflat.
  unfold moncomp in nflat.
  rewrite <- nflat.
  clear nflat.
  f_equal.
  induction ef. (* is really needed here *)
  rewrite H.
  reflexivity.
Qed.

Corollary BushToList_ok (A B: k0)(f:A->B)(t:Bush A):
  BushToList(bush f t) = map f (BushToList t).
Proof.
  intros.
  apply BushToListNAT.
Qed.

(* this is just to illustrate that BushM.MItNAT saves real work *)
Lemma BushToList_ok_manually (A B: k0)(f:A->B)(t:Bush A):
  BushToList(bush f t) = map f (BushToList t).
Proof.
  intros.
  generalize B f; clear B f.
  apply (BushBase.mu2Ind (fun A t =>  forall (B : Set) (f : A -> B), 
                               BushToList (bush f t) = map f (BushToList t))).
  clear A t.
  intros.
  destruct t as [u|(a,b)].
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n ).
  rewrite BushToList_bnil_.
  rewrite bush_bnil_.
  rewrite BushToList_bnil_.
  reflexivity.
(* bcons *)
  change (BushBase.In ef n (inr unit (a,b))) with (bcons_ ef n a b).
  rewrite BushToList_bcons_.
  rewrite bush_bcons_. (* has been proven through bush_bcons_ that
                                            needed a proof by induction on ef *)
  rewrite BushToList_bcons_.
  simpl map.
  f_equal.
  clear a.
  simpl.
  rewrite <- (flat_mapLaw1 (j B) (BushToList (A:=B))).
  rewrite flat_mapLaw2.
  rewrite n.
  rewrite H.
  rewrite map_map.
  rewrite flat_mapLaw1.
  apply flat_mapext.
  intro.
  unfold comp.
  rewrite <- H.
  rewrite n.
  reflexivity.
Qed.


Definition sizeIndirect : Bush c_k1 (fun _ => nat). 
Proof.
  red.
  intros.
  exact (length (BushToList H)).
Defined.

Theorem sizeIndirect_invariant (A B:k0)(f:A->B)(t:Bush A): sizeIndirect(bush f t) = sizeIndirect t.
Proof.
  intros.
  unfold sizeIndirect.
  rewrite BushToList_ok.
  rewrite map_length.
  reflexivity.
Qed.


Open Scope nat_scope.

Definition BushToValue: Bush c_k1 natCont.
Proof.
  refine (BushBase.MIt (fun (X:k1)(it: X c_k1 natCont)(A:Set)(t:BushF X A) => _)).
  destruct t as [u|(a,b)]; red; intro f.
  exact 0.
  exact (f a + it (X A) b (fun x => it A x f)).
Defined.

Definition sizeDirect:  Bush c_k1 (fun _ => nat). 
Proof.
  red.
  intros A t.
  exact (BushToValue t (fun _ => 1)).
Defined.


(* the behaviour of BushToValue on the general constructors *)
Lemma BushToValue_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2)(f:A->nat): BushToValue (bnil_  A ef n) f = 0.
Proof.
  intros.
  unfold BushToValue.
  unfold bnil_.
  rewrite BushBase.MItRed.
  reflexivity.
Qed.

Lemma BushToValue_bcons_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A))(f:A->nat): 
  BushToValue (bcons_ ef n a b) f = f a + BushToValue (j _ b) (fun x => BushToValue (j _ x) f).
Proof.
  intros.
  unfold BushToValue at 1.
  unfold bcons_.
  rewrite BushBase.MItRed.
  reflexivity.
Qed.


(* the following two lemmas are only necessary for a direct proof that sizeDirect 
    is invariant under bush *)
Lemma BushToValueExt (A:k0)(t:Bush A)(f g:A->nat):
  (forall a, f a = g a) -> BushToValue t f = BushToValue t g.
Proof.
  revert f g.
  apply (BushBase.mu2Ind (fun A t =>  
   forall f g : A -> nat,
      (forall a : A, f a = g a) -> BushToValue t f = BushToValue t g)).
  clear A t.
  intros.
  destruct t as [u|(a,b)].
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n ).
  do 2 rewrite BushToValue_bnil_.
  reflexivity.
(* bcons *)
  change (BushBase.In ef n (inr unit (a,b))) with (bcons_ ef n a b).
  do 2 rewrite BushToValue_bcons_.
  rewrite H0.
  f_equal.
  apply H.
  clear a b.
  intro.
  apply H.
  assumption.
Qed.

(* this is a pointwise formulation of naturality: *)
Lemma BushToValueNat (A B : k0) (f : A -> B) (t : Bush A)(g:B->nat):
  BushToValue (bush f t) g = BushToValue t (g o f).
(* the right-hand side is natCont_mon f (BushToValue t) g *)
Proof.
  intros.
  generalize B f g; clear B f g.
  apply (BushBase.mu2Ind (fun A t =>  
      forall (B : k0)(f : A -> B) (g : B -> nat),
            BushToValue (bush f t) g = BushToValue t (g o f))).
  clear A t.
  intros.
  destruct t as [u|(a,b)].
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n ).
  rewrite bush_bnil_.
  do 2 rewrite BushToValue_bnil_.
  reflexivity.
(* bcons *)
  change (BushBase.In ef n (inr unit (a,b))) with (bcons_ ef n a b).
  rewrite bush_bcons_.
  do 2 rewrite BushToValue_bcons_.
  f_equal.
  rewrite n.
  rewrite H.
  apply BushToValueExt.
  clear a b.
  intro.
  unfold comp at 1.
  rewrite <- H.
  rewrite n.
  reflexivity.
Qed.

Theorem sizeDirect_invariant (A B:k0)(f:A->B)(t:Bush A): sizeDirect(bush f t) = sizeDirect t.
Proof.
  intros.
  unfold sizeDirect.
  rewrite BushToValueNat.
  apply BushToValueExt.
  intro.
  reflexivity.
Qed.
(* we will later get an indirect proof, just by showing that sizeDirect and sizeIndirect coincide *)


Lemma values (A:k0)(t:Bush A)(f:A->nat): listToValue (BushToList t) f = BushToValue t f.
Proof.
  revert A t f.
  apply (BushBase.mu2Ind (fun A t =>  forall  (f : A -> nat), 
                  listToValue (BushToList t) f = BushToValue t f)).
  intros.
  destruct t as [u|(a,b)].
(* bnil *)
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n).
  rewrite BushToValue_bnil_.
  rewrite BushToList_bnil_.
  reflexivity.
(* bcons *)
  change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b).
  rewrite BushToValue_bcons_.
  rewrite BushToList_bcons_.
  simpl listToValue.
  f_equal.
  rewrite <- H.
  rewrite listToValueFlat_map.
  apply listToValueExt.
  clear a b.
  intro.
  unfold comp.
  apply H.
Qed.


Theorem size_ok (A:k0)(t:Bush A): sizeIndirect t = sizeDirect t.
Proof.
  intros.
  unfold sizeIndirect.
  unfold sizeDirect.
  rewrite listSize.
  apply values.
Qed.
  
Corollary sizeDirect_invariant_ALT (A B:k0)(f:A->B)(t:Bush A): 
         sizeDirect(bush f t) = sizeDirect t.
Proof.
  intros.
  do 2 rewrite <- size_ok.
  apply sizeIndirect_invariant.
Qed.


(** On canonization *)

Definition BushFmon2br: mon2br BushF.
Proof.
  red.  
  red.
  intros X Y mY f A t.
  destruct t as [u|(a,b)].
  unfold BushF.
  exact (inl _ u).
  unfold BushF.
  exact (inr _ (a, mY _ _ (f A) (f (X A) b))).
Defined.

Definition BushToCan: Bush c_k1 Bush := BushM.canonize BushFmon2br.

Lemma BushToCan_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2): BushToCan (bnil_  A ef n) = bnil A.
Proof.
  intros.
  unfold BushToCan.
  unfold BushM.canonize.
  unfold bnil_.
  rewrite BushBase.MItRed.
  unfold BushFmon2br.
  reflexivity.
Qed.

Lemma BushToCan_bcons_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): BushToCan(bcons_ ef n a b) =
                         bcons a (bush (BushToCan (A:=A) o j A) ((BushToCan (A:=G A) o j (G A)) b)).
Proof.
  intros.
  unfold BushToCan at 1.
  unfold BushM.canonize.
  unfold bcons_.
  rewrite BushBase.MItRed.
  unfold BushFmon2br at 1.
  reflexivity.
Qed.

Lemma BushToCan_bnil (A:k0): BushToCan (bnil A) = bnil A.
Proof.
  intros.
  rewrite bnilbnil_.
  rewrite BushToCan_bnil_.
  reflexivity.
Qed.

Lemma BushToCan_bcons (A:k0)(a:A)(b:Bush(Bush A)): BushToCan (bcons a b) = 
   bcons a (bush (BushToCan (A:=A)) (BushToCan b)).
Proof.
  intros.
  rewrite bconsbcons_.
  rewrite BushToCan_bcons_.
  rewrite BushM.mapmu2Comp.
  change (fun x : BushBase.mu2 A => x) with (id(A:=Bush A)).
  rewrite BushM.mapmu2Id.
  unfold comp.
  reflexivity.
Qed.


(* earlier approach: an inductive definition that does not take into account 
    non-canonical elements; the problem however is with inversion properties 
    that would be required for bush_elem *)
(*
Inductive elementInBush: forall (A:k0), A -> Bush A -> Prop :=
| elem1: forall (A:k0)(a:A)(b:Bush(Bush A)), elementInBush a (bcons a b)
| elem2: forall (A:k0)(a:A)(b:Bush(Bush A))(e:A)(t:Bush A), 
              elementInBush e t -> elementInBush t b -> elementInBush e (bcons a b).
*)

Definition elementInBush(A:k0)(a:A)(t:Bush A): Prop := In a (BushToList t).

Lemma elem1: forall (A:k0)(a:A)(b:Bush(Bush A)), elementInBush a (bcons a b).
Proof.
  intros.
  unfold elementInBush.
  rewrite BushToList_bcons.
  simpl.
  left.
  reflexivity.
Qed.

Lemma elem2: forall (A:k0)(a:A)(b:Bush(Bush A))(e:A)(t:Bush A), 
              elementInBush e t -> elementInBush t b -> elementInBush e (bcons a b).
Proof.
  unfold elementInBush.
  intros.
  rewrite BushToList_bcons.
  simpl.
  right.
  eapply (proj2 (in_flat_map (BushToList (A:=A)) (BushToList b) e)).
  exists t.
  split; assumption.
Qed.


Infix "elem" :=  elementInBush (at level 90).


(* Inductive definition of hereditarily canonical elements *)
Inductive canH : forall (A:k0), Bush A -> Prop :=
  | canH_bnil: forall(A:k0), canH (bnil A)
  | canH_bcons: forall (A:k0)(a:A)(b:Bush (Bush A)), 
        (forall t:Bush A, t elem b -> canH t) -> canH b -> canH(bcons a b).
(* this definition is effectively finitely branching since only finitely many t satisfy t elem b *)


(* the following lemma is restricted to canH t and therefore also works for the obsolete 
   inductive elem definition that does not care for non-canonical elements of Bush A *)
Lemma bushExt_refined (A B:k0)(f g:A->B)(t:Bush A):
  canH t -> (forall a, a elem t -> f a = g a) -> bush f t = bush g t.
Proof.
  intros.
  generalize B f g H0; clear B f g H0.
(* induction over being canonical: *)
  induction H; intros.
  do 2 rewrite bush_bnil.
  reflexivity.
  do 2 rewrite bush_bcons.
  assert (f a = g a).
  apply H2.
  apply elem1.
  rewrite H3.
  f_equal.
  apply IHcanH.
  intros.
  apply H0.
  assumption.
  intros.
  apply H2.
  exact (@elem2 A a b a1 a0 H5 H4). 
  (* explicit form of "exact" needed for compatibility with inductive def. of elem *)
Qed.

(* canonical elements are not changed by canonization *)  
Theorem BushToCan_invariant (A:k0)(t:Bush A): canH t -> BushToCan t = t.
Proof.
  intros.
  induction H.
  apply BushToCan_bnil.
  rewrite BushToCan_bcons.
  f_equal.
  change BushBase.mu2 with Bush.  (* hidden in implicit parameters *)
  rewrite IHcanH.
  transitivity (bush (id(A:=Bush A)) b).
  apply bushExt_refined.
  assumption.
  assumption.
  apply BushM.mapmu2Id.
Qed.

(* as an aside, we make use of our definition of elem that also takes into account
   non-canonical elements and try to prove a generalization of bushExt_refined to all bushes *)
(*
Lemma bushExt_refined_general_FAILS (A B:k0)(f g:A->B)(t:Bush A):
         (forall a, a elem t -> f a = g a) -> bush f t = bush g t.
Proof.
  intros.
  generalize B f g H; clear B f g H.
  apply (BushBase.mu2Ind (fun A t => forall (B : k0) (f g : A -> B),
               (forall a : A, (a elem t) -> f a = g a) -> bush f t = bush g t)).
  clear A t.
  intros.
  destruct t as [u|(a,b)].
(* bnil *)
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n).
  do 2 rewrite bush_bnil_.
  reflexivity.
(* bcons *)
  change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b).
  do 2 rewrite bush_bcons_.
  rewrite H0.
Focus 2.
  unfold elementInBush.
  change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b).
  rewrite BushToList_bcons_.
  simpl.
  left.
  reflexivity.
(* back *)
  apply (f_equal (fun x => bcons_ ef n (g a) x)).
(* how could we ever make use of H which is the induction hypothesis? *)  
  induction ef.
  simpl.
  simpl in n.
  apply e.
  intro.
  apply e.
(* now, we are completely stuck! *)
*)

(* the crucial auxiliary lemma which does not work with the inductive definition of elem *)
Lemma bush_elem (A B:k0)(f: A -> B)(t: Bush A)(b:B):
  b elem (bush f t) -> exists a:A, (a elem t) /\ (b = f a).
Proof.
  unfold elementInBush.
  intros.
  rewrite BushToList_ok in H.
  assert (exists a:A, f a =b /\ In a (BushToList t)).
  exact (proj1 (in_map_iff _ _ _) H).
  destruct H0.
  destruct H0.
  exists x.
  split.
  assumption.
  rewrite H0.
  reflexivity.
Qed.

(* preparation for the next lemma *)
Lemma bush_canH (A B:k0)(f: A -> B)(t: Bush A): canH t -> canH (bush f t).
Proof.
  intros.
  generalize B f; clear B f.
  induction H; intros.
(* bnil *)
  rewrite bush_bnil.
  apply canH_bnil.
(* bcons *)
  rewrite bush_bcons.
  apply canH_bcons.
Focus 2.
  apply IHcanH.
(* back *)
  intros.
  destruct (bush_elem (bush f) b t H2).
  destruct H3.
  rewrite H4.
  apply H0.
  assumption.
Qed.

(* canonization yields hereditarily canonical elements *)
Theorem BushToCanCanH (A:k0)(t:Bush A): canH (BushToCan t).
Proof.
  revert A t.
  apply (BushBase.mu2Ind (fun A t => canH (BushToCan t))).
  intros.
  destruct t as [u|(a,b)].
(* bnil *)
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n).
  rewrite BushToCan_bnil_.
  apply canH_bnil.
(* bcons *)
  change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b).
  rewrite BushToCan_bcons_.
  apply canH_bcons.
  intros.
  unfold comp at 2 in H0.
  destruct (bush_elem  (BushToCan (A:=A) o j A) _ t H0).
  destruct H1.
  rewrite H2.
  unfold comp.
  apply H.
  unfold comp at 2.
  apply bush_canH.
  apply H.
Qed.
(* we needed bush_elem and bush_canH *)
 
(* The usual corollary of these properties: BushToCan is idempotent *)
Corollary BushToCan_idempotent (A:k0)(t:Bush A):
  BushToCan(BushToCan t) = BushToCan t.
Proof.
  intros.
  apply BushToCan_invariant.
  apply BushToCanCanH.
Qed.


(* a preparation for the next lemma *)
Lemma BushToCanNAT: NAT BushToCan bush bush.
Proof.
  unfold BushToCan.
  unfold BushM.canonize.
  apply BushM.MItNAT.
  red.
  intros.
  destruct t as [u|(a,b)].
(* bnil *)
  simpl.
  induction u.
  change (BushM.InCan (inl (A * BushBase.mu2 (BushBase.mu2 A)) tt)) with (bnil A).
  rewrite bush_bnil.
  reflexivity.
(* bcons *)
  simpl.
  transitivity (bush f (bcons a (bush (it A) (it (X A) b)))).
  rewrite bush_bcons.
  unfold bcons.
  do 3 f_equal.
  unfold moncomp.
  rewrite H.
  do 2 rewrite <- BushM.mapmu2Comp.
  apply BushM.mapmu2Ext.
  clear a b.
  intro.
  unfold comp.
  rewrite <- H.
  induction ef.
  reflexivity.
  reflexivity.
Qed.

(* we also give a direct proof without the concept canH *)
Lemma BushToCan_idempotent_DIRECT (A:k0)(t:Bush A):
  BushToCan(BushToCan t) = BushToCan t.
Proof.
  revert A t.
  unfold BushToCan at 3.
  unfold BushM.canonize.
  apply BushM.MItUni.
(* alternatively, one could approach this by a direct inductive proof:
  apply (BushBase.mu2Ind (fun A t => BushToCan(BushToCan t) = BushToCan t)). *)
(* polyExtsub *)
  red.
  intros.
  destruct y as [u|(a,b)].
  reflexivity.
  simpl.
  do 3 f_equal.
  rewrite H.
  apply BushM.mapmu2Ext.
  apply H.
(* behaviour *)
  intros.
  destruct t as [u|(a,b)].
(* bnil *)
  induction u.
  change (BushBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n).
  rewrite BushToCan_bnil_.
  rewrite BushToCan_bnil.
  simpl.
  reflexivity.
(* bcons *)
  change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b).
  rewrite BushToCan_bcons_.
  rewrite BushToCan_bcons.
  simpl.
  unfold bcons.
  do 3 f_equal.
  unfold comp at 2 4.
  rewrite BushToCanNAT.
  rewrite <- BushM.mapmu2Comp.
  unfold comp.
  reflexivity.
Qed.

End Bush.