From e2a6d130d5274760f4591197bbbc66c3191e8a6a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 7 Nov 2008 10:27:20 +0000 Subject: [PATCH] ordered_set simplified --- .../contribs/dama/dama/nat_ordered_set.ma | 3 +-- .../matita/contribs/dama/dama/ordered_set.ma | 27 +++---------------- 2 files changed, 4 insertions(+), 26 deletions(-) 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 -- 2.39.2