(** redecorationTYPESfunind.v Version 1.0 December 2007 *)

(** This is companion material to the article "Verification of the Redecoration 
    Algorithm for Triangular Matrices" by Ralph Matthes and Martin Strecker in 
    the post-proceedings of TYPES 2007. *) 

(** This is the "official" version that is described in the article. It uses 
    the "old" functional induction for zipWith, the experimental functional
    induction for redecL and avoids functional induction for fromListRep. *)

(* can only work with Coq V8.1, tested with V8.1pl3 of December 2007, 
    does not work with V8.1pl2 *)

(** Copyright 2006, 2007, Ralph Matthes, CNRS & IRIT UPS Toulouse *)


Set Implicit Arguments.

Section TriangleDef.

Variable E:Set. (* fixed throughout *)

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

(** the datatype of triangles *)
Inductive Tri (A:Set) : Set :=
  sg : A -> Tri A
| constr : A -> Tri (E * A) -> Tri A.

Check Tri_ind : forall P : forall A : Set, Tri A -> Prop,
  (forall (A : Set) (a : A), P A (sg a)) ->
  (forall (A : Set) (a : A) (r : Tri (E * A)), P (E * A) r -> P A (constr a r)) ->
  forall (A : Set) (t : Tri A), P A t.

(** the datatype of trapeziums *)
Definition Trap (A:Set) := Tri (E * A).

Check constr : forall (A:Set), A -> Trap A -> Tri A.

(** the following specialisation of Tri_ind is not automatic *)
Lemma Trap_ind : forall P : forall A : Set, Trap A -> Prop,
  (forall (A : Set) (a : E*A), P A (sg a)) ->
  (forall (A : Set) (a : E*A) (r : Trap(E * A)), P (E * A) r -> P A (constr a r)) ->
  forall (A : Set) (t : Trap A), P A t.
Proof.
  refine (fix Trap_ind (P:forall A : Set, Trap A -> Prop)
  (Hyp1:forall (A : Set) (a : E*A), P A (sg a))
  (Hyp2:forall (A : Set) (a : E*A) (r : Trap(E * A)), 
        P (E * A) r -> P A (constr a r))
  (A:Set)(t:Trap A){struct t} : P A t :=
        match t return P A t with
           | sg a => _
           | constr a t' => _
        end).
  apply Hyp1.
  apply Hyp2.
  apply (Trap_ind P Hyp1 Hyp2).
Qed.


(** three more definitions before redec *)

Definition top (A:Set)(t:Tri A): A :=
  match t with
    | sg a => a
    | constr a _ => a
  end.

(** cutting off the top row *)
Fixpoint cut (A:Set)(t:Trap A){struct t} : Tri A :=
  match t with
     | sg (e,a) => sg a
     | constr (e,a) r => constr a (cut r)
  end.

Definition lift (A B:Set)(f:Tri A -> B)(r:Trap A) : E * B := (fst (top r), f(cut r)).

(** the short and elegant definition with the nested datatype *)
Fixpoint redec (A B:Set)(f:Tri A -> B)(t: Tri A){struct t} : Tri B :=
  match t with
     | sg a => sg (f(sg a))
     | constr a r => constr (f(constr a r)) (redec (lift f) r)
  end.


Lemma comonad1 (A B:Set)(f: Tri A -> B)(t:Tri A): top (redec f t) = f t.
Proof.
  intros.
  destruct t; reflexivity.
Qed.

Lemma auxcomonad2 (A:Set)(r:Trap A): lift (top(A:=A)) r = top r.
Proof.
  intros.
  destruct r; destruct p; reflexivity.
Qed.

(** redec only depends on the extension of its functional argument *)
Lemma redec_ext (A B:Set)(f f':Tri A -> B)(t:Tri A):
  (forall t':Tri A, f t' = f' t') -> redec f t = redec f' t.
Proof.
  intros.
  generalize B f f' H.
  clear B f f' H.
  induction t.
  simpl.
  intros.
  rewrite H.
  reflexivity.
  intros.
  simpl.
  rewrite H.
  apply (f_equal (fun x => constr (f'(constr a t)) x)).
  apply IHt.
  clear a t IHt.
  destruct t'.
  unfold lift.
  rewrite H.
  reflexivity.
  unfold lift.
  rewrite H.
  reflexivity.
Qed.

(* only now can the second comonad law be proven *)

Lemma comonad2 (A:Set)(t:Tri A): redec (top(A:=A)) t = t.
Proof.
  intros.
  induction t.
  reflexivity.
  simpl redec.
  apply (f_equal (fun x => constr a x)).
  replace (redec (lift (top(A:=A))) t) with (redec (top(A:=E*A)) t).
  assumption.
  apply redec_ext.
  clear a t IHt.
  intro.
  rewrite auxcomonad2.
  reflexivity.
Qed.


(** composition *)
Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x).
Infix "o" := comp (at level 90).


Lemma aux1comonad3 (A B:Set)(f:Tri A->B)(r:Trap A):
  redec f (cut r)=cut (redec (lift f) r).
Proof.
  intros.
  generalize B f; clear B f.
  induction r using Trap_ind.
  intros.
  destruct a.
  reflexivity.
  intros.
  destruct a.
  simpl.
  rewrite IHr.
  reflexivity.
Qed.


Lemma aux2comonad3 (A B C:Set)(f:Tri A->B)(g:Tri B->C)(r:Trap A):
  lift (g o redec f) r = (lift g o redec (lift f)) r.
Proof.
  intros.
  destruct r; destruct p.
  reflexivity.
  unfold comp at 1 2.
  unfold lift at 1 2.
  rewrite comonad1.
  simpl.
  rewrite aux1comonad3.
  reflexivity.
Qed.


Lemma comonad3 (A B C:Set)(f:Tri A->B)(g:Tri B->C)(t:Tri A): 
  redec (g o redec f) t = redec g (redec f t).
Proof.
  intros.
  generalize B C f g; clear B C f g.
  induction t.
  reflexivity.
  intros.
  simpl.
  unfold comp at 1.
  simpl redec at 1.
  apply (f_equal (fun x => 
     constr (g (constr (f (constr a t)) (redec (lift f) t))) x)).
  rewrite <- IHt.
  apply redec_ext.
  intro.
  rewrite aux2comonad3.
  reflexivity.  
Qed.  


(** * The List-Based Model *)

Require Import List.

(* the type transformer is "list", lists are built from "nil" and "::" (infix), and
   list concatenation is expressed by infix "++", the singleton lists [a] are
   only denoted by "a::nil" *)


(** Tri list based *)
Definition TriL (A:Set) := list (list E * A).


(** shift a diagonal component into the E part *)
Definition shiftToE (A:Set)(p: list E * (E*A)) : list E * A :=
  match p with (es,(e,a)) => (es++e::nil,a)
  end.

Definition shiftToEs (A:Set): TriL(E*A) -> TriL A :=
  map (shiftToE(A:=A)).


(** list representation of Tri *)
Fixpoint toListRep (A:Set)(t:Tri A) : TriL A :=
  match t with
     | sg a => (nil,a)::nil 
     | constr a r => (nil,a)::shiftToEs(toListRep r)
  end.

(* from the library:
tail = 
fun (A : Type) (l : list A) =>
match l with
| nil => nil (A:=A)
| _ :: m => m
end
     : forall A : Type, list A -> list A
*)

(** remove topmost E if present *)
Definition removeTopE(A:Set)(p: list E * A) : list E * A :=
  match p with (es, a) => (tail es, a) end.

(** output just the top E if it exists *)
Definition singletonTopE(A:Set)(p:list E * A) : list E :=
          match p with 
                          | (nil,a) => nil
                          | (e::es,a) => e::nil
                          end.

(** the means to append Es to a column *)
Definition appendEs (A:Set)(es:list E)(p:list E * A) : list E * A :=
  match p with (es',a) => (es++es',a) end.


Lemma appendEsLemma (A:Set)(p:list E * A):
   appendEs(singletonTopE p)(removeTopE p)=p.
Proof.
  intros.
  destruct p.
  destruct l; reflexivity.
Qed.  



(** according to zipWith of Haskell base Data.List *)
Function zipWith (A B C:Set)(f:A->B->C)(l1:list A)(l2:list B){struct l1} : list C :=
  match l1, l2 with
     | a::l1', b::l2' => f a b::@zipWith A B C f l1' l2'
     | nil, _ => nil
     | _, nil => nil
   end.
(** here, [Function] is used that generates an appropriate induction principle *)

Definition removeTopEs(A:Set)(r:TriL A) := 
    map (removeTopE(A:=A)) r.

Definition singletonTopEs(A:Set)(r:TriL A) := 
    map (singletonTopE(A:=A)) r.

(** append Es in all columns *)
Definition zipAppendEs (A:Set)(l1:list(list E))(l2:TriL A): TriL A :=
  zipWith (appendEs(A:=A)) l1 l2.

(** in order to show that the proof of  [zipAppendEsShiftToEsComm] does not depend on 
     the experimental extensions of functional induction, it is presented here and not only 
     just before [redecLMainLemma] where it would more naturally be placed *)

(** a preparation for the next lemma *)
Lemma shiftToEappendEsComp (A:Set)(a:list E)(b:list E * (E * A)) :
  shiftToE (appendEs a b) = appendEs a (shiftToE b).
Proof.
  intros.
  destruct b.
  destruct p.
  simpl.
  rewrite app_ass.
  reflexivity.
Qed.

Lemma zipAppendEsShiftToEsComm (A:Set)(l1:list(list E))(l2:TriL (E*A)) :
  shiftToEs(zipAppendEs l1 l2) = zipAppendEs l1 (shiftToEs l2).
Proof.
  intros.
  unfold zipAppendEs.
  unfold shiftToEs. 
(** do induction according to the recursive call structure *) 
  functional induction (zipWith (appendEs (A:=E * A)) l1 l2).
  simpl.
  rewrite IHl.
  rewrite shiftToEappendEsComp.
  reflexivity.
  reflexivity.
  destruct l1.
  destruct y.
  reflexivity.
Qed.



(** The following only work with the experimental extensions to functional induction. *)
Require Import Recdef.

Function redecL (A B:Set)(f:TriL A -> B)(t: TriL A)
                 {measure length t} : TriL B :=
  match t with nil => nil
      | (es,a)::rest => 
                    (es,f((es,a)::rest))::
                         zipAppendEs (singletonTopEs rest) (@redecL A B f (removeTopEs rest))
                     
  end. 
Proof.
  intros.
  unfold removeTopEs.
  rewrite map_length.
  simpl.
  auto.
Defined.
(** Note that the @ sign is needed to make functional induction work properly. *)


(** * The Verification *)

Definition TrapL (A:Set) := TriL(E*A).


Definition remsh(A:Set): list E * (E*A) -> list E * A := 
  removeTopE(A:=A) o shiftToE(A:=A).

(** the analogue of cut for list representations, see cutL_ok below *)
Definition cutL (A:Set): TrapL A -> TriL A :=
   map (remsh(A:=A)).

(** preparations for Lemma cutL_ok *)

(** If there are really Es, the order in the definition of remsh does not matter *)
Lemma remshEsComm (A:Set)(e:E)(es:list E)(p:E*A) :
  remsh (e::es,p) = shiftToE(removeTopE(e::es,p)).
Proof.
  intros.
  destruct p.
  reflexivity.
Qed.

(** shiftToE and remsh commute where they both exist*)
Lemma shiftToEremshComm (A:Set)(r:list E * (E * (E * A))) : 
  shiftToE (remsh r) = remsh (shiftToE r).
Proof.
  intros.
  unfold remsh at 1.
  destruct r.
  destruct p.
  simpl shiftToE at 2 3.
  destruct l.
  unfold app.
  rewrite remshEsComm.
  reflexivity.
  simpl app.
  rewrite remshEsComm.
  reflexivity.
Qed.
(* here, we preferred a proof that uses remshEsComm *)
(** This lemma will only be used in cutLmapShiftToEComm. *)

(** cutL commutes with shiftToEs *)
Lemma cutLShiftToEsComm (A:Set)(r:TrapL(E*A)) :
  shiftToEs(cutL r) = cutL (shiftToEs r).
Proof. 
  intros.
  unfold cutL.
  unfold shiftToEs.
  do 2 rewrite map_map. (* use functoriality of map *)
  refine (map_ext _ _ _ r).  (* use extensionality of map *)
(*  apply map_ext.    Did not work! Why?? *)
  apply shiftToEremshComm. 
Qed.
(** This lemma will only be used in the following soundness statement. *)

(** The following is Lemma 1 in the paper. *)
Lemma cutL_ok (A:Set)(r:Trap A) : toListRep (cut r) = cutL (toListRep r).
Proof.
  induction r using Trap_ind.
  destruct a.  
  reflexivity.
  destruct a.
  simpl.
  rewrite IHr.
  rewrite cutLShiftToEsComm.
  reflexivity.
Qed.


(** We assume a fixed e0:E throughout *)

Variable e0:E.

Definition liftL (A B:Set)(f : TriL A -> B)(r:TrapL A) : E * B :=
  (match head r with 
              | None => e0
              | Some x => fst(snd x) end, 
   f(cutL r)).

(** The following corresponds to Lemma 2 in the paper. *)
Lemma liftL_ok (A B:Set)(f : TriL A -> B)(r:Trap A) :
    lift (f o toListRep(A:=A)) r = liftL f (toListRep r).
Proof.
  intros.
  unfold liftL.
  rewrite <- cutL_ok.
  destruct r; reflexivity.
Qed.

(** now several preparatory lemmas for the proof of the Main Lemma *)

(** a simple consequence of the definition of cutL: *)
Lemma cutLShift (A:Set)(r:TrapL (E * A)) :
   cutL (shiftToEs r) = 
     map (fun x : list E * A => removeTopE x)
        (shiftToEs (shiftToEs r)).
Proof.
  intros.
  unfold cutL.
  unfold remsh.
  unfold shiftToEs.
  do 3 rewrite map_map.
  reflexivity.
Qed.


Lemma zipAppendEsComp (A B:Set)(f g: B-> list E)(t:list B)(u:TriL A) :
  zipAppendEs (map f t) (zipAppendEs (map g t) u) = 
      zipAppendEs (map (fun l => f l ++ g l) t) u.
Proof.
  intros.
  generalize u; clear u.
  induction t.
  reflexivity.
  intro.
  destruct u.
  reflexivity.
  destruct p.
  unfold zipAppendEs.
  simpl.
  rewrite app_ass.
  unfold zipAppendEs in IHt.  
  rewrite IHt.
  reflexivity.
Qed.

(** another simple observation *) 
Lemma singletonTopELemma (A:Set)(l:list E * (E * A)) :
  singletonTopE l ++ singletonTopE (shiftToE (removeTopE l)) = 
          singletonTopE (shiftToE l) ++ singletonTopE (removeTopE (shiftToE l)).
Proof.
  intros.
  destruct l.
  destruct p.
  destruct l; reflexivity.
Qed.

(** now, we will argue for redecL, using functional induction *)

Lemma redecLMainLemma (A B:Set)(f:TriL A -> B)(r: TrapL A): 
    shiftToEs (redecL (liftL  f) r) =
            zipAppendEs (singletonTopEs (shiftToEs r))
                       (redecL f (removeTopEs (shiftToEs r))).
Proof.
  intros.
(* functional induction allows to follow directly the recursive call structure *)
  functional induction (redecL (liftL f) r).
  reflexivity.
  destruct a.
(** good guessing needed for the following step: *)  
  replace (zipAppendEs (singletonTopEs (shiftToEs ((es, (e, a)) :: rest)))
  (redecL f (removeTopEs (shiftToEs ((es, (e, a)) :: rest))))) 
  with 
  ((es ++ e :: nil,
  f (remsh (es, (e, a)) :: removeTopEs (shiftToEs rest)))
  :: zipAppendEs (singletonTopEs (shiftToEs rest))
     (zipAppendEs
        (singletonTopEs (removeTopEs (shiftToEs rest)))
        (redecL f (removeTopEs (removeTopEs (shiftToEs rest)))))).
  simpl.
(** justify the replacement: *)
Focus 2.
  destruct es.
(** nil for es *)
  simpl.
  apply sym_eq.
  rewrite redecL_equation.
  reflexivity.
(** e1 :: es for es *)
  simpl.
  apply sym_eq.
  rewrite redecL_equation.
  reflexivity.
(** back *)
  replace (removeTopEs (shiftToEs rest)) with (cutL rest).
  apply (f_equal (fun x => (es ++ e :: nil, f (remsh (es, (e, a)) :: cutL rest))::x)).
Focus 2.
  unfold cutL.
  unfold remsh; unfold removeTopEs; unfold shiftToEs.
  rewrite map_map.
  reflexivity.
(** back *)
  rewrite zipAppendEsShiftToEsComm.
  rewrite IHt.
  clear IHt.
  unfold singletonTopEs.
  unfold removeTopEs at 1.
  unfold shiftToEs.
  unfold cutL.
  repeat rewrite map_map.
  repeat rewrite zipAppendEsComp.
  replace (removeTopEs (map (shiftToE (A:=A)) (removeTopEs rest))) with 
     (removeTopEs(map (remsh (A:=A)) rest)).
  apply (f_equal (fun x => 
     zipAppendEs x (redecL f (removeTopEs (map (remsh (A:=A)) rest))))).
  apply map_ext.
  intro.
  rewrite singletonTopELemma.
  reflexivity.
  unfold remsh.
  unfold removeTopEs.
  repeat rewrite map_map.
  apply map_ext.
  intro.
  fold (remsh a0).
  destruct a0.
  destruct l.
  destruct p.
  reflexivity.
  rewrite remshEsComm.
  reflexivity.
Qed.


(** Simulation *)
Lemma redecL_ok (A B:Set)(f:TriL A -> B)(t: Tri A) :
    toListRep (redec (fun x => f (toListRep x)) t) = redecL f (toListRep t).
Proof.
  intros A B f t.
  generalize B f; clear B f.
  induction t.
  reflexivity.
  intros.
  simpl.
  rewrite redecL_equation.
  apply (f_equal (fun x=> (nil(A:=E), f ((nil, a) :: shiftToEs (toListRep t)))::x)).
  replace (redec(lift (fun x => f (toListRep x))) t) with
              (redec(fun x: Trap A =>liftL f (toListRep x)) t).
Focus 2.
  apply redec_ext.
  intro.  
  apply sym_eq.
  change (fun x : Tri A => f (toListRep x)) with (f o toListRep(A:=A)).
  apply liftL_ok. 
(** back *) 
  rewrite IHt.
  clear a IHt.
  rewrite redecLMainLemma.
  reflexivity.
Qed.
(** This result is not yet in the form that allows to calculate redec through redecL. *)

(** left inverse operation to shiftToE *)
Definition shiftFromE (A:Set)(p: list E * A) : list E * (E*A) :=
  match p with (es,a) => (removelast es,(last es e0,a))
  end.

Lemma shiftFromENil (A:Set)(a:A):
  shiftFromE (nil(A:=E),a) = (nil(A:=E),(e0,a)).
Proof.
  reflexivity.
Qed.

Lemma shiftFromECons (e:E)(es:list E)(A:Set)(a:A):
  shiftFromE(e::es,a) = (removelast (e::es),(last (e::es) e0, a)).
Proof.
  reflexivity.
Qed.

Lemma removelastLemma (A:Set)(a:A)(l:list A):
  removelast (l++a::nil) = l.
Proof.
  intros.
  induction l.
  reflexivity.
  destruct l.
  reflexivity.
  simpl app.
  simpl removelast.
  simpl removelast in IHl.
  rewrite IHl.
  reflexivity.
Qed.  

Lemma lastLemma (A:Set)(a b:A)(l:list A):
  last (l++a::nil) b = a.
Proof.
  intros.
  induction l.
  reflexivity.
  simpl.
  destruct l.  
  reflexivity.
  assumption.
Qed.

(** shiftFromE is a left inverse to shiftToE *)
Lemma shiftToFromEInv (A:Set)(p: list E * (E*A)) :
  shiftFromE(shiftToE p) = p.
Proof.
  intros.
  destruct p.
  destruct p.
  destruct l.
  reflexivity.
  unfold shiftToE.
  unfold shiftFromE.
  rewrite removelastLemma.
  rewrite lastLemma.
  reflexivity.
Qed.

Definition shiftFromEs (A:Set): TriL A -> TrapL A :=
  map (shiftFromE(A:=A)).

(* the other functor law for map *)
Fact map_id: forall (A:Set)(l:list A), map (fun x => x) l = l.
Proof.
  intros.
  induction l; simpl; try rewrite IHl; try reflexivity.
Qed.

(** shiftFromEs is a left inverse to shiftToEs *)
Lemma shiftToFromEsInv (A:Set)(r:TrapL A) :
  shiftFromEs(shiftToEs r) = r.
Proof.
  intros.
  unfold shiftFromEs.
  unfold shiftToEs.
  rewrite map_map.
  replace (map (fun x : list E * (E * A) => shiftFromE(shiftToE x)) r) with (map (fun x : list E * (E * A)=>x) r).
  rewrite map_id; reflexivity.
  apply map_ext.
  intro; rewrite shiftToFromEInv; reflexivity.
Qed.


(** We need to work around a limitation of functional induction and therefore do structural
     recursion on the length of the list argument. In the following auxiliary function, the link
     between n and the list length is not yet manifest - as is usual with this approach *)
Fixpoint fromListRep_aux (A:Set)(a0:A)(l:list (list E * A))(n:nat)
                 {struct n} : Tri A  := 
    match n with 
      |      0 => sg a0
      | S m =>
          match l with 
           |                 nil => sg a0  (* dead code for fromListRep *)
           |  (es,a)::rest =>
                 match m with 
                    |      0 => sg a
                    | S m' => constr a (fromListRep_aux (e0, a0) (shiftFromEs rest) m)
                 end
          end
     end.

Definition  fromListRep (A:Set)(a0:A)(t:TriL A) : Tri A :=
   fromListRep_aux a0 t (length t).

Lemma fromListRepNil (A:Set)(a0:A):
  fromListRep a0 nil = sg a0.
Proof.
  reflexivity.
Qed.

Lemma fromListRepSingle (A:Set)(a0:A)(es:list E)(a:A):
  fromListRep a0 ((es, a)::nil) = sg a.
Proof.
  reflexivity.
Qed.

Lemma fromListRepCons (A:Set)(a0:A)(es:list E)(a:A)(p:list E * A)(rest:TriL A):
  fromListRep a0 ((es, a)::p::rest) = constr a (fromListRep (e0, a0) (shiftFromEs(p::rest))).
Proof.
  intros.
  unfold fromListRep.
  simpl.
  unfold shiftFromEs at 3 6.
  rewrite map_length.
  reflexivity.
Qed.


(** an auxiliary lemma *)
Lemma toListRepPair (A:Set)(t:Tri A):
  exists p:list E * A, exists rest: TriL A, toListRep t = p::rest.
Proof.
  intros.
  destruct t.
  simpl.
  exists (nil(A:=E),a).
  exists (nil(A:=list E * A)).
  reflexivity.
  simpl.
  exists (nil(A:=E),a).
  exists (shiftToEs (toListRep t)).
  reflexivity.
Qed.
  
(** fromListRep is a left inverse to toListRep *)
Lemma toFromListRepInv (A:Set)(a0:A)(t:Tri A):
  fromListRep a0 (toListRep t) = t.
Proof.
  intros.
  induction t.
(* sg *)
  simpl.
  apply  fromListRepSingle.
(* constr *)
  simpl.
  destruct (toListRepPair t).
  destruct H.
  rewrite H.
  simpl.
  rewrite fromListRepCons.
  apply (f_equal (fun x => constr a x)).
  change (shiftToE x :: shiftToEs x0) with (shiftToEs (x::x0)).
  rewrite shiftToFromEsInv.
  rewrite <- H.
  apply IHt.
Qed.

(** redec can be computed through redecL *)
Theorem MainTheorem (A B:Set)(a0:A)(b0:B)(f:Tri A -> B)(t: Tri A) :
    redec f t = fromListRep b0 (redecL (f o (fromListRep a0)) (toListRep t)).
(* f(sg a0) would be a way to obtain an element b0 of B *)
Proof.
  intros.
  rewrite <- redecL_ok.
  rewrite toFromListRepInv.
  apply redec_ext.
  intro.
  unfold comp.
  rewrite toFromListRepInv.
  reflexivity.
Qed.

  
End TriangleDef.

Section Test.

(** ** Tests after Andreas Abel's implementation in Haskell *)

Fixpoint sum' (A:Set)(f:A->nat)(t:Tri nat A){struct t} : nat :=
  match t with
     | sg a => f a
     | constr a r => f a + sum' (fun p:nat*A => fst p + f(snd p)) r
   end.

Definition sum (r:Tri nat nat) : nat := sum' (fun x=>x) r.


Definition t0 : Tri nat nat := sg _ 0.
Definition t1 := constr 0 (sg _ (1,2)).
Definition t2 := constr 0 (constr (1,2) (sg _ (3,(4,5)))).
Definition t3r := constr (1,2) (constr (3,(4,5)) (sg _ (6,(7,(8,9))))).
Definition t3 := constr 0 t3r.

Definition t01 := redec sum t0.
Definition t11 := redec sum t1.
Definition t21 := redec sum t2.
Definition t31 := redec sum t3.

Definition sumlist (l: list nat) : nat := fold_left plus l 0. 
Definition sumTriL (l:TriL nat nat) : nat := 
   fold_left (fun n (p:list nat * nat)=> n + sumlist (fst p) + snd p) l 0.

Eval compute in (sum t3).
(**
yields
    [= 45
     : nat]
*)
Eval compute in t21.
(**
yields 
     [= constr 15 (constr (1, 11) (sg nat (3, (4, 5))))
     : Tri nat nat]
*)
Eval compute in (toListRep t3).
(**
yields
     [= (nil, 0)
       :: (1 :: nil, 2)
          :: (3 :: 4 :: nil, 5) :: (6 :: 7 :: 8 :: nil, 9) :: nil
     : TriL nat nat]
*)
Eval compute in (toListRep t3r).
(**
yields
    [= (nil, (1, 2)) :: (3 :: nil, (4, 5)) :: (6 :: 7 :: nil, (8, 9)) :: nil
     : TriL nat (nat * nat)]
*)
Eval compute in (cut t3r).
(** 
yields
    [= constr 2 (constr (4, 5) (sg nat (7, (8, 9))))
     : Tri nat nat]
*)
Eval compute in (cutL (toListRep t3r)).
(** 
yields
    [= (nil, 2) :: (4 :: nil, 5) :: (7 :: 8 :: nil, 9) :: nil
     : TriL nat nat]
*)
Eval compute in (redecL sumTriL (toListRep t3)).
(**
yields
    [= (nil, 45)
       :: (1 :: nil, 35)
          :: (3 :: 4 :: nil, 22) :: (6 :: 7 :: 8 :: nil, 9) :: nil
     : TriL nat nat]
*)
Eval compute in (let t:=t3 in let f:=sumTriL in 
     toListRep (redec (fun x=>f(toListRep x)) t) = redecL f (toListRep t)).
(**
yields[
     = (nil, 45)
       :: (1 :: nil, 35)
          :: (3 :: 4 :: nil, 22) :: (6 :: 7 :: 8 :: nil, 9) :: nil =
       (nil, 45)
       :: (1 :: nil, 35)
          :: (3 :: 4 :: nil, 22) :: (6 :: 7 :: 8 :: nil, 9) :: nil
     : Prop]
*)

End Test.