From 7af9d84f465b5f4b609b08ae914681526d12480a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 11 Jun 2008 16:58:16 +0000
Subject: [PATCH] gran casino

---
 .../matita/contribs/dama/dama/depends         |   8 +-
 .../contribs/dama/dama/models/uniformnat.ma   | 261 +++++++++++++++---
 .../contribs/dama/dama/nat_ordered_set.ma     |  20 +-
 .../contribs/dama/dama/property_sigma.ma      |  13 +-
 .../contribs/dama/dama/russell_support.ma     |  27 ++
 .../matita/contribs/dama/dama/supremum.ma     |   9 +-
 .../matita/contribs/dama/dama/uniform.ma      |   2 +-
 7 files changed, 275 insertions(+), 65 deletions(-)
 create mode 100644 helm/software/matita/contribs/dama/dama/russell_support.ma

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index 59905eae8..368625b80 100644
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,5 +1,5 @@
 sandwich.ma ordered_uniform.ma
-property_sigma.ma ordered_uniform.ma
+property_sigma.ma ordered_uniform.ma russell_support.ma
 uniform.ma supremum.ma
 bishop_set.ma ordered_set.ma
 sequence.ma nat/nat.ma
@@ -11,10 +11,10 @@ cprop_connectives.ma logic/equality.ma
 nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma
 lebesgue.ma property_exhaustivity.ma sandwich.ma
 ordered_set.ma cprop_connectives.ma
-models/rationals.ma Q/q/q.ma uniform.ma
-models/uniformnat.ma bishop_set_rewrite.ma datatypes/constructors.ma nat_ordered_set.ma uniform.ma
-Q/q/q.ma 
+russell_support.ma cprop_connectives.ma nat/nat.ma
+models/uniformnat.ma bishop_set_rewrite.ma datatypes/constructors.ma decidable_kit/decidable.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma
 datatypes/constructors.ma 
+decidable_kit/decidable.ma 
 logic/equality.ma 
 nat/compare.ma 
 nat/nat.ma 
diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
index c65299ad6..8c0acd9a2 100644
--- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
+++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "datatypes/constructors.ma".
 include "nat_ordered_set.ma".
 include "bishop_set_rewrite.ma".
 include "uniform.ma".
@@ -51,54 +50,236 @@ notation "\naturals" non associative with precedence 99 for @{'nat}.
 interpretation "naturals" 'nat = nat.
 interpretation "Ordered set N" 'nat = nat_ordered_set.
 
+include "russell_support.ma".
+
+inductive cmp_cases (n,m:nat) : CProp ≝
+  | cmp_lt : n < m → cmp_cases n m
+  | cmp_eq : n = m → cmp_cases n m
+  | cmp_gt : m < n → cmp_cases n m.
+  
+lemma cmp_nat: ∀n,m.cmp_cases n m.
+intros;
+simplify; intros; generalize in match (nat_compare_to_Prop n m);
+cases (nat_compare n m); intros;
+[constructor 1|constructor 2|constructor 3]
+assumption;
+qed.
+
+lemma trans_le_lt_lt:
+  ∀n,m,o:nat.n≤m→m<o→n<o.
+intros; apply (trans_le ? (S m)); [apply le_S_S;apply H;|apply H1]
+qed.
+
+alias symbol "lt" (instance 2) = "ordered sets less than".
+lemma key: 
+ ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → ∀n,m. a n < a m → n < m.
+intros; cases (cmp_nat n m); 
+[assumption
+|generalize in match H1; rewrite < H2; intros; 
+ cases (not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3;
+|cases (not_lt_n_n (fst (a m))); 
+ apply (trans_le_lt_lt ? (fst (a n)));
+ [2: apply os_lt_to_nat_lt; apply H1;
+ |1: apply os_le_to_nat_le; apply (trans_increasing ?? H m n);
+     apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S; apply H2]]
+qed. 
+
+lemma le_lt_transitive:
+ ∀O:ordered_set.∀a,b,c:O.a≤b→b<c→a<c.
+intros;
+split;
+[1: apply (le_transitive ???? H); cases H1; assumption;
+|2: cases H1; cases (bs_cotransitive ??? a H3); [2:assumption]
+    cut (a<b);[2: split; [assumption] apply bs_symmetric; assumption]
+    cut (a<c);[2: apply (lt_transitive ???? Hcut H1);]
+    cases Hcut1; assumption]
+qed.
+
+alias symbol "pi1" = "sigma pi1".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
-    ∀x.x is_supremum a → ∃i.∀j.i ≤ j → x ≈ a j.
-intros 5; cases x; clear x; intros;
-cases H2; 
+    ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
+intros 5; cases x (s Hs); clear x; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) s Hs); 
+fold normalize X; intros; cases H1; 
+alias symbol "pi1" = "sigma pi1".
+letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)]));
 letin m ≝ (
   let rec aux i ≝
     match i with
-    [ O ⇒ match eqb (fst (a O)) x1 with
-            [ true ⇒ O
-            | false ⇒ match H4 (a O) ? with
-                      [ ex_introT n _ ⇒ n]]
-    | S m ⇒ let pred ≝ aux m in 
-            match eqb (fst (a pred)) x1 with
-            [ true ⇒ pred
-            | false ⇒ match H4 (a pred) ? with
-                      [ ex_introT n _ ⇒ n]]]
-   in aux
+    [ O ⇒ O
+    | S m ⇒ 
+        let pred ≝ aux m in
+        let apred ≝ a pred in 
+        match cmp_nat (fst apred) s with
+        [ cmp_eq _ ⇒ pred
+        | cmp_gt nP ⇒ match ? in False return λ_.nat with []
+        | cmp_lt nP ⇒ fst (H3 apred nP)]]
+  in aux 
    :
-   ∀i:nat.∃j.a j = x1 ∨ a i < a j);  
-        
-cases (∀n.a n = x1 ∨ x1 ≰ a n);
-
- elim x1 in H1 ⊢ % 0; 
-[1: intro H2; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) O H2); intros;
-    fold unfold X X in H1 ⊢ %;
-    exists [apply O] cases H1; intros; apply le_le_eq;[2: apply H3;]
-    intro; alias symbol "pi1" = "sigma pi1".
-    change in H6 with (fst (a j) < O);
-    apply (not_le_Sn_O (fst (a j))); apply H6;
-|2: intros 3; letin S_X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) (S n) H2); intros;
-    fold unfold S_X S_X in H3 ⊢ %;
-    generalize in match (leb_to_Prop l n); elim (leb l n); simplify in H4;
-    [1: cut (n ≤ u); [2: cases H2; normalize in H5 ⊢ %;
-          apply le_S_S_to_le; lapply (not_lt_to_le ?? H5) as XX;
-          apply le_S; apply XX;]
-        cases H1; [2:split; apply nat_le_to_os_le; assumption|3:simplify;
+   ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
+[1: apply (H2 pred nP);
+|4: right; split; whd; constructor 1;
+|2,3: whd in ⊢ (? ? %);
+  [1: left; assumption
+  |2: elim (H3 (a (aux n1)) H5) (res_n);
+      change with (fst (a res_n) = s ∨ (n1 < res_n ∧ fst (a n1) < fst (a res_n)));
+      change in H7 with (fst (a (aux n1)) < fst (a res_n));
+      elim (aux n1) in H7 ⊢ % (pred);
+      change in H8 with (fst (a pred) < fst (a res_n));
+      cases H7; clear H7;
+      [ left; apply le_to_le_to_eq;
+        [ apply os_le_to_nat_le; apply (H2 res_n);
+        | rewrite < H9; apply le_S_S_to_le; apply le_S; apply H8;]
+      | cases H9; clear H9; right; split;
+        [ lapply (trans_increasing ?? H n1 pred (nat_le_to_os_le ?? H7)) as H11;
+          clear H6; apply (key ??? H);
+          apply (le_lt_transitive ?? (a pred)); [assumption]
+          generalize in match H8; cases (a pred); cases (a res_n);
+          simplify; intro D; lapply (nat_lt_to_os_lt ?? D) as Q;
+          cases Q; clear D Q; split; assumption;
+        | generalize in match H10; generalize in match H7; clear H7 H10;
+          cases n1; intros;
+          [ rewrite < H9; assumption
+          | clear H9; apply (trans_le_lt_lt ??? ? H8);
+            apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
+            apply(trans_increasing ?? H (S n2) (pred) H77);]]]]] 
+clearbody m; unfold spec in m; clear spec;
+cut (∀i.fst a (m i) = s ∨ i ≤ fst (a (m i))) as key2;[ 
+letin find ≝ (
+ let rec find i u on u : nat ≝
+  match u with
+  [ O ⇒ (m i:nat)
+  | S w ⇒ match eqb (fst (a (m i))) s with
+          [ true ⇒ (m i:nat)
+          | false ⇒ find (S i) w]]
+ in find
+ :
+  ∀i,bound.∃j.i + bound = u → s = fst (a j));
+[1: cases (find (S n) n2); intro; change with (s = fst (a w));
+    apply H6; rewrite < H7; simplify; apply plus_n_Sm;
+|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
+|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
+    cases (key2 u); [symmetry;assumption]
+    cases Hs; apply le_to_le_to_eq;[2:change with (fst (a (m u)) ≤ fst X); apply os_le_to_nat_le; apply (H2 (m u));]
+    apply (trans_le ??? (os_le_to_nat_le ?? H5) H4);
+|4: clearbody find; cases (find O u);
+    exists [apply w]; intros; change with (s = fst (a j));
+    rewrite > (H4 ?); [2: reflexivity]
+    apply le_to_le_to_eq; [apply os_le_to_nat_le;
+      apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));]
+    apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
+    rewrite < (H4 ?); [2: reflexivity] apply le_n;]]
+alias symbol "pi1" (instance 15) = "exT fst".
+alias symbol "pi1" (instance 10) = "exT fst".
+alias symbol "pi1" (instance 7) = "exT fst".
+alias symbol "pi1" (instance 4) = "exT fst".
+alias symbol "nat" = "naturals".
+cut (∀i.fst (a (fst (m i))) = s
+        ∨ 
+        i ≤ fst (m i)
+        ∧ 
+        match i in nat return λn:ℕ.Prop with 
+        [O⇒ fst (a (fst(m i))) = fst (a O)
+        |S (w:ℕ)⇒fst (a w) < fst (a (fst(m i)))]) as mitico;[2:
+ intro; cases (m i); apply H4;]
+cut (∀i.fst (a (m i)) = s ∨ fst (a (m i)) < fst (a (m (S i))));[2:
+  intro; 
+  cases (mitico (S i));
+    [2: cases (mitico i);
+          [2: cases H5 (H6 _); cases H4 (_ H7); clear H4 H5;
+              change in H7 with (fst (a i) < fst (a (fst (m (S i)))));
+              right; 
+              
+  
+  generalize in match (mitico i); clear mitico;
+  
+  
+  cases (m i); intros; cases H5; clear H5;
+  [left; assumption]
+  cases H6; clear H6; simplify in H7;
+  
+   change with (fst (a w)=s ∨ a w<a (m (S i)));
+  cases H4; [left; assumption]
+  cases H5; clear H4 H5;
+  cases (m (S i)); change with (fst (a w)=s ∨ a w<a w1);
+  m i = w
+  m Si = w1
+  
+  
+  
+   elim i;
+  [1: cases (m (S O)); change with (fst (a (m O))=s∨a (m O)<a w);
+  |2: cases (m (S (S n))); change with (fst (a (m (S n)))=s∨a (m (S n))<a w);
+      
+      cases H4; clear H4;
+      [1: right; split; 
+          [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
+           rewrite > H5; apply (H2 (m O));
+          |
+      |2: cases H5; clear H5; change in H6 with (fst (a O) < fst (a w));
+          right; split;  [change with (le nat_ordered_set (fst (a (m O))) (fst (a w)));
+          apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S; 
+          (* apply H6; *)
+          |]]
+       
+  
+  
+      cases (m O); change with (fst (a w) = s ∨ a w < a (m (S O)));
+      cases H4[left; assumption] cases H5; clear H4 H5;
+      change in H7 with (fst (a w) = fst (a O));
+      
+
+intro; elim i; [1: right; apply le_O_n;]
+generalize in match (refl_eq ? (S n):S n = S n);
+generalize in match (S n) in ⊢ (? ? ? % → %); intro R; 
+cases (m R); intros; change with (fst (a w) = s ∨ R ≤ fst (a w));
+rewrite < H6 in H5 ⊢ %; clear H6 R; cases H5; [left; assumption]
+cases H6; clear H6 H5; change in H8 with (fst (a n) < fst (a w));
+lapply (key l u a H n w);
+
+w = m (S n)
+ 
     
-    elim (or_lt_le (S n) l); 
-      [ cases (?:l = S n ∨ l < S n);[ 
-          unfold lt; cases H2; normalize in H5; 
-        apply (Right (eq nat n (S n)) (lt n (S n)) ?).apply (not_le_to_lt (S n) n ?).apply (not_le_Sn_n n).]
-        [ destruct H4;
 
-  
-  ∀x.∃i.x ≰ a i ∨ x ≤ a i.
-intros; elim x;
+STOP
+
+
+letin m ≝ (
+  let rec aux i ≝
+    match i with
+    [ O ⇒ 
+        let a0 ≝ a O in 
+        match cmp_nat (fst a0) s with
+        [ cmp_eq _ ⇒ O
+        | cmp_gt nP ⇒ match ? in False return λ_.nat with []
+        | cmp_lt nP ⇒ fst (H3 a0 nP)]
+    | S m ⇒ 
+        let pred ≝ aux m in
+        let apred ≝ a pred in 
+        match cmp_nat (fst apred) s with
+        [ cmp_eq _ ⇒ pred
+        | cmp_gt nP ⇒ match ? in False return λ_.nat with []
+        | cmp_lt nP ⇒ 
+        
+                      fst (H3 apred nP)]]
+  in aux 
+   :
+   ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %;
+[1: apply (H2 O nP);
+|2: apply (H2 pred nP);
+|5: left; assumption;
+|6: right; cases (H3 (a O) H5); change with (fst (a O) < fst (a w));
+    apply H7;
+|4: right; elim (H3 (a (aux n1)) H5); change with (fst (a (S n1)) < fst (a a1));
+    rewrite < H4; elim (aux n1) in H7 ⊢ %; elim H7 in H8; clear H7;
+    simplify in H9;
+    
+|3: clear H6; generalize in match H5; cases (aux n1); intros; clear H5;
+    simplify 
+     
 
+STOP
+ 
 
 definition nat_uniform_space: uniform_space.
 apply (discrete_uniform_space_of_bishop_set ℕ);
diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index 6ecbe5424..18ecf8e60 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -12,10 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ordered_set.ma".
-
+include "bishop_set.ma". 
 include "nat/compare.ma".
-include "cprop_connectives.ma". 
+include "cprop_connectives.ma".
 
 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
 
@@ -60,4 +59,17 @@ lemma nat_le_to_os_le:
   ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
 intros 3; apply (le_to_not_lt a b);assumption;
 qed.
-  
\ No newline at end of file
+
+alias id "lt" = "cic:/matita/dama/bishop_set/lt.con".
+lemma nat_lt_to_os_lt:
+  ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
+intros 3; split;
+[1: apply nat_le_to_os_le; apply lt_to_le;assumption;
+|2: right; apply H;]
+qed.
+
+lemma os_lt_to_nat_lt:
+  ∀a,b:nat_ordered_set. lt nat_ordered_set a b → a < b.
+intros; cases H; clear H; cases H2;
+[2: apply H;| cases (H1 H)]
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index 757c18a07..ece02e9ba 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ordered_uniform.ma".
-
+include "russell_support.ma".
 
 (* Definition 3.5 *)
 alias num (instance 0) = "natural number".
@@ -57,17 +57,6 @@ qed.
 lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
 intros; rewrite > sym_max in H; apply (max_le_l ??? H); 
 qed.
-
-definition hide ≝ λT:Type.λx:T.x.
-
-notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide = (hide _ _).
-interpretation "hide2" 'hide = (hide _ _ _).
-
-definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
-coercion cic:/matita/dama/property_sigma/inject.con 0 1.
-definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
-coercion cic:/matita/dama/property_sigma/eject.con.
       
 (* Lemma 3.6 *)   
 lemma sigma_cauchy:
diff --git a/helm/software/matita/contribs/dama/dama/russell_support.ma b/helm/software/matita/contribs/dama/dama/russell_support.ma
new file mode 100644
index 000000000..bcaabd677
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/russell_support.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/nat.ma".
+include "cprop_connectives.ma".
+
+definition hide ≝ λT:Type.λx:T.x.
+
+notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
+interpretation "hide" 'hide = (hide _ _).
+interpretation "hide2" 'hide = (hide _ _ _).
+
+definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
+coercion cic:/matita/dama/russell_support/inject.con 0 1.
+definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
+coercion cic:/matita/dama/russell_support/eject.con.
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 1e6c95b8d..e6b9dbbc6 100644
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -14,6 +14,7 @@
 
 include "sequence.ma".
 include "ordered_set.ma".
+include "datatypes/constructors.ma".
 
 (* Definition 2.4 *)
 definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
@@ -257,7 +258,7 @@ intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
 |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
 qed.
 
-notation "hvbox({[a, break b]})" non associative with precedence 90 
+notation "hvbox({[a, break b]})" non associative with precedence 80 
   for @{'segment_set $a $b}.
 interpretation "Ordered set segment" 'segment_set a b = 
  (segment_ordered_set _ a b).
@@ -297,11 +298,11 @@ interpretation "pair pi2" 'pi2 x = (second _ _ x).
 notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
 interpretation "pair" 'pair a b = (prod _ _ a b).
  
-notation "a \times b" left associative with precedence 60 for @{'prod $a $b}.
-interpretation "prod" 'prod a b = (pair a b).
+interpretation "prod" 'product a b = (pair a b).
  
 lemma square_ordered_set: ordered_set → ordered_set.
-intro O; apply (mk_ordered_set (O × O));
+intro O;
+apply (mk_ordered_set (O × O));
 [1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
 |2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
     cases H (X X); apply (os_coreflexive ?? X);
diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index 25cfe67cb..348b99a81 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -31,7 +31,7 @@ notation "a \subseteq u" left associative with precedence 70
   for @{ 'subset $a $u }.
 interpretation "Bishop subset" 'subset a b = (subset _ a b). 
 
-notation "hvbox({ ident x : t | break p })" non associative with precedence 50
+notation "hvbox({ ident x : t | break p })" non associative with precedence 80
   for @{ 'explicitset (\lambda ${ident x} : $t . $p) }.  
 definition mk_set ≝ λT:bishop_set.λx:T→Prop.x.
 interpretation "explicit set" 'explicitset t = (mk_set _ t).
-- 
2.39.2