From 6b843ebfba2ed19d2bf7a564a9d2fc92da880169 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 30 May 2008 17:08:26 +0000
Subject: [PATCH] ...

---
 .../matita/contribs/dama/dama/bishop_set.ma   | 23 ++++++
 .../contribs/dama/dama/bishop_set_rewrite.ma  | 16 ++++
 .../contribs/dama/dama/cprop_connectives.ma   |  6 +-
 .../matita/contribs/dama/dama/ordered_set.ma  |  2 -
 .../matita/contribs/dama/dama/supremum.ma     | 79 ++++++++++++++++---
 5 files changed, 110 insertions(+), 16 deletions(-)

diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma
index 1c68695d3..1e7436af9 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma
@@ -75,3 +75,26 @@ qed.
 lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
 intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
 qed.
+
+definition lt ≝ λE:ordered_set.λa,b:E. a ≤ b ∧ a # b.
+
+interpretation "ordered sets less than" 'lt a b = 
+  (cic:/matita/dama/bishop_set/lt.con _ a b).
+
+lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
+intros 2 (E x); intro H; cases H (_ ABS);
+apply (bs_coreflexive ? x ABS);
+qed.
+
+lemma lt_transitive: ∀E.transitive ? (lt E).
+intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
+split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
+cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
+[1: cases (os_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (os_coreflexive ?? X)]
+|2: cases (os_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
+qed.
+
+theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
+intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
+assumption;
+qed.
diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
index bd5a83a88..19518a67b 100644
--- a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
+++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma
@@ -70,3 +70,19 @@ interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_re
 notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
 interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _).
 
+
+lemma lt_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z < y → z < x.
+intros (A x y z E H); split; cases H;
+[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption;
+qed.
+
+lemma lt_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y < z → x < z.
+intros (A x y z E H); split; cases H;
+[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption;
+qed.
+
+notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
+interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/bishop_set_rewrite/lt_rewl.con _ _ _).
+notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
+interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/bishop_set_rewrite/lt_rewr.con _ _ _).
+
diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 743803cd6..a53961733 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -33,9 +33,7 @@ inductive exT (A:Type) (P:A→CProp) : CProp ≝
 interpretation "CProp exists" 'exists \eta.x =
   (cic:/matita/dama/cprop_connectives/exT.ind#xpointer(1/1) _ x).
 
-inductive False : CProp ≝ .
-
-definition Not ≝ λx:CProp.x → False.
+definition Not : CProp → Prop ≝ λx:CProp.x → False.
 
 interpretation "constructive not" 'not x = 
   (cic:/matita/dama/cprop_connectives/Not.con x).
@@ -47,7 +45,7 @@ definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x).
 
 definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
 
-definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→CProp.∀x:A.∀y:A.R x y→R y x→eq x y.
+definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
 
 definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
 
diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index b5b4d8e78..4c72cfd98 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -51,5 +51,3 @@ cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
-  
-  
\ No newline at end of file
diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma
index 715fb5bdb..7fb1da4ba 100644
--- 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
-- 
2.39.2