Another bug.

[helm.git] / helm / software / matita / contribs / dama / dama / ordered_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index 2a1089fec45188916b69bfd8659df83030afcf49..890164ea950d405fd295ad26e0227d62b68d42e7 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -27,35 +27,19 @@ interpretation "" ' = ( (os_r _)).
 (* Definition 2.1 *)
 record half_ordered_set: Type ≝ {
   hos_carr:> Type;
-  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); 
+  wloss: ∀A,B:Type. (A → A → B) → A → A → B;
+  wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y); 
   hos_excess_: hos_carr → hos_carr → CProp;
-  hos_coreflexive: coreflexive ? (wloss ? hos_excess_);
-  hos_cotransitive: cotransitive ? (wloss ? hos_excess_)
+  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 hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O). 
 
 definition dual_hos : half_ordered_set → half_ordered_set.
 intro; constructor 1;
 [ apply (hos_carr h);
-| apply (λT,f,x,y.wloss h T f y x); 
+| apply (λT,R,f,x,y.wloss h T R f y x); 
 | intros; cases (wloss_prop h);[right|left]intros;apply H; 
 | apply (hos_excess_ h);
 | apply (hos_coreflexive 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.
@@ -169,12 +151,12 @@ apply (mk_half_ordered_set (O × O));
 [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;
+|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;
+    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;
@@ -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