X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;h=a4b40be7a4ba844f3d774583e5890a9561862ec5;hb=bde2f037924b8854d5ed4e6b133c306156a1fcf5;hp=7008b632bb2be063a8952d1652abe4a5cdc98af6;hpb=f36588e673e67f0758fdbec52baa515a28fd9a7a;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 7008b632b..a4b40be7a 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -27,17 +27,37 @@ interpretation "" ' = ( (os_r _)).
 (* Definition 2.1 *)
 record half_ordered_set: Type ≝ {
   hos_carr:> Type;
-  hos_excess: hos_carr → hos_carr → CProp;
-  hos_coreflexive: coreflexive ? hos_excess;
-  hos_cotransitive: cotransitive ? hos_excess 
+  wloss: ∀A:Type. (A → A → CProp) → A → A → CProp;
+  wloss_prop: (∀T,P,x,y.P x y = wloss T P x y) ∨ (∀T,P,x,y.P y x = wloss T P x y); 
+  hos_excess_: hos_carr → hos_carr → CProp;
+  hos_coreflexive: coreflexive ? (wloss ? hos_excess_);
+  hos_cotransitive: cotransitive ? (wloss ? hos_excess_)
 }.
 
+definition hos_excess ≝ λO:half_ordered_set.wloss O ? (hos_excess_ O). 
+
+lemma find_leq : half_ordered_set → half_ordered_set.
+intro O; constructor 1;
+[1: apply (hos_carr O);
+|2: apply (λT:Type.λf:T→T→CProp.f); 
+|3: intros; left; intros; reflexivity;
+|4: apply (hos_excess_ O);
+|5: intro x; lapply (hos_coreflexive O x) as H; cases (wloss_prop O);
+    rewrite < H1 in H; apply H;
+|6: intros 4 (x y z H); cases (wloss_prop O);
+    rewrite > (H1 ? (hos_excess_ O)) in H ⊢ %; 
+    rewrite > (H1 ? (hos_excess_ O)); lapply (hos_cotransitive O ?? z H);
+    [assumption] cases Hletin;[right|left]assumption;]
+qed.
+
 definition dual_hos : half_ordered_set → half_ordered_set.
 intro; constructor 1;
 [ apply (hos_carr h);
-| apply (λx,y.hos_excess h y x);
+| apply (λT,f,x,y.wloss h T f y x); 
+| intros; cases (wloss_prop h);[right|left]intros;apply H; 
+| apply (hos_excess_ h);
 | apply (hos_coreflexive h);
-| intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h ?? z H);
+| intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h y x z H);
   [right|left] assumption;]
 qed.
 
@@ -49,6 +69,13 @@ record ordered_set : Type ≝ {
 
 definition os_r : ordered_set → half_ordered_set.
 intro o; apply (dual_hos (os_l o)); qed.
+
+lemma half2full : half_ordered_set → ordered_set.
+intro hos;
+constructor 1; [apply hos; | apply (dual_hos hos); | reflexivity] 
+qed.
+
+(* coercion half2full. *)
   
 definition Type_of_ordered_set : ordered_set → Type.
 intro o; apply (hos_carr (os_l o)); qed.
@@ -68,26 +95,26 @@ interpretation "Ordered set excess" 'nleq a b = (hos_excess (os_l _) a b).
 notation "'exc_coreflexive'" non associative with precedence 90 for @{'exc_coreflexive}.
 notation "'cxe_coreflexive'" non associative with precedence 90 for @{'cxe_coreflexive}.
 
-interpretation "exc_coreflexive" 'exc_coreflexive = (hos_coreflexive (os_l _)).
-interpretation "cxe_coreflexive" 'cxe_coreflexive = (hos_coreflexive (os_r _)).
+interpretation "exc_coreflexive" 'exc_coreflexive = ((hos_coreflexive (os_l _))).
+interpretation "cxe_coreflexive" 'cxe_coreflexive = ((hos_coreflexive (os_r _))).
 
 notation "'exc_cotransitive'" non associative with precedence 90 for @{'exc_cotransitive}.
 notation "'cxe_cotransitive'" non associative with precedence 90 for @{'cxe_cotransitive}.
 
-interpretation "exc_cotransitive" 'exc_cotransitive = (hos_cotransitive (os_l _)).
-interpretation "cxe_cotransitive" 'cxe_cotransitive = (hos_cotransitive (os_r _)).
+interpretation "exc_cotransitive" 'exc_cotransitive = ((hos_cotransitive (os_l _))).
+interpretation "cxe_cotransitive" 'cxe_cotransitive = ((hos_cotransitive (os_r _))).
 
 (* Definition 2.2 (3) *)
 definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
 
 notation "hvbox(a break ≤≤ b)" non associative with precedence 45 for @{ 'leq_low $a $b }.
-interpretation "Ordered half set less or equal than" 'leq_low a b = (le _ a b).
+interpretation "Half ordered set greater or equal than" 'leq_low a b = ((le _ a b)).
 
-interpretation "Ordered set greater or equal than" 'geq a b = (le (os_r _) a b).
-interpretation "Ordered set less or equal than" 'leq a b = (le (os_l _) a b).
+interpretation "Ordered set greater or equal than" 'geq a b = ((le (os_r _) a b)).
+interpretation "Ordered set less or equal than" 'leq a b = ((le (os_l _) a b)).
 
 lemma hle_reflexive: ∀E.reflexive ? (le E).
-unfold reflexive; intros 3 (E x H); apply (hos_coreflexive ?? H);
+unfold reflexive; intros 3; apply (hos_coreflexive ? x H);
 qed.
 
 notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
@@ -108,7 +135,7 @@ intros; apply le_reflexive. qed.
 *)
 
 lemma hle_transitive: ∀E.transitive ? (le E).
-unfold transitive; intros 7 (E x y z H1 H2 H3); cases (hos_cotransitive ??? y H3) (H4 H4);
+unfold transitive; intros 7 (E x y z H1 H2 H3); cases (hos_cotransitive E x z y H3) (H4 H4);
 [cases (H1 H4)|cases (H2 H4)]
 qed.
 
@@ -120,10 +147,10 @@ interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
 
 (* Lemma 2.3 *)
 lemma exc_hle_variance: 
-  ∀O:half_ordered_set.∀a,b,a',b':O.a ≰≰ b → a ≤≤ a' → b' ≤≤ b → a' ≰≰ b'.
+  ∀O:half_ordered_set.∀a,b,a',b':O.a ≰≰ b → a ≤≤ a' → b' ≤≤ b → a' ≰≰ b'. 
 intros (O a b a1 b1 Eab Laa1 Lb1b);
-cases (hos_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
-cases (hos_cotransitive ??? b1 H) (H1 H1); [assumption]
+cases (hos_cotransitive ? a b a1 Eab) (H H); [cases (Laa1 H)]
+cases (hos_cotransitive ? ?? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
 
@@ -133,16 +160,26 @@ notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_va
 interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
 interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
 
+definition square_exc ≝
+ λO:half_ordered_set.λx,y:O×O.\fst x ≰≰ \fst y ∨ \snd x ≰≰ \snd y.
+
 lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
 intro O;
 apply (mk_half_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 (hos_coreflexive ?? X);
-|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); 
-    clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
-    [1: cases (hos_cotransitive ??? z1 H1); [left; left|right;left]assumption;
-    |2: cases (hos_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
+[1: apply (wloss O);
+|2: intros; cases (wloss_prop O); [left|right] intros; apply H;
+|3: apply (square_exc O); 
+|4: intro x; cases (wloss_prop O); rewrite < (H  ? (square_exc O) x x); clear H;
+    cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1;
+    [1,3: apply (hos_coreflexive O h H1);
+    |*: apply (hos_coreflexive O h1 H1);]
+|5: intros 3 (x0 y0 z0); cases (wloss_prop O);
+    do 3 rewrite < (H  ? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0;
+    simplify; intro H; cases H; clear H;
+    [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption;
+    |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption;
+    |3: cases (hos_cotransitive ? h2 h h4 H1); [right;left|left;left] assumption;
+    |4: cases (hos_cotransitive ? h3 h1 h5 H1); [right;right|left;right] assumption;]]
 qed.
 
 lemma square_ordered_set: ordered_set → ordered_set.