| 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
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.
End Bsh3.
| 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)).
reflexivity.
Qed.
the brute-force alternative to the above proof:
compute.
Time repeat rewrite M.It_Eq_k1_Reduction.
reflexivity.
|
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.
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.
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.
On the Definition of
|
| 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 |
the following is not carried out in order to save time:
|
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. |