X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids.ma;h=28761806f0a9bab4d7f4e34eb0f858678d5c3db1;hb=742913ecf0e021372665974e4b4e3a203a3428ab;hp=87546cae917e94addf8a25dbdf142ad05a9e808f;hpb=347c7d213fd1d106f22acd6fff82a83af14c1bbd;p=helm.git diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index 87546cae9..28761806f 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -1,249 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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; - 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. -*) +notation "hvbox(a break = \sub \ID b)" non associative with precedence 45 +for @{ 'eqID $a $b }. -(* -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. +notation > "hvbox(a break =_\ID b)" non associative with precedence 45 +for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }. +interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y). *) -(************************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')) +nrecord setoid : Type[1] ≝ + { carr:> Type[0]; + eq: equivalence_relation carr }. -*) -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. +interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y). -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. +notation > "hvbox(a break =_0 b)" non associative with precedence 45 +for @{ eq_rel ? (eq ?) $a $b }. -interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b). +interpretation "setoid symmetry" 'invert r = (sym ???? r). +notation ".= r" with precedence 50 for @{'trans $r}. +interpretation "trans" 'trans r = (trans ????? r). -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) +nrecord unary_morphism (A,B: setoid) : Type[0] ≝ + { fun1:1> A → B; + prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a') }. -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. +nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝ + { fun2:2> A → B → C; + prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b') + }. -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); - | - | - | -*) -*******************) +notation "† c" with precedence 90 for @{'prop1 $c }. +notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }. +notation "#" with precedence 90 for @{'refl}. +interpretation "prop1" 'prop1 c = (prop1 ????? c). +interpretation "prop2" 'prop2 l r = (prop2 ???????? l r). +interpretation "refl" 'refl = (refl ???).