X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids.ma;h=e593ea7d52be439e22b776a8c5d81aa334547f3f;hb=e8fbe5898b3214a5b0c4d48e8c9d1ee55f3415cc;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..e593ea7d5 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -1,249 +1,113 @@ +(**************************************************************************) +(* ___ *) +(* ||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". +include "hints_declaration.ma". + +nrecord setoid : Type[1] ≝ { + carr:> Type[0]; + eq0: equivalence_relation carr +}. + +(* activate non uniform coercions on: Type → setoid *) +unification hint 0 ≔ R : setoid; + MR ≟ carr R, + lock ≟ mk_lock1 Type[0] MR setoid R +(* ---------------------------------------- *) ⊢ + setoid ≡ force1 ? MR lock. + +interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y). + +notation > "hvbox(a break =_0 b)" non associative with precedence 45 +for @{ eq_rel ? (eq0 ?) $a $b }. + +interpretation "setoid symmetry" 'invert r = (sym ???? r). +notation ".= r" with precedence 50 for @{'trans $r}. +interpretation "trans" 'trans r = (trans ????? r). +notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}. +interpretation "trans_x0" 'trans_x0 r = (trans ????? r). + +nrecord unary_morphism (A,B: setoid) : Type[0] ≝ { + fun1:1> A → B; + prop1: ∀a,a'. a = a' → fun1 a = fun1 a' +}. + +notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}. +notation "hvbox(B break ⇒\sub 0 C)" right associative with precedence 72 for @{'umorph0 $B $C}. +interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B). + +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 "refl" 'refl = (refl ???). +notation "┼_0 c" with precedence 89 for @{'prop1_x0 $c }. +notation "l ╪_0 r" with precedence 89 for @{'prop2_x0 $l $r }. +interpretation "prop1_x0" 'prop1_x0 c = (prop1 ????? c). + +ndefinition unary_morph_setoid : setoid → setoid → setoid. +#S1; #S2; @ (S1 ⇒_0 S2); @; +##[ #f; #g; napply (∀x,x'. x=x' → f x = g x'); +##| #f; #x; #x'; #Hx; napply (.= †Hx); napply #; +##| #f; #g; #H; #x; #x'; #Hx; napply ((H … Hx^-1)^-1); +##| #f; #g; #h; #H1; #H2; #x; #x'; #Hx; napply (trans … (H1 …) (H2 …)); //; ##] +nqed. + +alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". +unification hint 0 ≔ o1,o2 ; + X ≟ unary_morph_setoid o1 o2 + (* ----------------------------- *) ⊢ + carr X ≡ o1 ⇒_0 o2. + +interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). +interpretation "prop2_x0" 'prop2_x0 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). -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; -##] +nlemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g. +#A B f g H x1 x2 E; napply (.= †E); napply H; nqed. + +nlemma mk_binary_morphism: + ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') → + A ⇒_0 (unary_morph_setoid B C). + #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y] + /2/. 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')) - }. +ndefinition composition ≝ + λo1,o2,o3:Type[0].λf:o2 → o3.λg: o1 → o2.λx.f (g x). +interpretation "function composition" 'compose f g = (composition ??? f g). + +ndefinition comp_unary_morphisms: + ∀o1,o2,o3:setoid.o2 ⇒_0 o3 → o1 ⇒_0 o2 → o1 ⇒_0 o3. +#o1; #o2; #o3; #f; #g; @ (f ∘ g); + #a; #a'; #e; nnormalize; napply (.= †(†e)); napply #. +nqed. -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); - | - | - | -*) -*******************) +unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2; + R ≟ mk_unary_morphism ?? (composition … f g) + (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g)) + (* -------------------------------------------------------------------- *) ⊢ + fun1 ?? R ≡ (composition … f g). + +ndefinition comp_binary_morphisms: + ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)). +#o1; #o2; #o3; napply mk_binary_morphism + [ #f; #g; napply (comp_unary_morphisms ??? f g) + (* CSC: why not ∘? + GARES: because the coercion to FunClass is not triggered if there + are no "extra" arguments. We could fix that in the refiner + *) + | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] +nqed.