]> matita.cs.unibo.it Git - helm.git/commitdiff
initial qork for models
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Jun 2008 13:26:13 +0000 (13:26 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Jun 2008 13:26:13 +0000 (13:26 +0000)
helm/software/matita/contribs/dama/dama/bishop_set.ma
helm/software/matita/contribs/dama/dama/depends
helm/software/matita/contribs/dama/dama/extra.ma [deleted file]
helm/software/matita/contribs/dama/dama/models/uniformnat.ma [new file with mode: 0644]

index 7ac1b83f01a42a8a4acab41fa2b06ff6f77f6c4e..d572820799b26ed2080451ef81083c0064784a86 100644 (file)
@@ -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). 
index aa4bd85f9ea2773b12969b5467e0634837257eb3..59905eae8194600902d5c5ca43efca74abd35e8a 100644 (file)
@@ -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 (file)
index 008d842..0000000
+++ /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 (file)
index 0000000..3149776
--- /dev/null
@@ -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.