Library Sieve

Require Export Systems.
Require Export Cpo_nat.
Require Export Arith.
Require Export Euclid.

Sieve.v: Example of Sieve of Eratosthenes
  • sift (cons a s) == cons a (sift (filter (div a) s))

Preliminaries on divisibility


Definition div (n m:nat) := exists q, m = q * n.

Lemma div0 : forall q n r, r=q * n -> r < n -> r = O.
intros; destruct q; auto.
simpl in H.
absurd (n <= r)%nat; try omega.
subst; case (q*n); intros; omega.
Save.

Lemma div0bis : forall q q' n r, q * n = q' * n + r -> r < n -> r = O.
intros; assert (r= (q-q')*n).
assert (0<n).
apply le_lt_trans with r; auto with arith.
assert (~q * n < q' * n).
red; intro; try omega.
rewrite mult_minus_distr_r.
rewrite H; omega.
apply div0 with (q-q') n; auto.
Save.

Definition div_dec : forall n m, {div n m}+ {~ div n m}.
intro; assert ({n=O}+{0<n}).
destruct n; auto with arith.
case H; intros.
subst n.
destruct m; intros.
left; exists O; simpl; auto with arith.
right; intros (q,H1).
absurd (S m = O); try omega.
case (modulo n l m); intros r H1.
assert (Hr:{r=O}+{0<r}).
destruct r; auto with arith.
case Hr; intro.
left; case H1; intros q (H2,H3); exists q; subst; auto with arith.
right; intro H2; case H2; intros q H3; case H1; intros q' (H4,H5).
absurd (r=O); try omega.
apply div0bis with q q' n; auto.
transitivity m; auto.
Save.

Definition of the system
  • o = sift i is recursively defined by: o = app i Y ; Y = sift X; X = fdiv i

Definition LI : Type := unit.
Definition i := tt.

Inductive LO : Type := X | Y | o.

Definition D := nat.

Definition SL : LI+LO -> Type := fun i => D.

Node corresponding to the division


Definition fdiv : DS D -c> DS D := DSCASE D D (fun a => FILTER (div a) (div_dec a)).

Lemma fdiv_cons : forall a s, fdiv (cons a s) = filter (div a) (div_dec a) s.
intros; unfold fdiv; rewrite DSCASE_simpl; rewrite DScase_cons; auto.
Save.

Definition of the system parameterized by sift


Definition Funsift : (DS D -C-> DS D) -m> system SL.
exists (fun fs (x:LO) => match x with X => fdiv @_ PROJ (DS_fam SL) (inl LO i)
                                                            | Y => fs @_ PROJ (DS_fam SL) (inr LI X)
                                                            | o => (APP D @2_ PROJ (DS_fam SL) (inl LO i))
                                                                                       (PROJ (DS_fam SL) (inr LI Y))
              end).
red; intros f g Hfg; intro x.
case x; auto.
apply (fcont_le_intro (D1:=Dprodi (DS_fam SL)) (D2:=DS D)); intro P;
repeat rewrite fcont_comp_simpl; auto.
Defined.

Lemma Funsift_simpl : forall fs x, Funsift fs x = match x with X => fdiv @_ PROJ (DS_fam SL) (inl LO i)
                                                            | Y => fs @_ PROJ (DS_fam SL) (inr LI X)
                                                            | o => (APP D @2_ PROJ (DS_fam SL) (inl LO i))
                                                                                       (PROJ (DS_fam SL) (inr LI Y))
              end.
trivial.
Save.

Definition FunSift : (DS D -C-> DS D) -c> system SL.
exists Funsift; red; intros; intro x.
rewrite Funsift_simpl.
unfold system; rewrite Dprodi_lub_simpl.
apply (fcont_le_intro (D1:=DS_prod SL) (D2:=DS (inrSL SL x))); intro p.
rewrite fcont_lub_simpl.
case x; repeat rewrite fcont_comp_simpl.
apply Ole_trans with (2:= le_lub (Proj (fun x0 : LO => DS_prod SL -C-> DS (inrSL SL x0)) X @ (Funsift @ h) <__>
   p) O); trivial.
rewrite fcont_lub_simpl.
apply lub_le_compat; intro n; auto.
repeat rewrite fcont_comp2_simpl.
apply Ole_trans with (2:= le_lub (Proj (fun x0 : LO => DS_prod SL -C-> DS (inrSL SL x0)) o @ (Funsift @ h) <__>
   p) O); trivial.
Defined.

Lemma FunSift_simpl : forall fs x, FunSift fs x = match x with X => fdiv @_ PROJ (DS_fam SL) (inl LO i)
                                                            | Y => fs @_ PROJ (DS_fam SL) (inr LI X)
                                                            | o => (APP D @2_ PROJ (DS_fam SL) (inl LO i))
                                                                                       (PROJ (DS_fam SL) (inr LI Y))
              end.
trivial.
Save.
  • focus restrict to the input and output observed
Definition focus : (DS_prod (inlSL SL) -C-> DS_prod SL) -c> DS D -C-> DS D :=
     PROJ (DS_fam SL) (inr LI o) @@_ fcont_SEQ (DS D) (DS_prod (inlSL SL)) (DS_prod SL) (PAIR1 (DS D)).

Lemma focus_simpl : forall (f : DS_prod (inlSL SL) -C-> DS_prod SL) (s:DS D),
    focus f s = f (pair1 s) (inr LI o).
trivial.
Save.

Definition and properties of sift

Definition sift : DS D -C-> DS D :=
               FIXP (DS D -C->DS D) (focus @_ (sol_of_system SL @_ FunSift)).

Lemma sift_eq : sift == focus (sol_of_system SL (FunSift sift)).
exact (FIXP_eq (focus @_ (sol_of_system SL @_ FunSift))).
Save.
Hint Resolve sift_eq.

Lemma sift_le_compat : forall x y, x <= y -> sift x <= sift y.
intros; apply fcont_monotonic; auto.
Save.
Hint Resolve sift_le_compat.

Lemma sift_eq_compat : forall x y, x == y -> sift x == sift y.
intros; apply fcont_stable; auto.
Save.
Hint Resolve sift_eq_compat.

Lemma sol_of_system_i : forall s : DS D, sol_of_system SL (FunSift sift) (pair1 s) (inl LO i) == s.
intro s; exact (Oprodi_eq_elim (sol_of_system_eq (FunSift sift) (pair1 s)) (inl LO i)).
Save.

Lemma sol_of_system_X : forall s : DS D,
            sol_of_system SL (FunSift sift) (pair1 s) (inr LI X) == fdiv s.
intro s; apply Oeq_trans with (1:=Oprodi_eq_elim (sol_of_system_eq (FunSift sift) (pair1 s)) (inr LI X)).
rewrite eqn_of_system_simpl.
rewrite FunSift_simpl.
rewrite fcont_comp_simpl.
apply (fcont_stable fdiv).
exact (sol_of_system_i s).
Save.

Lemma sol_of_system_Y : forall s : DS D,
            sol_of_system SL (FunSift sift) (pair1 s) (inr LI Y) == sift (fdiv s).
intro s; apply Oeq_trans with (1:=Oprodi_eq_elim (sol_of_system_eq (FunSift sift) (pair1 s)) (inr LI Y)).
rewrite eqn_of_system_simpl.
rewrite FunSift_simpl.
rewrite fcont_comp_simpl.
apply (fcont_stable sift).
exact (sol_of_system_X s).
Save.

Lemma sol_of_system_o : forall s : DS D,
            sol_of_system SL (FunSift sift) (pair1 s) (inr LI o) == app s (sift (fdiv s)).
intro s; apply Oeq_trans with (1:=Oprodi_eq_elim (sol_of_system_eq (FunSift sift) (pair1 s)) (inr LI o)).
rewrite eqn_of_system_simpl.
rewrite FunSift_simpl.
rewrite fcont_comp2_simpl.
rewrite APP_simpl.
exact (app_eq_compat (sol_of_system_i s) (sol_of_system_Y s)).
Save.

Lemma sift_prop : forall a s, sift (cons a s) == cons a (sift (filter (div a) (div_dec a) s)).
intros ; apply Oeq_trans with (1:=fcont_eq_elim sift_eq (cons a s)).
rewrite focus_simpl.
rewrite sol_of_system_o.
rewrite app_cons.
apply cons_eq_compat; trivial.
apply sift_eq_compat.
rewrite fdiv_cons; auto.
Save.
Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (30 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (14 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (3 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (11 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

Global Index

D

D [definition, in Sieve]
div [definition, in Sieve]
div0 [lemma, in Sieve]
div0bis [lemma, in Sieve]
div_dec [definition, in Sieve]


F

fdiv [definition, in Sieve]
fdiv_cons [lemma, in Sieve]
focus [definition, in Sieve]
focus_simpl [lemma, in Sieve]
FunSift [definition, in Sieve]
Funsift [definition, in Sieve]
Funsift_simpl [lemma, in Sieve]
FunSift_simpl [lemma, in Sieve]


I

i [definition, in Sieve]


L

LI [definition, in Sieve]
LO [inductive, in Sieve]


O

o [constructor, in Sieve]


S

Sieve [library]
sift [definition, in Sieve]
sift_eq [lemma, in Sieve]
sift_eq_compat [lemma, in Sieve]
sift_le_compat [lemma, in Sieve]
sift_prop [lemma, in Sieve]
SL [definition, in Sieve]
sol_of_system_i [lemma, in Sieve]
sol_of_system_o [lemma, in Sieve]
sol_of_system_X [lemma, in Sieve]
sol_of_system_Y [lemma, in Sieve]


X

X [constructor, in Sieve]


Y

Y [constructor, in Sieve]


Lemma Index

D

div0 [in Sieve]
div0bis [in Sieve]


F

fdiv_cons [in Sieve]
focus_simpl [in Sieve]
Funsift_simpl [in Sieve]
FunSift_simpl [in Sieve]


S

sift_eq [in Sieve]
sift_eq_compat [in Sieve]
sift_le_compat [in Sieve]
sift_prop [in Sieve]
sol_of_system_i [in Sieve]
sol_of_system_o [in Sieve]
sol_of_system_X [in Sieve]
sol_of_system_Y [in Sieve]


Constructor Index

O

o [in Sieve]


X

X [in Sieve]


Y

Y [in Sieve]


Inductive Index

L

LO [in Sieve]


Definition Index

D

D [in Sieve]
div [in Sieve]
div_dec [in Sieve]


F

fdiv [in Sieve]
focus [in Sieve]
FunSift [in Sieve]
Funsift [in Sieve]


I

i [in Sieve]


L

LI [in Sieve]


S

sift [in Sieve]
SL [in Sieve]


Library Index

S

Sieve


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (30 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (14 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (3 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (11 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)
This page has been generated by coqdoc