From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 7 Nov 2008 10:27:20 +0000 (+0000)
Subject: ordered_set simplified
X-Git-Tag: make_still_working~4581
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e2a6d130d5274760f4591197bbbc66c3191e8a6a;p=helm.git

ordered_set simplified
---

diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
index 9129cef9a..26e2f0d29 100644
--- a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma
@@ -47,8 +47,7 @@ lemma nat_ordered_set : ordered_set.
 letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
 [ intros; left; intros; reflexivity;
 | intro x; intro H; apply (not_le_Sn_n ? H);]
-constructor 1;  
-[ apply hos; | apply (dual_hos hos); | reflexivity]
+constructor 1;  apply hos;
 qed.
 
 interpretation "ordered set N" 'N = nat_ordered_set.
diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 56b354859..890164ea9 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -36,22 +36,6 @@ record half_ordered_set: Type ≝ {
 
 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);
@@ -64,9 +48,7 @@ intro; constructor 1;
 qed.
 
 record ordered_set : Type ≝ {
-  os_l : half_ordered_set;
-  os_r_ : half_ordered_set;
-  os_with : os_r_ = dual_hos os_l
+  os_l : half_ordered_set
 }.
 
 definition os_r : ordered_set → half_ordered_set.
@@ -74,7 +56,7 @@ 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] 
+constructor 1; apply hos;  
 qed.
 
 definition Type_of_ordered_set : ordered_set → Type.
@@ -183,10 +165,7 @@ apply (mk_half_ordered_set (O × O));
 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]
+intro O; constructor 1; apply (square_half_ordered_set (os_l O));
 qed.
 
 notation "s 2 \atop \nleq" non associative with precedence 90