(** BushRecPred.v Version 1.0 January 2008 *)
(** does not need impredicative Set, runs under V8.1, tested with 8.1pl3, but also under V8.4, tested with 8.4pl1 *)
(** We illustrate how MRec allows a different definition of size but show that
    the new sizeRecursive and sizeIndirect agree on all arguments. *)

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

Set Implicit Arguments.

Require Import LNMItPred.
Require Import LNMRecPred.

Require Import BushPred.

Module Type BUSHRec := LNMRec_Type with Definition F:=BushF
                                                with Definition FpEFct := bushpEFct.


(** we base this on a hypothetical implementation of BUSHRec *)
Module BushRec (BushRecBase:BUSHRec).

Import BushRecBase.

Module BushRecDef := LNMRecDef BushRecBase.

Import BushRecDef.

Module BushBase := LNMItFromRec BushRecBase.

Module BushDef := LNMItPred.LNMItDef BushBase.

Module Bush := Bush BushBase.

Import Bush.

Require Import List.

(*
Print fold_right.
yields
fold_right = 
fun (A B : Type) (f : B -> A -> A) (a0 : A) =>
fix fold_right (l : list B) : A :=
  match l with
  | nil => a0
  | b :: t => f b (fold_right t)
  end
     : forall A B : Type, (B -> A -> A) -> A -> list B -> A
*)

Lemma sizeIndirect_bcons (A:k0)(a:A)(b:Bush(Bush A)):
  sizeIndirect (bcons a b) = 
             S (fold_right (fun x s => sizeIndirect x + s) 0 (BushToList b)).
Proof.
  intros.
  unfold sizeIndirect at 1.
  rewrite BushToList_bcons.
  simpl.
  f_equal.
  induction (BushToList b).
  reflexivity.
  simpl.
  rewrite app_length.
  rewrite IHl.
  reflexivity.
Qed.
  
Definition sizeRecursive : Bush c_k1 (fun A => nat). 
Proof.
  refine (MRec (fun (X:k1)(mX:mon X)(j: X c_k1 Bush)(rec: X c_k1 (fun A => nat))(A:Set)(t:BushF X A) => _)).
  destruct t as [u|(a,b)].
  exact 0.
  exact (S (fold_right (fun x s => rec _ x + s) 0 (BushToList (j _ b)))).
Defined.
(** note that we do not use the mX argument in this definition *)

(* the behaviour for the canonical constructors *)
Lemma sizeRecursive_bnil (A:k0): sizeRecursive (bnil A) = 0.
Proof.
  intros.
  unfold sizeRecursive.
  unfold bnil.
  rewrite MRecRedCan.
  reflexivity.
Qed.

Lemma sizeRecursive_bcons (A:k0)(a:A)(b:Bush(Bush A)): 
         sizeRecursive (bcons a b) = S (fold_right (fun x s => sizeRecursive x + s) 0 (BushToList b)).
Proof.
  intros.
  unfold sizeRecursive at 1.
  unfold bcons.
  rewrite MRecRedCan.
  reflexivity.
Qed.

(* now  the behaviour for the general constructors *)
Lemma sizeRecursive_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush)
    (n:NAT j (m ef) BushBase.mapmu2): sizeRecursive (bnil_  A ef n) = 0.
Proof.
  intros.
  unfold sizeRecursive.
  unfold bnil_.
  rewrite MRecRed.
  reflexivity.
Qed.

Lemma sizeRecursive_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)): 
          sizeRecursive (bcons_  ef n a b) = 
             S (fold_right (fun x s => (sizeRecursive(A:=A) o j A) x + s) 0 (BushToList (j _ b))).
Proof.
  intros.
  unfold sizeRecursive at 1.
  unfold bcons_.
  rewrite MRecRed.
  reflexivity.
Qed.

Lemma sizeRecursiveNAT: NAT sizeRecursive bush (fun A B f t => t).
Proof.
  unfold sizeRecursive.
  apply MRecNAT.
  red.
  intros.
  destruct t as [u|(a,b)]; simpl.
  reflexivity.
  f_equal.
  clear a.
  unfold moncomp.
  rewrite H.
  rewrite BushToListNAT.
(** here, we hide a little map fusion law for fold_right: *)
  induction (BushToList (j (X A) b)).
  reflexivity.
  simpl.
  induction ef. (* is really needed here *)
  simpl in H0.
  rewrite H0.
  rewrite IHl.
  reflexivity.
Qed.

Corollary sizeRecursive_invariant (A B: k0)(f:A->B)(t:Bush A):
  sizeRecursive(bush f t) = sizeRecursive t.
Proof.
  intros.
  apply sizeRecursiveNAT.
Qed.

(** sizeIndirect_bcons for the general constructor: sizeIndirect satisfies sizeRecursive_bcons_ with 
     sizeIndirect in place of sizeRecursive *)
Lemma sizeIndirect_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)): 
          sizeIndirect (bcons_  ef n a b) = 
             S (fold_right (fun x s => (sizeIndirect(A:=A) o j A) x + s) 0 (BushToList (j _ b))).
Proof.
  intros.
  unfold sizeIndirect.
  rewrite BushToList_bcons_.
  simpl.
  f_equal.
  induction (BushToList (j (G A) b)).
  reflexivity.
  simpl.
  rewrite app_length.
  rewrite IHl.
  reflexivity.
Qed.

(** the earlier lemma is now an instance *)
Corollary sizeIndirect_bconsALT (A:k0)(a:A)(b:Bush(Bush A)):
  sizeIndirect (bcons a b) = 
             S (fold_right (fun x s => sizeIndirect x + s) 0 (BushToList b)).
Proof.
  intros.
  rewrite bconsbcons_.
  rewrite sizeIndirect_bcons_.
  reflexivity.
Qed.


Theorem sizeRecursive_ok (A:k0)(t:Bush A): sizeRecursive t = sizeIndirect t.
Proof.
  intros.
  apply sym_eq.
  unfold sizeRecursive.
  apply (MRecUni(G:=fun A => nat)); clear A t.
(* extensionality *)
  red.
  intros.
  destruct y as [u|(a,b)]; simpl.
  reflexivity.
  f_equal.
(** here, we hide extensionality of fold_right *)
  induction (BushToList (j (X A) b)).
  reflexivity.
  simpl.
  rewrite H.
  rewrite IHl.
  reflexivity.
(* behaviour *)  
  intros.
  destruct t as [u|(a,b)]; simpl.
  induction u.
  change (LNMItBase.In ef n (inl (A * X (X A)) tt)) with (bnil_ A ef n).
  unfold sizeIndirect.
  rewrite BushToList_bnil_.
  reflexivity.
  change (LNMItBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b).
  apply sizeIndirect_bcons_.
Qed.


End BushRec.