CProp hierarchy is there!

[helm.git] / helm / software / matita / contribs / dama / dama / supremum.ma

diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 715fb5bdbcd5f50f87afaef34b4d27ce48a4222c..7fb1da4ba8e512f208b2661862cc6f949bf3762f 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -18,7 +18,7 @@ include "ordered_set.ma".
 (* Definition 2.4 *)
 definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
 
-definition strong_sup ≝
+definition supremum ≝
   λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
 
 definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
@@ -27,33 +27,92 @@ notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50
   for @{'upper_bound $s $x}.
 notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 
   for @{'increasing $s}.
-notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 
-  for @{'strong_sup $s $x}.
+notation < "x \nbsp 'is_supremum' \nbsp s"  non associative with precedence 50 
+  for @{'supremum $s $x}.
 
 notation > "x 'is_upper_bound' s" non associative with precedence 50 
   for @{'upper_bound $s $x}.
 notation > "s 'is_increasing'"    non associative with precedence 50 
   for @{'increasing $s}.
-notation > "x 'is_strong_sup' s"  non associative with precedence 50 
-  for @{'strong_sup $s $x}.
+notation > "x 'is_supremum' s"  non associative with precedence 50 
+  for @{'supremum $s $x}.
 
 interpretation "Ordered set upper bound" 'upper_bound s x = 
   (cic:/matita/dama/supremum/upper_bound.con _ s x).
 interpretation "Ordered set increasing"  'increasing s    = 
   (cic:/matita/dama/supremum/increasing.con _ s).
-interpretation "Ordered set strong sup"  'strong_sup s x  = 
-  (cic:/matita/dama/supremum/strong_sup.con _ s x).
+interpretation "Ordered set strong sup"  'supremum s x  = 
+  (cic:/matita/dama/supremum/supremum.con _ s x).
 
-include "bishop_set.ma".  
+include "nat/compare.ma".
+include "nat/plus.ma".  
+include "bishop_set.ma".
   
 lemma uniq_supremum: 
   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
-    t1 is_strong_sup s → t2 is_strong_sup s → t1 ≈ t2.
+    t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
 intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2); 
 apply le_le_eq; intro X;
 [1: cases (H1 ? X); apply (U2 w); assumption
 |2: cases (H2 ? X); apply (U1 w); assumption]
 qed.
 
+(* Fact 2.5 *)
+lemma supremum_is_upper_bound: 
+  ∀C:ordered_set.∀a:sequence C.∀u:C.
+   u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
+intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
+cases (H1 ? H) (w Hw); apply Hv; assumption;
+qed.
+
+(* Lemma 2.6 *)
+definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
+ 
+definition nat_excess : nat → nat → CProp ≝ λn,m. leb (m+S O) n = true.
+
+axiom nat_excess_cotransitive: cotransitive ? nat_excess.
+(*intros 3 (x y z); elim x 0; elim y 0; elim z 0;
+    [1: intros; left; assumption
+    |2,5,6,7: intros; first [right; constructor 1|left; constructor 1]
+    |3: intros (n H abs); simplify in abs; destruct abs;
+    |4: intros (n H m W abs); simplify in abs; destruct abs;
+    |8: clear x y z; intros (x H1 y H2 z H3 H4);
+*)
+
+lemma nat_ordered_set : ordered_set.
+apply (mk_ordered_set ? nat_excess);
+[1: intro x; elim x (w H); simplify; intro X; [destruct X] apply H; assumption;
+|2: apply nat_excess_cotransitive]
+qed.
 
-    
+notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 
+  for @{'strictly_increasing $s}.
+notation > "s 'is_strictly_increasing'" non associative with precedence 50 
+  for @{'strictly_increasing $s}.
+interpretation "Ordered set increasing"  'strictly_increasing s    = 
+  (cic:/matita/dama/supremum/strictly_increasing.con _ s).
+  
+notation "a \uparrow u"  non associative with precedence 50 for  @{'sup_inc $a $u}.
+interpretation "Ordered set supremum of increasing" 'sup_inc s u =
+ (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) 
+  (cic:/matita/dama/supremum/increasing.con _ s)
+  (cic:/matita/dama/supremum/supremum.con _ s u)).
+  
+lemma trans_increasing: 
+  ∀C:ordered_set.∀s:sequence C.s is_increasing → ∀n,m. m ≰ n → s n ≤ s m.
+intros 5 (C s Hs n m); elim m; [1: cases (?:False); autobatch]
+cases (le_to_or_lt_eq ?? H1);
+ [2: destruct H2; apply Hs;
+ |1: apply (le_transitive ???? (H (lt_S_S_to_lt ?? H2))); apply Hs;]
+qed.
+  
+lemma selection: 
+  ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
+    ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
+intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split; 
+[1: intro n; simplify; apply trans_increasing; [assumption] 
+    lapply (Hm n) as W; unfold nat_ordered_set in W; simplify in W;
+    cases W;
+|2: intro n;
+|3:
+    
\ No newline at end of file