From b1087303f8e1601aaa3723c42a32626b31e5b10e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Jun 2008 13:26:13 +0000 Subject: [PATCH] initial qork for models --- .../matita/contribs/dama/dama/bishop_set.ma | 4 +- .../matita/contribs/dama/dama/depends | 21 +++-- .../matita/contribs/dama/dama/extra.ma | 87 ------------------- .../contribs/dama/dama/models/uniformnat.ma | 50 +++++++++++ 4 files changed, 64 insertions(+), 98 deletions(-) delete mode 100644 helm/software/matita/contribs/dama/dama/extra.ma create mode 100644 helm/software/matita/contribs/dama/dama/models/uniformnat.ma diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma index 7ac1b83f0..d57282079 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma @@ -23,7 +23,7 @@ record bishop_set: Type ≝ { bs_cotransitive: cotransitive ? bs_apart }. -notation "hvbox(a break # b)" non associative with precedence 50 +notation "hvbox(a break # b)" non associative with precedence 45 for @{ 'apart $a $b}. interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y). @@ -41,7 +41,7 @@ qed. (* Definition 2.2 (2) *) definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b). -notation "hvbox(a break ≈ b)" non associative with precedence 50 +notation "hvbox(a break ≈ b)" non associative with precedence 45 for @{ 'napart $a $b}. interpretation "Bishop set alikeness" 'napart a b = (eq _ a b). diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index aa4bd85f9..59905eae8 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,17 +1,20 @@ +sandwich.ma ordered_uniform.ma +property_sigma.ma ordered_uniform.ma +uniform.ma supremum.ma bishop_set.ma ordered_set.ma -extra.ma bishop_set_rewrite.ma -ordered_set.ma cprop_connectives.ma -cprop_connectives.ma logic/equality.ma -bishop_set_rewrite.ma bishop_set.ma sequence.ma nat/nat.ma -uniform.ma supremum.ma -supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma -nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma -property_sigma.ma ordered_uniform.ma ordered_uniform.ma uniform.ma +supremum.ma bishop_set.ma cprop_connectives.ma nat/plus.ma nat_ordered_set.ma ordered_set.ma sequence.ma property_exhaustivity.ma ordered_uniform.ma property_sigma.ma +bishop_set_rewrite.ma bishop_set.ma +cprop_connectives.ma logic/equality.ma +nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma lebesgue.ma property_exhaustivity.ma sandwich.ma -sandwich.ma ordered_uniform.ma +ordered_set.ma cprop_connectives.ma +models/rationals.ma Q/q/q.ma uniform.ma +models/uniformnat.ma bishop_set_rewrite.ma datatypes/constructors.ma nat_ordered_set.ma uniform.ma +Q/q/q.ma +datatypes/constructors.ma logic/equality.ma nat/compare.ma nat/nat.ma diff --git a/helm/software/matita/contribs/dama/dama/extra.ma b/helm/software/matita/contribs/dama/dama/extra.ma deleted file mode 100644 index 008d84202..000000000 --- a/helm/software/matita/contribs/dama/dama/extra.ma +++ /dev/null @@ -1,87 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "bishop_set_rewrite.ma". - -definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x # y. - - - -definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b. - -interpretation "ordered sets less than" 'lt a b = (lt _ a b). - -lemma lt_coreflexive: ∀E.coreflexive ? (lt E). -intros 2 (E x); intro H; cases H (_ ABS); -apply (ap_coreflexive ? x ABS); -qed. - -lemma lt_transitive: ∀E.transitive ? (lt E). -intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); -split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2; -cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz; -[1: cases (exc_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (exc_coreflexive ?? X)] -|2: cases (exc_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]] -qed. - -theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a). -intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)] -fold normalize (b ≰ a); assumption; (* BUG *) -qed. - -lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x. -intros (A x y z E H); split; cases H; -[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption; -qed. - -lemma lt_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y < z → x < z. -intros (A x y z E H); split; cases H; -[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption; -qed. - -notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}. -interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _). -notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}. -interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _). - -lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z. -intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)] -cases APx (EXx EXx); [cases (LEx EXx)] -cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)] -right; assumption; -qed. - -lemma le_lt_transitive: ∀A:excess.∀x,y,z:A.x ≤ y → y < z → x < z. -intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)] -cases APx (EXx EXx); [cases (LEx EXx)] -cases (exc_cotransitive ??? x EXx) (EXz EXz); [right; assumption] -cases LE; assumption; -qed. - -lemma le_le_eq: ∀E:excess.∀a,b:E. a ≤ b → b ≤ a → a ≈ b. -intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption; -qed. - -lemma eq_le_le: ∀E:excess.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a. -intros (E x y H); whd in H; -split; intro; apply H; [left|right] assumption. -qed. - -lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a. -intros; split; assumption; -qed. - -definition total_order_property : ∀E:excess. Type ≝ - λE:excess. ∀a,b:E. a ≰ b → b < a. - diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma new file mode 100644 index 000000000..314977675 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "datatypes/constructors.ma". +include "nat_ordered_set.ma". +include "bishop_set_rewrite.ma". +include "uniform.ma". + +definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space. +intro C; apply (mk_uniform_space C); +[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); +|2: intros 4 (U H x Hx); unfold in Hx; + cases H (_ H1); cases (H1 x); apply H2; apply Hx; +|3: intros; cases H (_ PU); cases H1 (_ PV); + exists[apply (λx.U x ∧ V x)] split; + [1: exists[apply something] intro; cases (PU n); cases (PV n); + split; intros; try split;[apply H2;|apply H4] try assumption; + apply H3; cases H6; assumption; + |2: simplify; unfold mk_set; intros; assumption;] +|4: intros; cases H (_ PU); exists [apply U] split; + [1: exists [apply something] intro n; cases (PU n); + split; intros; try split;[apply H1;|apply H2] assumption; + |2: intros 2 (x Hx); cases Hx; cases H1; clear H1; + cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5; + cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8; + generalize in match H5; generalize in match H8; + generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8; + cases x; simplify; intros; cases H1; clear H1; apply H4; + apply (eq_trans ???? H3 H2);] +|5: intros; cases H (_ H1); split; cases x; + [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉); + lapply (H6 H4) as H7; apply eq_sym; apply H7; + |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉); + lapply (H6 H4) as H7; apply eq_sym; apply H7;]] +qed. + +definition nat_uniform_space: uniform_space. +apply (discrete_uniform_space_of_bishop_set nat_ordered_set); +qed. -- 2.39.2