(** Copyright 2006, 2007, 2012, Ralph Matthes, IRIT, CNRS & Univ. de Toulouse *) (** This is companion material to the article "A datastructure for Iterated Powers", presented at the conference MPC 2006. *) (** It has been tested with Coq V8.4 pl1 - just coqide/coqc with no options. *) (** If execution time seems too high, consider commenting out the lemmas that use the vernacular command [Time], in order of decreasing urgency for -towerBsh4OK -linBshOK -mkBsh3OK -mkTriBsh3_3ListOK Those lemmas only appear in the appendix and hence go beyond the material in the MPC article. *) Require Import List. Set Implicit Arguments. (** the universe of all monotypes *) Definition k0 := Set. (** the type of all type transformations *) Definition k1 := k0 -> k0. (* needed because of sort polymorphism *) Definition listk1 (A:k0) : k0 := list A. (** the identity type transformation *) Definition Id : k1 := fun X => X. (** iterating X n times *) Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= match k with 0 => Id | S k' => fun A => X (Pow X k' A) end. (** polymorphic identity *) Definition id : forall (A:k0), A -> A := fun A x => x. Section Bsh3. (** * Introduction: 3-Bushes over Ternary Trees *) (** 3-bushes and their constructors *) Variable Bsh3 : k1. Variable bnil3 : forall (A:k0), Bsh3 A. Variable bcons3: forall (A:k0), A -> Pow (Bsh3) 3 A -> Bsh3 A. (** ternary unlabelled finite trees *) Inductive Tri : k0 := L:Tri | N:Tri->Tri->Tri->Tri. Definition mkTriBsh3' : nat -> forall (A:k0), (Tri->A) -> Bsh3 A := fun m A f => (fix F (n:nat)(A:k0)(f:Tri->A) {struct n} : Bsh3 A := match n with 0 => bnil3 _ | S m => bcons3 (f L) (F m (Bsh3(Bsh3 A)) (fun t1 => F m (Bsh3 A) (fun t2 => (F m A (fun t3 => f(N t1 t2 t3)))))) end) m A f. (** the third argument runs the fastest *) Definition mkTriBsh3 (m:nat) := mkTriBsh3' m (id(A:=Tri)). Definition mkTriBsh3_3 := Eval compute in mkTriBsh3 3. (* Print mkTriBsh3_3. *) End Bsh3. (* Print mkTriBsh3_3. *) (** the pure kind of rank 2 *) Definition k2 := k1 -> k1. Definition less_k1 (X G:k1) : Type := forall (A B:k0), (A->B) -> X A -> G B. Infix "<_k1" := less_k1 (at level 60). Definition sub_k1 (X G:k1) : Type := forall A:k0, X A -> G A. Infix "c_k1" := sub_k1 (at level 60). (** Refined monotonicity for [k2] *) Definition mon2 (F:k2) : Type := forall (X G:k1), X <_k1 G -> F X <_k1 F G. (** ** Refined Conventional Iteration *) Module Type It_Eq_k1_Type. Parameter mu_k1: k2 -> k1. Parameter in_k1 : forall F:k2, F(mu_k1 F) c_k1 mu_k1 F. Parameter It_Eq_k1 : forall (G:k1)(F:k2), mon2 F -> F G c_k1 G -> mu_k1 F <_k1 G. Axiom It_Eq_k1_Reduction : forall (G:k1)(F:k2) (m:mon2 F)(s:F G c_k1 G)(A:k0)(B:k0) (f:A -> B)(t:F (mu_k1 F) A), It_Eq_k1 m s f (in_k1 _ _ t) = s _ (m _ _ (It_Eq_k1 m s) _ _ f t). End It_Eq_k1_Type. (** flattening lists, taken from [List.v] in the library *) Definition flatten : forall (A:k0), list(list A) -> list A := fun A => flat_map (id(A:=list A)). (** the usual rules for flatten hold in the strong form that both sides have the same normal form: *) Lemma flattenNil : forall (A:k0), flatten(A:=A) nil = nil. Proof. reflexivity. Qed. Lemma flattenCons: forall (A:k0)(a:list A)(l:list(list A)), flatten (a::l) = a ++ flatten l. (** ([++] is the usual list append) *) Proof. reflexivity. Qed. (** composition *) Definition comp (A B C:k0)(g:B->C)(f:A-> B) : A-> C := fun x => g (f x). Infix "o" := comp (at level 90). (** map is functorial; first law *) Fact mapid: forall (A:k0)(l:list A), map (id(A:=A)) l = l. Proof. intros. induction l. reflexivity. simpl. apply (f_equal (fun x => a :: x)). rewrite IHl. reflexivity. Qed. (** map is functorial; second law *) Lemma mapcomp: forall (A B C:k0)(g:B->C)(f:A->B)(l:list A), map (g o f) l = map g (map f l). Proof. intros. induction l. reflexivity. simpl. apply (f_equal (fun x=> g(f a) :: x)). rewrite IHl. reflexivity. Qed. (** map only depends on the extension of its first argument (clearly, one could restrict to the x's that occur in l) *) Lemma mapExt: forall (A B:k0)(f g:A->B)(l:list A), (forall x, f x = g x) -> map f l = map g l. Proof. intros. induction l. reflexivity. simpl. rewrite (H a). apply (f_equal (fun x => g a :: x)). rewrite IHl. reflexivity. Qed. (** a preparation for the naturality lemma *) Lemma mapappend: forall (A B:k0)(f:A->B)(l1 l2:list A), map f (l1++l2) = map f l1 ++ map f l2. Proof. intros. generalize l2. clear l2. induction l1. intro. reflexivity. intro. simpl. apply (f_equal (fun x=> f a :: x)). rewrite IHl1. reflexivity. Qed. (** naturality of flatten in the categorical sense *) Lemma mapflatten : forall (A B:k0)(f:A->B)(l:list (list A)), flatten(map(map f) l) = map f (flatten l). Proof. intros. induction l. reflexivity. simpl. rewrite IHl. unfold id. rewrite <- mapappend. reflexivity. Qed. (** ** Implementation *) (** we just take a parameter M of this module type *) Module Bsh3Mod(M:It_Eq_k1_Type). (** implementation of the 3-bushes *) Definition BshF3 : k2 := fun X A => (unit + A * (X (X (X A))))%type. Definition Bsh3 : k1 := M.mu_k1 BshF3. Definition bnil3 : forall (A:k0), Bsh3 A := fun A => M.in_k1 _ _ (inl _ tt : BshF3 Bsh3 A). Definition bcons3 : forall (A:k0), A -> Pow Bsh3 3 A -> Bsh3 A := fun A a b => M.in_k1 _ _ (inr _ (a, b) : BshF3 Bsh3 A). Definition bshf3: mon2 BshF3. Proof. do 2 red. intros G1 G2 e A B f r. elim r. intro. red. exact (inl _ a). intros [a r']. red. apply inr. split. exact (f a). apply (e (G1(G1 A))). apply (e (G1 A)). apply e. assumption. assumption. Defined. (** turning 3-bushes into lists, first the more general function *) Definition toListBsh3' : Bsh3 <_k1 listk1. Proof. refine(M.It_Eq_k1 bshf3 (fun A t => _)). case t. intro. exact nil. intros [a b]. apply (cons a). exact (flatten(flatten b)). Defined. Lemma toListBsh3'Red1 : forall (A B:k0)(f:A->B), toListBsh3' f (bnil3 _) = nil. Proof. intros. unfold toListBsh3'. unfold bnil3. rewrite M.It_Eq_k1_Reduction. reflexivity. Qed. Lemma toListBsh3'Red2 : let toL:=toListBsh3' in forall (A B:k0)(f:A->B)(a:A)(b:Pow Bsh3 3 A), toL _ _ f (bcons3 a b) = f a :: flatten(flatten(toL _ _ (toL _ _ (toL _ _ f))b)). Proof. intros. unfold toL at 1. unfold toListBsh3'. unfold bcons3. rewrite M.It_Eq_k1_Reduction. reflexivity. Qed. Definition toListBsh3 : Bsh3 c_k1 listk1 := fun A => toListBsh3' (id(A:=A)). (** the example list *) Definition mkTriBsh3_3List := toListBsh3(mkTriBsh3_3 Bsh3 bnil3 bcons3). Lemma mkTriBsh3_3ListOK : mkTriBsh3_3List = L :: N L L L :: N L L (N L L L) :: N L (N L L L) L :: N L (N L L L) (N L L L) :: N (N L L L) L L :: N (N L L L) L (N L L L) :: N (N L L L) (N L L L) L :: N (N L L L) (N L L L) (N L L L) :: nil. Proof. unfold mkTriBsh3_3List. unfold toListBsh3. unfold mkTriBsh3_3. Time repeat ((rewrite toListBsh3'Red1||rewrite toListBsh3'Red2)). (* unfold flatten. simpl. *) reflexivity. Qed. (** the brute-force alternative to the above proof: [ compute. Time repeat rewrite M.It_Eq_k1_Reduction. reflexivity. Qed.] *) Fixpoint Iter(A:Type)(a:A)(s:A->A)(m:nat){struct m}:A := match m with 0 => a | S m' => s (Iter a s m') end. Definition aB(A:k0)(f:Tri->A): Bsh3 A := bnil3 A. Definition sB(v:forall A:k0,(Tri->A)->Bsh3 A)(A:k0)(f:Tri->A): Bsh3 A := bcons3 (f L) (v _ (fun t1 => v _ (fun t2 => (v _ (fun t3 => f(N t1 t2 t3)))))). Lemma mkTriBsh3'ext : forall (m:nat)(A:k0)(f f':Tri->A), (forall x, f x=f' x) -> mkTriBsh3' Bsh3 bnil3 bcons3 m f = mkTriBsh3' Bsh3 bnil3 bcons3 m f'. Proof. intro m. induction m. reflexivity. intros. simpl. rewrite H. apply (f_equal (fun x=> bcons3 (f' L) x)). simpl. apply IHm. intro. apply IHm. intro. apply IHm. intro. apply H. Qed. Lemma aBsBOk : forall (m:nat)(A:k0)(f:Tri->A), mkTriBsh3' Bsh3 bnil3 bcons3 m f = Iter aB sB m A f. Proof. intro m. induction m. reflexivity. intros. simpl. unfold sB at 1. apply (f_equal (fun x=> bcons3 (f L) x)). replace (mkTriBsh3' Bsh3 bnil3 bcons3 m (fun t1 : Tri => mkTriBsh3' Bsh3 bnil3 bcons3 m (fun t2 : Tri => mkTriBsh3' Bsh3 bnil3 bcons3 m (fun t3 : Tri => f (N t1 t2 t3))))) with (mkTriBsh3' Bsh3 bnil3 bcons3 m(fun t1 : Tri => Iter aB sB m (Bsh3 A) (fun t2 : Tri => Iter aB sB m A (fun t3 : Tri => f (N t1 t2 t3))))). rewrite IHm. reflexivity. apply mkTriBsh3'ext. intro. replace (Iter aB sB m (Bsh3 A) (fun t2 : Tri => Iter aB sB m A (fun t3 : Tri => f (N x t2 t3)))) with (mkTriBsh3' Bsh3 bnil3 bcons3 m (fun t2 : Tri => Iter aB sB m A (fun t3 : Tri => f (N x t2 t3)))). apply mkTriBsh3'ext. intro. rewrite IHm. reflexivity. rewrite IHm. reflexivity. Qed. Definition aL : list Tri := nil (A:=Tri). Definition sL(l:list Tri) : list Tri := L::flatten(flatten(map(fun t1=>map(fun t2=>map(fun t3=>N t1 t2 t3) l) l) l)). Definition mkTriList : nat -> list Tri := Iter aL sL. Eval compute in (mkTriList 3). Lemma fusion: forall (A A':Type)(a:A)(a':A')(s:A->A)(s':A'->A')(f:A->A'), a' = f a -> (forall x:A, s'(f x) = f(s x)) -> forall m:nat, f(Iter a s m) = Iter a' s' m. Proof. intros. induction m. simpl. apply sym_eq. assumption. simpl. rewrite <- IHm. apply sym_eq. apply H0. Qed. Definition mkTriListMap(m:nat)(A:k0)(f:Tri->A) : list A := map f (mkTriList m). Definition map' (l:list Tri)(A:k0)(f:Tri -> A) : list A := map f l. Definition aM(A:k0)(f:Tri->A): list A := nil (A:=A). Definition sM(v: forall A:k0,(Tri -> A) -> list A)(A:k0)(f:Tri->A) : list A := f L::flatten(flatten(v _ (fun t1 => v _ (fun t2=> v _ (fun t3 =>f(N t1 t2 t3)))))). Lemma sMext : forall (v v':forall A:k0,(Tri -> A) -> list A), (forall (A:k0)(f f':Tri->A), (forall x, f x = f' x) -> v _ f = v _ f') -> (forall (A:k0)(f:Tri->A), v _ f = v' _ f) -> forall (A:k0)(f:Tri->A), sM v f = sM v' f. Proof. intros. unfold sM. apply (f_equal (fun x => f L::flatten(flatten x))). replace (v (list (list A)) (fun t1 : Tri => v (list A) (fun t2 : Tri => v A (fun t3 : Tri => f (N t1 t2 t3))))) with (v (list (list A)) (fun t1 : Tri => v' (list A) (fun t2 : Tri => v' A (fun t3 : Tri => f (N t1 t2 t3))))). apply H0. apply H. intro. replace (v (list A) (fun t2 : Tri => v A (fun t3 : Tri => f (N x t2 t3)))) with (v (list A) (fun t2 : Tri => v' A (fun t3 : Tri => f (N x t2 t3)))). apply sym_eq. apply H0. apply H. intro. apply sym_eq. apply H0. Qed. Lemma sMOk : forall (A:k0)(f:Tri -> A)(l:list Tri), sM (fun A f => map f l) f = map f (sL l). Proof. intros. unfold sL. simpl map. unfold sM. rewrite <- mapflatten. rewrite <- mapflatten. apply (f_equal (fun x => f L::flatten (flatten x))). rewrite <- mapcomp. unfold comp. apply mapExt. intro. rewrite <- mapcomp. unfold comp. apply mapExt. intro. rewrite <- mapcomp. unfold comp. reflexivity. Qed. Lemma IteraMsMext : forall (m:nat)(A:k0)(f f':Tri->A), (forall x, f x = f' x) -> Iter aM sM m _ f = Iter aM sM m _ f'. Proof. intro m. induction m. reflexivity. intros. simpl. unfold sM at 1 3. rewrite H. apply (f_equal (fun x => f' L::flatten (flatten x))). apply IHm. intro. apply IHm. intro. apply IHm. intro. apply H. Qed. Lemma mapCons : forall (A B:k0)(f:A->B)(a:A)(l:list A), map f (a::l) = f a :: map f l. Proof. reflexivity. Qed. Lemma mkTriListMapOk: forall (m:nat)(A:k0)(f:Tri->A), mkTriListMap m f = Iter aM sM m _ f. Proof. intro m. induction m. reflexivity. intros. unfold mkTriListMap. simpl. rewrite <- mapCons. fold (sL (Iter aL sL m)). rewrite <- sMOk. apply sMext. intros. apply mapExt. assumption. apply IHm. Qed. (** Note that a direct application of the fusion rule is impossible since we only have our assumptions fulfilled pointwise. *) Lemma mkTriBsh3'Ok : forall (m:nat)(A B:k0)(f:Tri->A)(g:A->B), toListBsh3' g (mkTriBsh3' Bsh3 bnil3 bcons3 m f) = Iter aM sM m _ (g o f). Proof. intro m. induction m. intros. simpl. rewrite toListBsh3'Red1. reflexivity. (** S m *) intros. simpl. rewrite toListBsh3'Red2. unfold comp at 1. unfold sM at 1. apply (f_equal (fun x => g(f L) :: flatten(flatten x))). rewrite IHm. unfold comp at 1. apply IteraMsMext. intro. rewrite IHm. unfold comp at 1. apply IteraMsMext. intro. rewrite IHm. reflexivity. Qed. End Bsh3Mod. (** * n-Bushes *) Module BshnMod(M:It_Eq_k1_Type). Module M3 := Bsh3Mod M. Section Bshn. (** the fixed parameter n *) Variable n:nat. (** n-bushes *) Definition BshF : k2 := fun X A => (unit + A * Pow X n A)%type. Definition Bsh : k1 := M.mu_k1 BshF. (** first constructor *) Definition bnil : forall (A:k0), Bsh A := fun A => M.in_k1 _ _ (inl _ tt : BshF Bsh A). (** second constructor *) Definition bcons : forall (A:k0), A -> Pow Bsh n A -> Bsh A := fun A a b => M.in_k1 _ _ (inr _ (a, b) : BshF Bsh A). (** ** From n-Bushes to Lists *) (** k times iterated flattening *) Fixpoint flat (k:nat) : forall (A:k0), Pow listk1 k A -> list A := match k return forall (A:k0), Pow listk1 k A -> list A with 0 => fun _ a => a::nil | S k' => fun _ l => flatten (map (flat k' _) l) end. Fixpoint POW (k:nat)(X G:k1)(i:X<_k1 G){struct k} : Pow X k<_k1 Pow G k := match k return Pow X k<_k1 Pow G k with 0 => fun _ _ f => f | S k' => fun _ _ f => i _ _ (POW k' i f) end. Definition bshf: mon2 BshF. Proof. do 2 red. intros X G i A B f t. elim t. intro u. red. exact (inl _ u). intros [a b]. red. apply inr. split. exact (f a). exact (POW n i f b). Defined. Definition toListBsh' : Bsh <_k1 listk1 := M.It_Eq_k1 bshf (fun (A : k0) (t : BshF listk1 A) => match t with | inl _ => nil (A:=A) | inr p => let (a, b) := p in a :: flat n A b end). (** for comparison: how it would be defined interactively *) Definition toListBsh'interactive : Bsh <_k1 listk1. Proof. refine(M.It_Eq_k1 bshf (fun A t => _)). case t. intro. exact nil. intros [a b]. apply (cons a). exact (flat n _ b). Defined. Lemma toListBsh'Red1 : forall (A B:k0)(f:A->B), toListBsh' f (bnil _) = nil. Proof. intros. unfold toListBsh'. unfold bnil. rewrite M.It_Eq_k1_Reduction. reflexivity. Qed. Lemma toListBsh'Red2 : forall (A B:k0)(f:A->B)(a:A)(b:Pow Bsh n A), toListBsh' f (bcons a b) = f a :: flat n _ (POW n toListBsh' f b). Proof. intros. unfold toListBsh' at 1. unfold bcons. rewrite M.It_Eq_k1_Reduction. reflexivity. Qed. (** our interpretation of n-bushes as lists *) Definition toListBsh : Bsh c_k1 listk1 := fun _ => toListBsh' (id(A:=_)). (** * Programming the n-Bushes *) Require Vector. (* Print Vector.t. *) (* Check @Vector.hd : forall (A : Set) (n : nat), Vector.t A (S n) -> A. Check @Vector.tl : forall (A : Set) (n : nat), Vector.t A (S n) -> Vector.t A n. *) Inductive Tree: k0 := L' : Tree | N' : Vector.t Tree n -> Tree. Definition vec (k:nat) := Vector.t Tree k. Definition vnil : vec 0 := Vector.nil Tree. Definition vcons (t:Tree)(k:nat) : vec k -> vec (S k) := Vector.cons Tree t k. Fixpoint LL(l:list Tree)(k:nat){struct k} : (vec k->Tree) -> Pow listk1 k Tree := match k return (vec k->Tree) -> Pow listk1 k Tree with 0 => fun f => f vnil | S k' => fun f => map (fun t => LL l (f o (vcons t (k:=k')))) l end. Definition aLn : list Tree := nil (A:=Tree). Definition sLn (l:list Tree) : list Tree := L'::flat n _ (LL l N'). Definition mkTriListn : nat -> list Tree := M3.Iter aLn sLn. Fixpoint BB (v:forall A:k0, (Tree ->A) -> Bsh A)(k:nat)(A:k0){struct k}: (vec k -> A) -> Pow Bsh k A := match k return (vec k -> A) -> Pow Bsh k A with 0 => fun f => f vnil | S k' => fun f => v (Pow Bsh k' A)(fun t => BB v (f o (vcons t (k:=k')))) end. Definition aBn (A:k0)(f:Tree -> A) : Bsh A := bnil _. Definition sBn (v:forall A:k0, (Tree ->A) -> Bsh A)(A:k0)(f:Tree -> A) : Bsh A := bcons (f L') (BB v (f o N')). Definition mkTreeBsh': nat -> forall A:k0, (Tree -> A) -> Bsh A := M3.Iter aBn sBn. Definition mkTreeBsh (m:nat) : Bsh Tree := mkTreeBsh' m (fun x=>x). Definition T (m:nat) : Prop := forall (A B:k0)(f:Tree->A)(g:A->B), toListBsh' g (mkTreeBsh' m f) = map (g o f) (mkTriListn m). Definition P (m k:nat) : Prop := forall (A B : k0) (f0:vec k->Tree) (f : Tree -> A) (g : A -> B), flat k B (POW k toListBsh' g (BB (mkTreeBsh' m) (f o f0))) = map (g o f) (flat k Tree (LL (mkTriListn m) f0)). (** the more concrete statement is a corollary to T *) Lemma ThmImpTheorem : forall (m:nat), T m -> toListBsh (mkTreeBsh m) = mkTriListn m. Proof. intros. unfold toListBsh. unfold mkTreeBsh. rewrite H. unfold comp. change (fun x : Tree => id x) with (id(A:=Tree)). exact (mapid _). Qed. Lemma ThmImpProp : forall (m:nat), T m -> forall (k:nat), P m k. Proof. intros m Tm k. induction k. red. reflexivity. red. intros. simpl. (* rewrite (Tm _ _ (fun t : Tree => BB (mkTreeBsh' m) ((f o f0) o (vcons t (k:=k)))) (POW k toListBsh' g)). *) rewrite Tm. rewrite <- mapcomp. unfold comp at 1 2. replace (map (fun x : Tree => flat k B (POW k toListBsh' g (BB (mkTreeBsh' m) ((f o f0) o (vcons x (k:=k)))))) (mkTriListn m)) with (map (fun x : Tree => map (g o f) (flat k Tree (LL (mkTriListn m) (f0 o (vcons x (k:=k))))) ) (mkTriListn m)). Focus 2. apply mapExt. intro. change ((f o f0) o (vcons x (k:=k))) with (f o (f0 o (vcons x (k:=k)))). rewrite IHk. reflexivity. (** back *) rewrite <- mapcomp. rewrite <- mapflatten. rewrite <- mapcomp. reflexivity. Qed. Lemma Main : forall m, T m. Proof. induction m. red. intros. unfold mkTreeBsh'. simpl. unfold aBn. rewrite toListBsh'Red1. reflexivity. (** S m *) red. intros. unfold mkTreeBsh'. simpl. unfold sBn. rewrite toListBsh'Red2. unfold comp at 3. apply (f_equal (fun x => g(f L'):: x)). apply (ThmImpProp IHm). Qed. End Bshn. Definition N'alt(t1 t2 t3:Tree 3): Tree 3 := N' (vcons t1 (vcons t2 (vcons t3 (vnil 3)))). Lemma sLn3Ok : sLn (n:=3) = fun l:list (Tree 3) => L' 3:: flat 3 _ (map (fun t1 => map (fun t2 => map (fun t3 => N'alt t1 t2 t3)l)l)l). Proof. reflexivity. Qed. Lemma sBn3Ok : sBn (n:=3) = fun (v:forall A : k0, (Tree 3 -> A) -> Bsh 3 A) (A:k0)(f:Tree 3-> A) => bcons 3 (f (L' 3))(v _ (fun t1 => v _ (fun t2 => v _ (fun t3 => f(N'alt t1 t2 t3))))). Proof. reflexivity. Qed. (** * A P P E N D I X *) (** ** Towerbushes *) Section Tower. Require Import Plus. Require Import Mult. (** This development has been described in the first submitted version of the MPC '06 article. Here, we define elements of Bsh n nat that contain precisely the elements 0, 1,..., powerplus m n -1. This is the number of n-ary trees of height less than m, but here we directly work with natural numbers. *) Variable n:nat. (** the crucial auxiliary function for defining towerbushes *) Fixpoint FF (F:forall (A:k0), (nat -> A) -> Bsh n A)(k:nat){struct k} : forall (A:k0),(nat->A)->nat->nat-> Pow (Bsh n) k A := match k return forall (A:k0),(nat->A)->nat->nat-> Pow (Bsh n) k A with 0 => fun _ f t off => f (S off) | S k' => fun _ f t off => F _ (fun x => FF F k' f t (off * t + x)) end. (** exponentiation x^k *) Fixpoint pow (k:nat)(x:nat) {struct k} : nat := match k with 0 => 1 | S k' => x * pow k' x end. (** iterated exponentiation with exponent n plus 1 *) Fixpoint powerplus (m:nat) : nat := match m with 0 => 0 | S m' => S (pow n (powerplus m')) end. Notation "# m" := (powerplus m) (at level 0, m at level 0). (** the desired function, first more generally with a function argument f that changes during the recursion in FF *) Fixpoint towerBsh' (m:nat) : forall (A:k0), (nat -> A) -> Bsh n A := match m return forall (A:k0), (nat -> A) -> Bsh n A with | 0 => fun _ _ => bnil n _ | S m' => fun _ f => bcons n (f 0) (FF (towerBsh' m') n f (# m') 0) end. (** the n-bush with [# m] elements, from 0 onwards numbered *) Definition towerBsh (m:nat) : Bsh n nat := towerBsh' m (id(A:=_)). (** ** Verification *) (** list of i numbers from x onwards *) Fixpoint count (x i:nat){struct i} : list nat := match i with 0 => nil | S i' => x::count (S x) i' end. (** list of first i numbers *) Definition first (i:nat) := count 0 i. (** a simple observation *) Fact appendCount : forall (a b c:nat), (count a b) ++ (count (a+b) c) = count a (b+c). Proof. intros. generalize a. clear a. induction b. intro a. rewrite plus_0_r. reflexivity. (** S b *) intro a. simpl. apply (f_equal (fun x => a :: x)). rewrite <- IHb. apply (f_equal (fun x => count(S a)b ++ x)). rewrite plus_Snm_nSm. reflexivity. Qed. (** the crucial combinatorial lemma for the verification *) Lemma flattenCount : forall (a b c d:nat), flatten(map (fun x => count (a+x*b) b) (count c d)) = count (a+c*b)(b*d). Proof. intros. generalize c. clear c. induction d. intro. simpl. rewrite mult_0_r. reflexivity. (** S d *) intro. simpl. rewrite IHd. rewrite <- mult_n_Sm. rewrite (plus_comm (b*d) b). rewrite <- appendCount. apply (f_equal (fun x => count(a+c*b)b ++ x)). simpl. rewrite <- plus_assoc. rewrite (plus_comm (c*b) b). reflexivity. Qed. (** Here, we parallel the proof structure for mkTreeBsh'. *) (** the theorem as a definition of a statement *) Definition T' (m:nat) : Prop := forall (A B:k0)(f:nat->A)(g:A->B), toListBsh' g (towerBsh' m f) = map (g o f) (first (# m)). (** the more concrete statement is a corollary to T' *) Lemma ThmImpTheorem' : forall (m:nat), T' m -> toListBsh (towerBsh m) = first (# m). Proof. intros. unfold toListBsh. unfold towerBsh. rewrite H. unfold id. unfold comp. rewrite (mapid(A:=nat)). reflexivity. Qed. (** the proposition as a definition of a statement *) Definition P' (m k:nat) : Prop := forall (A B:k0)(f:nat->A)(g:A->B)(off:nat), flat k _ (POW k (toListBsh'(n:=n)) g (FF (towerBsh' m) k f (# m) off)) = map (g o f) (let num := pow k (# m) in count (S(off*num)) num). (** at stage m, the theorem implies the proposition *) Lemma ThmImpProp' : forall (m:nat), T' m -> forall (k:nat), P' m k. Proof. intros m Tm k. induction k. (** 0 *) red. intros. simpl. apply (f_equal (fun x => x :: nil(A:=B))). rewrite mult_1_r. reflexivity. (** S k *) red. intros. simpl. rewrite Tm. rewrite <- mapcomp. unfold comp at 1 2. simpl. replace (map (fun x : nat => flat k B (POW k (toListBsh'(n:=n)) g (FF (towerBsh' m) k f #m (off * #m + x)))) (first #m)) with (map (fun x : nat => map (g o f) (let num := pow k (# m) in count (S((off * (# m) + x)*num)) num))(first (# m))). (** first justify the replacement *) Focus 2. apply mapExt. intro. simpl. rewrite IHk. apply (f_equal(map(g o f))). reflexivity. (** back to the main proof *) change (fun x : nat => map (g o f) (let num := pow k (# m) in count (S ((off * (# m) + x) * num)) num)) with ((map (g o f)) o (fun x : nat =>let num := pow k (# m) in count (S ((off * (# m) + x) * num)) num)). rewrite mapcomp. rewrite mapflatten. apply (f_equal(map(g o f))). unfold first. replace (map (fun x : nat => count (S ((off * (# m) + x) * (pow k (# m)))) (pow k (# m)) ) (count 0 (# m))) with (map (fun x : nat => count (S (off * (# m * (pow k (# m)))) + x * (pow k (# m))) (pow k (# m)) ) (count 0 (# m))). rewrite flattenCount. (** How can the remainder be automatized? *) apply (f_equal2 count). rewrite (mult_comm (# m)(pow k (# m))). simpl. apply (f_equal S). rewrite plus_0_r. reflexivity. rewrite mult_comm. reflexivity. (** justification of the replacement *) apply mapExt. intro. apply (f_equal2 count). simpl. apply (f_equal S). rewrite mult_plus_distr_r. apply (f_equal (fun y => y + x * pow k #m)). rewrite mult_assoc. reflexivity. reflexivity. Qed. Theorem Main' : forall (m:nat), T' m. Proof. intro. induction m. (** 0 *) red. intros. simpl. rewrite toListBsh'Red1. reflexivity. (** S m *) red. intros. simpl. rewrite toListBsh'Red2. apply (f_equal (fun x => g(f 0) :: x)). exact (ThmImpProp' IHm n f g 0). Qed. End Tower. (* Check Main. *) (** ** On the Definition of [flat 3] *) (** We argue that, extensionally, toListBsh3' is the same as the instance of toListBsh' for n:=3 *) (** flattening singletons *) Lemma flattensingl : forall (A:k0)(l: list A), flatten (map (fun a => a::nil) l) = l. Proof. intros. induction l. reflexivity. simpl. rewrite IHl. reflexivity. Qed. Lemma flat1OK: forall (A:k0)(l:list A), flat 1 _ l = l. Proof. intros. simpl. rewrite flattensingl. reflexivity. Qed. Lemma flat2OK: forall (A:k0)(l:list(list A)), flat 2 _ l = flatten l. Proof. intros. induction l. reflexivity. simpl. rewrite flattensingl. unfold Id. apply (f_equal (fun x => flatten(A:=A)(a :: x))). replace (map (fun l0 : listk1 A => flatten (map (fun a0 : A => a0 :: nil) l0)) l) with (map (fun l0 : list A => l0) l). rewrite (mapid(A:=list A)). reflexivity. apply mapExt. intro. rewrite flattensingl. reflexivity. Qed. (** a simple preparation *) Lemma flattenappend: forall (A:k0)(l1 l2:list(list A)), flatten(l1 ++ l2) = flatten l1 ++ flatten l2. Proof. intros. induction l1. reflexivity. (** [a::l1] *) simpl. rewrite IHl1. apply sym_eq. apply app_ass. Qed. Infix "o" := comp (at level 90). Definition flat3 (A:k0) : Pow listk1 3 A -> list A := flatten(A:=A) o flatten(A:=list A). (** the crucial observation *) Lemma flat3OK: forall (A:k0)(l:Pow listk1 3 A), flat 3 _ l = flat3 l. Proof. intros. induction l. reflexivity. simpl. unfold Id. unfold flat3. unfold comp. unfold listk1. rewrite flattenCons. rewrite flattenappend. apply (f_equal2(app(A:=A))). replace (map (fun l0 : list A => flatten (map (fun a0 : A => a0 :: nil) l0)) a) with (map (fun l0 : list A => l0) a). rewrite (mapid(A:=list A)). reflexivity. Focus 2. simpl in IHl. unfold Id in IHl. assumption. (** justifying the replacement: *) apply mapExt. intro. rewrite flattensingl. reflexivity. Qed. (** Hence, the arguments to M.It_Eq_k1 for toListBsh3' and for toListBsh' 3 are extensionally equal and we expect that those two functions will be extensionally equal as well. *) (** ** Testing towerBsh' *) Section Testing. (** the n-bush with [#n m] elements, taken from the list l, with the default element if there are not sufficiently many elements in l *) Definition mkBsh (n m:nat)(A:k0)(default:A)(l:list A) : Bsh n A := towerBsh' n m (fun x => nth x l default). Lemma mkBsh3OK: toListBsh(mkBsh 3 3 99 (first 6))= first 6 ++ 99::99::99::nil. Proof. unfold first at 1. unfold mkBsh. simpl. unfold toListBsh. Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)). reflexivity. Qed. Lemma towerBsh4OK: forall (g:nat->nat), toListBsh' g (towerBsh 4 3) = map g (first (powerplus 4 3)). Proof. intro. unfold towerBsh. simpl. Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)). reflexivity. Qed. (* Admitted. *) (** We could have saved time in not saving the proof with [Qed.] but using [Admitted.] instead. *) (** the following is not carried out in order to save time: [ Lemma tower_bsh5finalOK: forall (g:nat->nat), toListBsh' g (towerBsh 5 3) = map g (first (powerplus 5 3)). Proof. intro. unfold towerBsh. simpl. Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)). ] *) (** an idea of the time consumption on a 2005 laptop: [Finished transaction in 539. secs (532.88u,1.12s)] *) (** [ reflexivity. ] *) End Testing. (** ** n-Bushes with i Elements for any i *) Section LinearBushes. (** We show that one can easily get elements of Bsh n with a given number of data entries. *) (** singletons in Pow (Bsh n) k A for n>0 *) Fixpoint sg (n k:nat)(A:k0)(a:A){struct k} : Pow (Bsh (S n)) k A := match k return Pow (Bsh (S n)) k A with | 0 => a | S k' => bcons (S n) (sg n k' a) (bnil _ _) end. (** function for constructing bushes with k elements *) Fixpoint linBsh (n x i:nat)(A:k0)(f:nat->A) {struct i} : Bsh (S n) A := match i with | 0 => bnil (S n) _ | S i' => bcons (S n) (f x) (linBsh n (S x) i' ((sg n n (A:=_)) o f)) end. (** testing: *) Variable ft : nat -> nat. Lemma linBshOK : toListBsh (linBsh 3 7 5 ft) = map ft (count 7 5). Proof. simpl. unfold comp. unfold toListBsh. Time repeat ((rewrite toListBsh'Red1||rewrite toListBsh'Red2);try(unfold POW)). (** On a 2010 laptop: Finished transaction in 6. secs (5.344334u,0.s) *) reflexivity. Qed. Section Verification. Variable n:nat. (** n is just a parameter of the whole verification *) Definition linBshThm (i:nat) : Prop := forall(x:nat)(A B:k0)(f:nat->A)(g:A->B), toListBsh' g (linBsh n x i f) = map (g o f) (count x i). (** the auxiliary proposition where the eta-expansions of f is needed *) Definition linBshProp (i k:nat) : Prop := forall(x:nat)(A B:k0)(f:nat->A)(g:A->B), flat (S k) _ (POW (S k) (toListBsh' (n:=S n)) g (linBsh n x i ((sg n k (A:=_)) o f))) = toListBsh' g (linBsh n x i (fun y => f y)). (** some preparation *) Lemma linBshPrep : forall (k:nat)(A B:k0)(f:A->B)(a:A), flat k _ (POW k (toListBsh' (n:=S n)) f (sg n k a)) = f a::nil. Proof. intros. induction k. reflexivity. simpl. fold Pow. rewrite toListBsh'Red2. simpl. rewrite IHk. simpl. rewrite toListBsh'Red1. reflexivity. Qed. (** the crucial lemma for the later induction step *) Lemma linBshThmImpProp : forall (i:nat), linBshThm i -> forall (k: nat), linBshProp i k. Proof. intros. destruct k. red. intros. simpl. rewrite flattensingl. reflexivity. (** S k *) red. intros. set (k':=S k). unfold POW. fold POW. unfold flat. fold flat. rewrite H. rewrite <- mapcomp. unfold comp. replace (map (fun x0 : nat => flat k' B (POW k' (toListBsh' (n:=S n)) g (sg n k' (f x0)))) (count x i)) with (map (fun x:nat => g(f x)::nil)(count x i)). Focus 2. apply mapExt. intro. rewrite linBshPrep. reflexivity. change (fun x : nat => g (f x) :: nil) with ((fun x => x::nil) o (g o f)). rewrite mapcomp. rewrite flattensingl. rewrite H. reflexivity. Qed. Lemma linBshMain : forall (i:nat), linBshThm i. Proof. red. intro. induction i. intros. simpl. rewrite toListBsh'Red1. reflexivity. (** S i *) fold (linBshThm i) in IHi. intros. simpl. rewrite toListBsh'Red2. apply (f_equal (fun y => g(f x) :: y)). rewrite (linBshThmImpProp IHi). apply (IHi (S x) _ _ (fun y : nat => f y) g). Qed. (** Hence, linBsh n x i f contains i elements. *) End Verification. End LinearBushes. End BshnMod. (** ## Acknowledgement: ## The student project of Dulma Rodriguez with me at LMU Munich (and still during my first months in Toulouse) brought up the questions that led to this work. I am especially thankful to her for the programs that compute a powerlist of height n with elements 1,...,2^n, the linear 2-bush (with an arbitrary finite number of elements) and the 2-bushes with a number of entries that iterates squares. My efforts to verify them led me to the present programs. The whole student project, carried out also in Coq, can be found at ##http://www.tcs.ifi.lmu.de/~rodrigue/project.html##. I also made use of some of the code lines. *)