exhaustivity defined

[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 b2411f65263a318cee22f7529a0dec08baa59a60..b99323140e3fd8a9423b142fade9a2b7a33a4114 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/supremum.ma
+++ b/helm/software/matita/contribs/dama/dama/supremum.ma
@@ -122,6 +122,17 @@ include "nat_ordered_set.ma".
 alias symbol "nleq" = "Ordered set excess".
 alias symbol "leq" = "Ordered set less or equal than".
 lemma trans_increasing: 
+  ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m.
+intros 5 (C a Hs n m); elim m; [
+  rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
+  intro X; cases (os_coreflexive ?? X);]
+cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
+[2: rewrite > H2; intro; cases (os_coreflexive ?? H1);
+|1: apply (le_transitive ???? (H ?) (Hs ?));
+    intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
+qed.
+
+lemma trans_increasing_exc: 
   ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
 intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
 intro; apply H; 
@@ -153,12 +164,12 @@ 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] apply (Hm n);
+[1: intro n; simplify; apply trans_increasing_exc; [assumption] apply (Hm n);
 |2: intro n; simplify; apply Uu;
 |3: intros (y Hy); simplify; cases (Hu ? Hy);
     cases (strictly_increasing_reaches C ? Hm w); 
     exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]  
-    cases (trans_increasing C ? Ia ?? H1); assumption;]
+    cases (trans_increasing_exc C ? Ia ?? H1); assumption;]
 qed.     
     
 (* Definition 2.7 *)
@@ -281,15 +292,40 @@ definition convex ≝
 definition upper_located ≝
   λO:ordered_set.λa:sequence O.∀x,y:O. y ≰ x → 
     (∃i:nat.a i ≰ x) ∨ (∃b:O.y≰b ∧ ∀i:nat.a i ≤ b).
+
+definition lower_located ≝
+  λO:ordered_set.λa:sequence O.∀x,y:O. x ≰ y → 
+    (∃i:nat.x ≰ a i) ∨ (∃b:O.b≰y ∧ ∀i:nat.b ≤ a i).
+
+notation < "s \nbsp 'is_upper_located'" non associative with precedence 50 
+  for @{'upper_located $s}.
+notation > "s 'is_upper_located'" non associative with precedence 50 
+  for @{'upper_located $s}.
+interpretation "Ordered set upper locatedness" 'upper_located s    = 
+  (cic:/matita/dama/supremum/upper_located.con _ s).
+
+notation < "s \nbsp 'is_lower_located'" non associative with precedence 50 
+  for @{'lower_located $s}.
+notation > "s 'is_lower_located'" non associative with precedence 50 
+  for @{'lower_located $s}.
+interpretation "Ordered set lower locatedness" 'lower_located s    = 
+  (cic:/matita/dama/supremum/lower_located.con _ s).
     
 (* Lemma 2.12 *)    
-lemma uparrow_located:
-  ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → upper_located ? a.
+lemma uparrow_upperlocated:
+  ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → a is_upper_located.
 intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
 cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
 [2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
 |1: right; exists [apply u]; split; [apply W|apply H4]]
 qed. 
 
+lemma downarrow_lowerlocated:
+  ∀C:ordered_set.∀a:sequence C.∀u:C.a ↓ u → a is_lower_located.
+intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
+cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
+[1: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
+|2: right; exists [apply u]; split; [apply W|apply H4]]
+qed. 
      
     
\ No newline at end of file