From 1ff3965d308be074f3ed5181b3c38921f289b6a9 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 12 Mar 2008 12:02:02 +0000
Subject: [PATCH] Nuova dimostrazione riflessiva di le_to_Bertrand.

---
 helm/software/matita/library/nat/bertrand.ma | 168 ++++++++++++++++++-
 1 file changed, 163 insertions(+), 5 deletions(-)

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index bb4fde497..3f613c8d7 100644
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -70,7 +70,8 @@ definition in_list \def
    \lambda A.\lambda a:A.\lambda l:list A.
    \exists l1,l2.l = l1@(a::l2).
 
-lemma in_list_filter_to_p_true : \forall l,x,p.in_list nat x (filter nat l p) \to p x = true.
+lemma in_list_filter_to_p_true : \forall l,x,p.
+in_list nat x (filter nat l p) \to p x = true.
 intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
   [simplify;intro;elim l1
      [simplify in H;destruct H
@@ -435,10 +436,11 @@ intro.elim n 0
      |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]]
 qed.
 
+definition list_of_primes \def \lambda n.\lambda l.
+\forall p.in_list nat p l  \to prime p \land p \leq n.
+
 lemma sieve_sound1 : \forall n.2 \leq n \to
-                               sorted_gt (sieve n) \land
-                               (\forall p.in_list ? p (sieve n) \to
-                               prime p \land p \leq n).
+sorted_gt (sieve n) \land list_of_primes n (sieve n).
 intros;elim (sieve_prime n n (list_n n) [])
   [split
      [assumption
@@ -546,6 +548,23 @@ definition bertrand \def \lambda n.
 definition not_bertrand \def \lambda n.
 \forall p.n < p \to p \le 2*n \to \not (prime p).
 
+(*
+lemma list_of_primes_SO: \forall l.list_of_primes 1 l \to
+l = [].
+intro.cases l;intros
+  [reflexivity
+  |apply False_ind.unfold in H.
+   absurd ((prime n) \land n \le 1)
+    [apply H.
+     apply in_list_head
+    |intro.elim H1.
+     elim H2.
+     apply (lt_to_not_le ? ? H4 H3)
+    ]
+  ]
+qed.
+*)
+
 lemma min_prim : \forall n.\exists p. n < p \land prime p \land
                  \forall q.prime q \to q < p \to q \leq n.
 intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
@@ -571,6 +590,144 @@ intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
       |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]]
 qed.
 
+theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
+list_of_primes pn l  \to
+(\forall p. prime p \to p \le pn \to in_list nat p l) \to 
+(\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
+intros.
+elim (min_prim n).
+apply (ex_intro ? ? a).
+elim H6.clear H6.elim H7.clear H7.
+split
+  [split
+    [assumption
+    |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
+      [elim (H5 a)
+        [elim H10.clear H10.elim H11.clear H11.
+         apply (trans_le ? ? ? H12).
+         apply le_times_r.
+         apply H8
+          [unfold in H3.
+           elim (H3 a1 H10).
+           assumption
+          |assumption
+          ]
+        |apply H4
+          [assumption
+          |apply not_lt_to_le.intro. 
+           apply (lt_to_not_le ? ? H2).
+           apply H8;assumption
+          ]
+        |assumption
+        ]
+      |rewrite < H7.
+       apply O_lt_const_to_le_times_const.
+       assumption
+      ]
+    ]
+  |assumption
+  ]
+qed.
+
+let rec check_list l \def
+  match l with
+  [ nil \Rightarrow true
+  | cons (hd:nat) tl \Rightarrow
+    match tl with
+     [ nil \Rightarrow eqb hd 2
+     | cons hd1 tl1 \Rightarrow 
+      (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
+    ]
+  ]
+.
+
+lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to 
+m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
+intros 3.
+change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
+intro.
+lapply (andb_true_true ? ? H) as H1.
+lapply (andb_true_true_r ? ? H) as H2.clear H.
+lapply (andb_true_true ? ? H1) as H3.
+lapply (andb_true_true_r ? ? H1) as H4.clear H1.
+split
+  [split
+    [split
+      [apply leb_true_to_le.assumption
+      |apply leb_true_to_le.assumption
+      ]
+    |assumption
+    ]
+  |generalize in match H2.
+   cases l
+    [intro.reflexivity
+    |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
+     intro.
+     lapply (andb_true_true_r ? ? H) as H2.
+     assumption
+    ]
+  ]
+qed.
+    
+theorem check_list2: \forall l. check_list l = true \to
+\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
+intro.elim l 2
+  [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
+  |cases l1;intros
+    [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
+     apply False_ind.
+     apply (lt_to_not_eq ? ? H3).
+     apply sym_eq.apply eqb_true_to_eq.
+     rewrite > H4.apply H1
+    |elim (check_list1 ? ? ? H1).clear H1.
+     elim H4.clear H4.
+     elim H1.clear H1.
+     elim (in_list_cons_case ? ? ? ? H2)
+      [apply (ex_intro ? ? n).
+       split
+        [split
+          [apply in_list_cons.apply in_list_head
+          |rewrite > H1.assumption
+          ]
+        |rewrite > H1.assumption
+        ]
+      |elim (H H6 p H1 H3).clear H.
+       apply (ex_intro ? ? a). 
+       elim H8.clear H8.
+       elim H.clear H.
+       split
+        [split
+          [apply in_list_cons.assumption
+          |assumption
+          ]
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
+(* qualcosa che non va con gli S *)
+lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
+intros.
+apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
+  [assumption
+  |apply primeb_true_to_prime.reflexivity
+  |apply (le_to_lt_to_lt ? ? ? H1).
+   apply le_n
+  |lapply (sieve_sound1 (S(exp 2 8))) as H
+    [elim H.assumption
+    |apply leb_true_to_le.reflexivity
+    ]
+  |intros.apply (sieve_sound2 ? ? H3 H2)
+  |(* se tolgo l'argomento l'apply diventa lenta *)
+   apply (check_list2 (sieve (S(exp 2 8)))).
+   reflexivity
+  ]
+qed.
+
 (*lemma pippo : \forall k,n.in_list ? (nth_prime (S k)) (sieve n) \to
               \exists l.sieve n = l@((nth_prime (S k))::(sieve (nth_prime k))).
 intros;elim H;elim H1;clear H H1;apply (ex_intro ? ? a);
@@ -578,6 +735,7 @@ cut (a1 = sieve (nth_prime k))
   [rewrite < Hcut;assumption
   |lapply (sieve_sorted n);generalize in match H2*) 
 
+(* old proof by Wilmer 
 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 intros;
 elim (min_prim n);apply (ex_intro ? ? a);elim H2;elim H3;clear H2 H3;
@@ -660,7 +818,7 @@ split
             |apply prime_nth_prime
             |rewrite < H3;apply increasing_nth_prime]]]
    |assumption]
-qed.
+qed. *)
 
 lemma not_not_bertrand_to_bertrand1: \forall n.
 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
-- 
2.39.2