From: Enrico Tassi Date: Wed, 8 Jul 2009 14:09:06 +0000 (+0000) Subject: few more files, one diverges X-Git-Tag: make_still_working~3729 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a88be1ca42c0969dbab9a5c76240f5931df876d9 few more files, one diverges --- diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 1b7a60cdb..2aca2bbd3 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,5 +1,8 @@ sets/sets.ma logic/equality.ma +topology/igt.ma logic/connectives.ma properties/relations.ma logic/equality.ma logic/connectives.ma +.unnamed.ma logic/pts.ma logic/connectives.ma logic/pts.ma algebra/magmas.ma sets/sets.ma +properties/relations.ma logic/pts.ma logic/pts.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index eb6855410..8898c6c2e 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,12 +1,19 @@ digraph g { "sets/sets.ma" []; "sets/sets.ma" -> "logic/equality.ma" []; + "topology/igt.ma" []; + "topology/igt.ma" -> "logic/connectives.ma" []; + "topology/igt.ma" -> "properties/relations.ma" []; "logic/equality.ma" []; "logic/equality.ma" -> "logic/connectives.ma" []; + ".unnamed.ma" []; + ".unnamed.ma" -> "logic/pts.ma" []; "logic/connectives.ma" []; "logic/connectives.ma" -> "logic/pts.ma" []; "algebra/magmas.ma" []; "algebra/magmas.ma" -> "sets/sets.ma" []; + "properties/relations.ma" []; + "properties/relations.ma" -> "logic/pts.ma" []; "logic/pts.ma" []; } \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index 31bab1539..6d8cfcfd9 100644 Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ diff --git a/helm/software/matita/nlibrary/properties/relations.ma b/helm/software/matita/nlibrary/properties/relations.ma new file mode 100644 index 000000000..619ab7807 --- /dev/null +++ b/helm/software/matita/nlibrary/properties/relations.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "logic/pts.ma". + +ndefinition reflexive ≝ λT:Type.λP:T → T → CProp. ∀x.P x x. +ndefinition symmetric ≝ λT:Type.λP:T → T → CProp. ∀x,y.P x y → P y x. +ndefinition transitive ≝ λT:Type.λP:T → T → CProp. ∀z,x,y. P x z → P z y → P x y. diff --git a/helm/software/matita/nlibrary/topology/igt.ma b/helm/software/matita/nlibrary/topology/igt.ma new file mode 100644 index 000000000..fbe12b638 --- /dev/null +++ b/helm/software/matita/nlibrary/topology/igt.ma @@ -0,0 +1,249 @@ +include "logic/connectives.ma". +include "properties/relations.ma". + +nrecord iff (A,B: CProp) : CProp ≝ + { if: A → B; + fi: B → A + }. + +notation > "hvbox(a break \liff b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +notation "hvbox(a break \leftrightarrow b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +interpretation "logical iff" 'iff x y = (iff x y). + +nrecord setoid : Type[1] ≝ + { carr:> Type; + eq: carr → carr → CProp; + refl: reflexive ? eq; + sym: symmetric ? eq; + trans: transitive ? eq + }. + +ndefinition proofs: CProp → setoid. +#P; napply (mk_setoid ?????); +##[ napply P; +##| napply (λ_,_.True); + #x; #y; napply True; (* DIVERGE *) + intro; + constructor 1; + [ apply A + | intros; + apply True + | intro; + constructor 1 + | intros 3; + constructor 1 + | intros 5; + constructor 1] +qed. + +definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x. +definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x. +definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z. + +record setoid1 : Type ≝ + { carr1:> Type; + eq1: carr1 → carr1 → CProp; + refl1: reflexive1 ? eq1; + sym1: symmetric1 ? eq1; + trans1: transitive1 ? eq1 + }. + +definition proofs1: CProp → setoid1. + intro; + constructor 1; + [ apply A + | intros; + apply True + | intro; + constructor 1 + | intros 3; + constructor 1 + | intros 5; + constructor 1] +qed. + +definition CCProp: setoid1. + constructor 1; + [ apply CProp + | apply iff + | intro; + split; + intro; + assumption + | intros 3; + cases H; clear H; + split; + assumption + | intros 5; + cases H; cases H1; clear H H1; + split; + intros; + [ apply (H4 (H2 H)) + | apply (H3 (H5 H))]] +qed. + +record function_space (A,B: setoid): Type ≝ + { f:1> A → B; + f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a')) + }. + +notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }. + +record function_space1 (A: setoid1) (B: setoid1): Type ≝ + { f1:1> A → B; + f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a')) + }. + +definition function_space_setoid: setoid → setoid → setoid. + intros (A B); + constructor 1; + [ apply (function_space A B); + | intros; + apply (∀a:A. proofs (eq ? (f a) (f1 a))); + | simplify; + intros; + apply (f_ok ? ? x); + unfold carr; unfold proofs; simplify; + apply (refl A) + | simplify; + intros; + unfold carr; unfold proofs; simplify; + apply (sym B); + apply (f a) + | simplify; + intros; + unfold carr; unfold proofs; simplify; + apply (trans B ? (y a)); + [ apply (f a) + | apply (f1 a)]] +qed. + +definition function_space_setoid1: setoid1 → setoid1 → setoid1. + intros (A B); + constructor 1; + [ apply (function_space1 A B); + | intros; + apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a))); + |*: cases daemon] (* simplify; + intros; + apply (f1_ok ? ? x); + unfold proofs; simplify; + apply (refl1 A) + | simplify; + intros; + unfold proofs; simplify; + apply (sym1 B); + apply (f a) + | simplify; + intros; + unfold carr; unfold proofs; simplify; + apply (trans1 B ? (y a)); + [ apply (f a) + | apply (f1 a)]] *) +qed. + +interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b). + +record isomorphism (A,B: setoid): Type ≝ + { map1:> function_space_setoid A B; + map2:> function_space_setoid B A; + inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a); + inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b) + }. + +interpretation "isomorphism" 'iff x y = (isomorphism x y). + +definition setoids: setoid1. + constructor 1; + [ apply setoid; + | apply isomorphism; + | intro; + split; + [1,2: constructor 1; + [1,3: intro; assumption; + |*: intros; assumption] + |3,4: + intros; + simplify; + unfold proofs; simplify; + apply refl;] + |*: cases daemon] +qed. + +definition setoid1_of_setoid: setoid → setoid1. + intro; + constructor 1; + [ apply (carr s) + | apply (eq s) + | apply (refl s) + | apply (sym s) + | apply (trans s)] +qed. + +coercion setoid1_of_setoid. + +(* +record dependent_product (A:setoid) (B: A ⇒ setoids): Type ≝ + { dp:> ∀a:A.carr (B a); + dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a'))) + }.*) + +record forall (A:setoid) (B: A ⇒ CCProp): CProp ≝ + { fo:> ∀a:A.proofs (B a) }. + +record subset (A: setoid) : CProp ≝ + { mem: A ⇒ CCProp }. + +definition ssubset: setoid → setoid1. + intro; + constructor 1; + [ apply (subset s); + | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a) + | simplify; + intros; + split; + intro; + assumption + | simplify; + cases daemon + | cases daemon] +qed. + +definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp. + intros; + constructor 1; + [ apply mem; + | unfold function_space_setoid1; simplify; + intros (b b'); + change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a); + unfold proofs1; simplify; intros; + unfold proofs1 in c; simplify in c; + unfold ssubset in c; simplify in c; + cases (c a); clear c; + split; + assumption] +qed. + +(* +definition sand: CCProp ⇒ CCProp. + +definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A. + intro; + constructor 1; + [ intro; + constructor 1; + [ intro; + constructor 1; + constructor 1; + intro; + apply (mem ? c c2 ∧ mem ? c1 c2); + | + | + | +*)