X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fordered_set.ma;h=8a1191442087608a404182a3f89212e73423ec47;hb=bf7f52019b3f65b6d635a8b49a63f0d95080f189;hp=a227af3c1928927fe04185224cfe1b409d9b8029;hpb=ca41435a6021292ccba239aa173651c0be705b45;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 a227af3c1..8a1191442 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -12,53 +12,144 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "cprop_connectives.ma".
+include "datatypes/constructors.ma".
+include "logic/cprop_connectives.ma".
+
+
+(* TEMPLATES
+notation "''" non associative with precedence 90 for @{'}.
+notation "''" non associative with precedence 90 for @{'}.
+
+interpretation "" ' = ( (os_l _)).
+interpretation "" ' = ( (os_r _)).
+*)
 
 (* Definition 2.1 *)
-record ordered_set: Type ≝ {
-  os_carr:> Type;
-  os_excess: os_carr → os_carr → CProp;
-  os_coreflexive: coreflexive ? os_excess;
-  os_cotransitive: cotransitive ? os_excess 
+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 
+}.
+
+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 (hos_coreflexive h);
+| intros 4 (x y z H); simplify in H ⊢ %; cases (hos_cotransitive h ?? z H);
+  [right|left] assumption;]
+qed.
+
+record ordered_set : Type ≝ {
+  os_l : half_ordered_set;
+  os_r_ : half_ordered_set;
+  os_with : os_r_ = dual_hos os_l
 }.
 
-interpretation "Ordered set excess" 'nleq a b = (os_excess _ a b). 
+definition os_r : ordered_set → half_ordered_set.
+intro o; apply (dual_hos (os_l o)); qed.
+  
+definition Type_of_ordered_set : ordered_set → Type.
+intro o; apply (hos_carr (os_l o)); qed.
+
+definition Type_of_ordered_set_dual : ordered_set → Type.
+intro o; apply (hos_carr (os_r o)); qed.
+
+coercion Type_of_ordered_set_dual.
+coercion Type_of_ordered_set.
+
+notation "a ≰≰ b" non associative with precedence 45 for @{'nleq_low $a $b}.
+interpretation "Ordered half set excess" 'nleq_low a b = (hos_excess _ a b).
+
+interpretation "Ordered set excess (dual)" 'ngeq a b = (hos_excess (os_r _) a b).
+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 _)).
+
+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 _)).
 
 (* Definition 2.2 (3) *)
-definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b).
+definition le ≝ λE:half_ordered_set.λa,b:E. ¬ (a ≰≰ b).
 
-interpretation "Ordered set greater or equal than" 'geq a b = (le _ b a).
+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 "Ordered set less or equal than" 'leq 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).
 
-lemma le_reflexive: ∀E.reflexive ? (le E).
-unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H);
+lemma hle_reflexive: ∀E.reflexive ? (le E).
+unfold reflexive; intros 3 (E x H); apply (hos_coreflexive ?? H);
 qed.
 
-lemma le_transitive: ∀E.transitive ? (le E).
-unfold transitive; intros 7 (E x y z H1 H2 H3); cases (os_cotransitive ??? y H3) (H4 H4);
+notation "'le_reflexive'" non associative with precedence 90 for @{'le_reflexive}.
+notation "'ge_reflexive'" non associative with precedence 90 for @{'ge_reflexive}.
+
+interpretation "le reflexive" 'le_reflexive = (hle_reflexive (os_l _)).
+interpretation "ge reflexive" 'ge_reflexive = (hle_reflexive (os_r _)).
+
+(* DUALITY TESTS 
+lemma test_le_ge_convertible :∀o:ordered_set.∀x,y:o. x ≤ y → y ≥ x.
+intros; assumption; qed.
+
+lemma test_ge_reflexive :∀o:ordered_set.∀x:o. x ≥ x.
+intros; apply ge_reflexive. qed.
+
+lemma test_le_reflexive :∀o:ordered_set.∀x:o. x ≤ x.
+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);
 [cases (H1 H4)|cases (H2 H4)]
 qed.
 
+notation "'le_transitive'" non associative with precedence 90 for @{'le_transitive}.
+notation "'ge_transitive'" non associative with precedence 90 for @{'ge_transitive}.
+
+interpretation "le transitive" 'le_transitive = (hle_transitive (os_l _)).
+interpretation "ge transitive" 'ge_transitive = (hle_transitive (os_r _)).
+
 (* Lemma 2.3 *)
-lemma exc_le_variance: 
-  ∀O:ordered_set.∀a,b,a',b':O.a ≰ b → a ≤ a' → b' ≤ b → a' ≰ b'.
+lemma exc_hle_variance: 
+  ∀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 (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
-cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
+cases (hos_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
+cases (hos_cotransitive ??? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
 
-lemma square_ordered_set: ordered_set → ordered_set.
+notation "'exc_le_variance'" non associative with precedence 90 for @{'exc_le_variance}.
+notation "'exc_ge_variance'" non associative with precedence 90 for @{'exc_ge_variance}.
+
+interpretation "exc_le_variance" 'exc_le_variance = (exc_hle_variance (os_l _)).
+interpretation "exc_ge_variance" 'exc_ge_variance = (exc_hle_variance (os_r _)).
+
+lemma square_half_ordered_set: half_ordered_set → half_ordered_set.
 intro O;
-apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
+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 (os_coreflexive ?? X);
+    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 (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
-    |2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
+    [1: cases (hos_cotransitive ??? z1 H1); [left; left|right;left]assumption;
+    |2: cases (hos_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
+qed.
+
+lemma square_ordered_set: ordered_set → ordered_set.
+intro O; constructor 1;
+[ apply (square_half_ordered_set (os_l O));
+| apply (dual_hos (square_half_ordered_set (os_l O)));
+| reflexivity]
 qed.
 
 notation "s 2 \atop \nleq" non associative with precedence 90
@@ -70,7 +161,5 @@ interpretation "ordered set square" 'square_os s = (square_ordered_set s).
 
 definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
 
-notation "a \subseteq u" left associative with precedence 70 
-  for @{ 'subset $a $u }.
-interpretation "ordered set subset" 'subset a b = (os_subset _ a b). 
+interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).