(** redecorationTYPES.v Version 1.0.1 December 2012 *) (** 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 version that does not use at all function induction: neither for zipWith nor redecL nor fromListRep. In the case of redecL, the lemma redecL_ind shows what has to be done manually if functional induction is not available. *) (* tested with V8.4pl1 of December 2012 *) (** Copyright 2006, 2007, 2012, 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. f_equal. 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. f_equal. 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. f_equal. 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 *) Fixpoint 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 f l1' l2' | nil, _ => nil | _, nil => nil end. 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. Fixpoint redecL_aux (A B:Set)(f:TriL A -> B)(t: TriL A)(n:nat){struct n}: TriL B := match n with | 0 => nil | S m => match t with | nil => nil | (es,a)::rest => (es,f((es,a)::rest)):: zipAppendEs (singletonTopEs rest) (redecL_aux f (removeTopEs rest) m) end end. (** redecoration in the list-based model *) Definition redecL (A B:Set)(f:TriL A -> B)(t: TriL A) : TriL B := redecL_aux f t (length t). (** the recursive equation for the composite case *) Lemma redecL_equation (A B:Set)(f:TriL A -> B)(es:list E)(a:A)(rest: TriL A): redecL f ((es,a)::rest) = (es,f((es,a)::rest)):: zipAppendEs (singletonTopEs rest) (redecL f (removeTopEs rest)). Proof. intros. unfold redecL. simpl. unfold removeTopEs at 3. rewrite map_length. reflexivity. Qed. (** inversion according to the list length *) Lemma length_aux1 (A:Set)(l:list A): length l = 0 -> l = nil. Proof. intros. induction l. reflexivity. simpl in H. inversion H. Qed. Lemma length_aux2 (A:Set)(l:list A)(n:nat): length l = S n -> exists a:A, exists l':list A, l = a::l'. Proof. intros. induction l. simpl in H. inversion H. simpl in H. inversion H. exists a. exists l. reflexivity. Qed. (** the induction principle that follows the recursive call pattern and incorporates the results *) Lemma redecL_ind (A B : Set) (f : TriL A -> B) (P : TriL A -> TriL B -> Prop): P nil nil -> (forall (es : list E) (a : A) (rest : list (list E * A)), P (removeTopEs rest) (redecL f (removeTopEs rest)) -> P ((es, a) :: rest) ((es, f ((es, a) :: rest)) :: zipAppendEs (singletonTopEs rest) (redecL f (removeTopEs rest)))) -> forall t : TriL A, P t (redecL f t). Proof. intros Hnil Hcons. assert (forall (n:nat)(t:TriL A), length t = n -> P t (redecL f t)). Focus 2. intro. apply (H (length t) t). reflexivity. (* back *) intro n. induction n. intros. assert (t=nil). rewrite (length_aux1 t H). reflexivity. rewrite H0. clear H0. unfold redecL. simpl. assumption. intros. assert (exists l, exists rest:TriL A, t = l::rest). apply (length_aux2 t H). destruct H0 as[l]. destruct H0 as [rest]. destruct l as [es a]. assert (length (removeTopEs rest) = n). rewrite H0 in H. inversion H. unfold removeTopEs. rewrite map_length. reflexivity. rewrite H0. clear H0. rewrite redecL_equation. apply (Hcons es a rest). apply (IHn _ H1). Qed. (** * 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 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:TrapL A) : shiftToEs(zipAppendEs l1 l2) = zipAppendEs l1 (shiftToEs l2). Proof. revert l2. induction l1. reflexivity. intro. destruct l2. reflexivity. simpl. unfold zipAppendEs at 1 in IHl1. rewrite IHl1. rewrite shiftToEappendEsComp. reflexivity. Qed. (** 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. 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. apply (redecL_ind (liftL f) (fun r res => shiftToEs res = zipAppendEs (singletonTopEs (shiftToEs r)) (redecL f (removeTopEs (shiftToEs r))))). intros. reflexivity. intros. 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). f_equal. Focus 2. unfold cutL. unfold remsh; unfold removeTopEs; unfold shiftToEs. rewrite map_map. reflexivity. (** back *) rewrite zipAppendEsShiftToEsComm. rewrite H. clear H. 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)). f_equal. 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. revert B f. induction t. reflexivity. intros. simpl. rewrite redecL_equation. f_equal. 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. 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. f_equal. 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.