(** Copyright 2006, Ralph Matthes, CNRS & IRIT UPS 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.0pl3 - just coqide/coqtop/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.
(** 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 _ (fun t1 => F m _
(fun t2 => (F m _ (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 flattenCons.
rewrite IHl.
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 list.
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 list :=
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 list k A -> list A :=
match k return forall (A:k0), Pow list 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 list := M.It_Eq_k1 bshf
(fun (A : k0) (t : BshF list 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 list.
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 list := fun _ => toListBsh' (id(A:=_)).
(** * Programming the n-Bushes *)
Require Import Bvector.
Print vector.
(* Check Vhead : forall (A : Set) (n : nat), vector A (S n) -> A.
Check Vtail : forall (A : Set) (n : nat), vector A (S n) -> vector A n. *)
Inductive Tree: k0 := L' : Tree | N' : vector Tree n -> Tree.
Definition vec (k:nat) := vector Tree k.
Definition vnil : vec 0 := Vnil Tree.
Definition vcons (t:Tree)(k:nat) : vec k -> vec (S k) := Vcons Tree t k.
Fixpoint LL(l:list Tree)(k:nat){struct k} : (vector Tree k->Tree) -> Pow list k Tree :=
match k return (vector Tree k->Tree) -> Pow list 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}:
(vector Tree k -> A) -> Pow Bsh k A :=
match k return (vector Tree 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:vector Tree 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)).
apply 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.
Require Import Bvector.
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 flattenCons.
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 flattenCons.
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 : list 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.
do 2 rewrite flattenCons.
rewrite IHl1.
apply sym_eq.
apply app_ass.
Qed.
Infix "o" := comp (at level 90).
Definition flat3 (A:k0) : Pow list 3 A -> list A :=
flatten(A:=A) o flatten(A:=list A).
(** the crucial observation *)
Lemma flat3OK: forall (A:k0)(l:Pow list 3 A),
flat 3 _ l = flat3 l.
Proof.
intros.
induction l.
reflexivity.
simpl.
rewrite flattenCons.
unfold Id.
unfold flat3.
unfold comp.
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.
Admitted.
(** We save time in not saving the proof with [Qed.] *)
(** 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: [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)).
(** Finished transaction in 25. secs (25.03u,0.01s) *)
reflexivity.
Admitted.
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.
*)