From: Claudio Sacerdoti Coen Date: Mon, 27 Jul 2009 10:31:40 +0000 (+0000) Subject: setoids.ma split into setoids.ma + setoids1.ma X-Git-Tag: make_still_working~3613 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1dd64d6c49db7dc0dc0ee39c30da4c7a043b8bde;p=helm.git setoids.ma split into setoids.ma + setoids1.ma --- diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 9147636b0..c8f0287ad 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,4 +1,5 @@ sets/sets.ma logic/equality.ma +sets/setoids1.ma sets/setoids.ma sets/setoids.ma logic/connectives.ma properties/relations.ma logic/equality.ma logic/connectives.ma logic/connectives.ma logic/pts.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index 53ce1f34c..6a1e65939 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,6 +1,8 @@ digraph g { "sets/sets.ma" []; "sets/sets.ma" -> "logic/equality.ma" []; + "sets/setoids1.ma" []; + "sets/setoids1.ma" -> "sets/setoids.ma" []; "sets/setoids.ma" []; "sets/setoids.ma" -> "logic/connectives.ma" []; "sets/setoids.ma" -> "properties/relations.ma" []; diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index c648df50e..cb081dd85 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/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma index 25fb2ce93..026e92169 100644 --- a/helm/software/matita/nlibrary/logic/connectives.ma +++ b/helm/software/matita/nlibrary/logic/connectives.ma @@ -39,3 +39,18 @@ ninductive Ex (A:Type) (P:A → CProp) : CProp ≝ ex_intro: ∀x:A. P x → Ex A P. interpretation "exists" 'exists x = (Ex ? x). + +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). diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index 87546cae9..ed2973d87 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -1,21 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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; @@ -32,82 +31,19 @@ ndefinition proofs: CProp → setoid. ##] 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}.; +nrecord 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); +ndefinition function_space_setoid: setoid → setoid → setoid. + #A; #B; napply (mk_setoid ?????); +##[ napply (function_space A B); +##| #f; #f1; napply (∀a:A. proofs (eq ? (f a) (f1 a))); +##| nwhd; #x; #a; + napply (f_ok ? ? x ? ? ?); (* QUI!! *) unfold carr; unfold proofs; simplify; apply (refl A) | simplify; @@ -123,33 +59,7 @@ definition function_space_setoid: setoid → setoid → setoid. | 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 ≝ +nrecord 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); @@ -158,92 +68,10 @@ record isomorphism (A,B: setoid): Type ≝ 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 diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma new file mode 100644 index 000000000..0571b6dfa --- /dev/null +++ b/helm/software/matita/nlibrary/sets/setoids1.ma @@ -0,0 +1,176 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "sets/setoids.ma". + +(* +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. + +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_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). + +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 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); + | + | + | + +*)