(** redecorationTYPESfunindeverywhere.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 uses the Function command even for fromListRep that used to be a problem with most versions of Coq 8.1. *) (* 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. 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. (** 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 do not assume a fixed e0 throughout but keep it as an argument. *) Definition liftL (A B:Set)(e0:E)(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)(e0:E)(f : TriL A -> B)(r:Trap A) : lift (f o toListRep(A:=A)) r = liftL e0 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. 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. (** 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)(e0:E)(f:TriL A -> B)(r: TrapL A): shiftToEs (redecL (liftL e0 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 e0 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)(e0:E)(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. 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 e0 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 (e0:E)(A:Set)(p: list E * A) : list E * (E*A) := match p with (es,a) => (removelast es,(last es e0,a)) end. 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 (e0:E)(A:Set)(p: list E * (E*A)) : shiftFromE e0 (shiftToE p) = p. Proof. intros. destruct p. destruct p. destruct l. reflexivity. unfold shiftToE. unfold shiftFromE. rewrite removelastLemma. rewrite lastLemma. reflexivity. Qed. Definition shiftFromEs (e0:E)(A:Set): TriL A -> TrapL A := map (shiftFromE e0 (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 (e0:E)(A:Set)(r:TrapL A) : shiftFromEs e0 (shiftToEs r) = r. Proof. intros. unfold shiftFromEs. unfold shiftToEs. rewrite map_map. replace (map (fun x : list E * (E * A) => shiftFromE e0 (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. Definition meas (l:@sigT Set (fun A : Set => A * list (list E * A))) : nat := match l with existT _ (_, l) => length l end. Definition extract (x:{A : Set & A * list (list E * A)}) : Set := match x with existT A _ => A end. Definition build (A:Set) (p:A * TriL A) : {A : Set & A * list (list E * A)}. exists A. exact p. Defined. Function fromListRep_aux (e0:E)(x:{A : Set & A * list (list E * A)}) {measure meas x} : Tri (extract x) := match x as u return Tri (extract u) with | existT A p => match p with (a0,nil) => sg a0 | (a0, (es, a)::nil) => sg a | (a0, (es, a)::p::rest) => constr a (@fromListRep_aux e0 (build (A:=E*A) ((e0, a0) , shiftFromEs e0 (p::rest)))) end end. Proof. intros. simpl. unfold shiftFromEs. rewrite map_length. unfold lt. apply le_n. Defined. (* Coq V8.1pl3 yields the following error already with the Function definition: Error: refiner was given an argument "sg a0" of type "Tri A" instead of "Tri (extract x)" *) Definition fromListRep (e0:E)(A:Set)(a0:A)(t:TriL A) : Tri A := fromListRep_aux e0 (build (a0, t)). Lemma fromListRepNil (e0:E)(A:Set)(a0:A): fromListRep e0 a0 nil = sg a0. Proof. reflexivity. Qed. Lemma fromListRepSingle (e0:E)(A:Set)(a0:A)(es:list E)(a:A): fromListRep e0 a0 ((es, a)::nil) = sg a. Proof. reflexivity. Qed. Lemma fromListRepCons (e0:E)(A:Set)(a0:A)(es:list E)(a:A)(p:list E * A)(rest:TriL A): fromListRep e0 a0 ((es, a)::p::rest) = constr a (fromListRep e0 (e0, a0) (shiftFromEs e0 (p::rest))). Proof. intros. unfold fromListRep. rewrite fromListRep_aux_equation. simpl. 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). exists nil. reflexivity. simpl. exists (nil,a). exists (shiftToEs (toListRep t)). reflexivity. Qed. (** fromListRep is a left inverse to toListRep *) Lemma toFromListRepInv (e0:E)(A:Set)(a0:A)(t:Tri A): fromListRep e0 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)(e0:E)(a0:A)(b0:B)(f:Tri A -> B)(t: Tri A) : redec f t = fromListRep e0 b0 (redecL (f o (fromListRep e0 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. assumption. 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.