From: Claudio Sacerdoti Coen Date: Mon, 27 Jul 2009 10:18:47 +0000 (+0000) Subject: topology/igt.ma (???) |-> sets/setoids.ma X-Git-Tag: make_still_working~3614 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=347c7d213fd1d106f22acd6fff82a83af14c1bbd;p=helm.git topology/igt.ma (???) |-> sets/setoids.ma --- diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 379c57656..9147636b0 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,5 +1,5 @@ sets/sets.ma logic/equality.ma -topology/igt.ma logic/connectives.ma properties/relations.ma +sets/setoids.ma logic/connectives.ma properties/relations.ma logic/equality.ma logic/connectives.ma logic/connectives.ma logic/pts.ma algebra/magmas.ma sets/sets.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index 9069f0cd9..53ce1f34c 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,9 +1,9 @@ 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" []; + "sets/setoids.ma" []; + "sets/setoids.ma" -> "logic/connectives.ma" []; + "sets/setoids.ma" -> "properties/relations.ma" []; "logic/equality.ma" []; "logic/equality.ma" -> "logic/connectives.ma" []; "logic/connectives.ma" []; diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index c00871d4a..c648df50e 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/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma new file mode 100644 index 000000000..87546cae9 --- /dev/null +++ b/helm/software/matita/nlibrary/sets/setoids.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; +##| #x; #y; napply True; +##|##*: nwhd; nrepeat (#_); napply I; +##] +nqed. + +(* +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. +*) + +(* +ndefinition 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. + +*) + +(************************CSC +nrecord function_space (A,B: setoid): Type[1] ≝ + { f:1> carr A → carr 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); + | + | + | +*) +*******************) diff --git a/helm/software/matita/nlibrary/topology/igt.ma b/helm/software/matita/nlibrary/topology/igt.ma deleted file mode 100644 index df8880733..000000000 --- a/helm/software/matita/nlibrary/topology/igt.ma +++ /dev/null @@ -1,249 +0,0 @@ -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; -##| #x; #y; napply True; -##|##*: nwhd; nrepeat (#_); napply I; -##] -nqed. - -(* -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. -*) - -(* -ndefinition 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. - -*) - -(************************CSC -nrecord function_space (A,B: setoid): Type[1] ≝ - { f:1> carr A → carr 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); - | - | - | -*) -*******************) \ No newline at end of file