include "sets/sets.ma".
nrecord magma_type : Type[1] ≝
- { carr:> Type;
- op: carr → carr → carr
+ { mcarr:> setoid;
+ op: mcarr → mcarr → mcarr
}.
nrecord magma (A: magma_type) : Type[1] ≝
- { mcarr:> Ω \sup A;
+ { mcarr:> powerset_setoid1 A;
op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
}.
-sets/sets.ma logic/equality.ma
-sets/setoids1.ma sets/setoids.ma
+sets/sets.ma sets/setoids.ma sets/setoids1.ma
+logic/cprop.ma sets/setoids1.ma
+sets/setoids1.ma properties/relations1.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
-algebra/magmas.ma sets/sets.ma
+algebra/magmas.ma sets/setoids.ma
+properties/relations1.ma logic/pts.ma
properties/relations.ma logic/pts.ma
logic/pts.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/setoids1.ma".
+
+ndefinition CPROP: setoid1.
+ napply mk_setoid1
+ [ napply CProp[0]
+ | napply (mk_equivalence_relation1 CProp[0])
+ [ napply iff
+ | #x; napply mk_iff; #H; nassumption
+ | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
+ | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
+ [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
+nqed.
+
+unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
+
+(*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
+ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
+ on _x: carr1 CPROP to CProp[0].*)
+
+alias symbol "eq" = "setoid1 eq".
+
+ndefinition fi': ∀A,B:CPROP. A = B → B → A.
+ #A; #B; #H; napply (fi … H); nassumption.
+nqed.
+
+notation ". r" with precedence 50 for @{'fi $r}.
+interpretation "fi" 'fi r = (fi' ?? r).
+
+ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+ [ napply And
+ | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
+ [ napply (H1 K1)
+ | napply (H3 K2)
+ | napply (H2 K1)
+ | napply (H4 K2)]##]
+nqed.
+
+unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
+
+(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2;
+ napply (. ((#‡H1)‡H2^-1)); nnormalize;
+nqed.*)
+
+(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
+
+ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+ [ napply Or
+ | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
+ ##[##1,3: napply or_introl |##*: napply or_intror ]
+ ##[ napply (H1 H)
+ | napply (H2 H)
+ | napply (H3 H)
+ | napply (H4 H)]##]
+nqed.
+
+unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
+
+(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
+
+ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+ [ napply (λA,B. A → B)
+ | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
+ [ napply (if … H2); napply H; napply (fi … H1); nassumption
+ | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
+nqed.
\ No newline at end of file
(* *)
(**************************************************************************)
-universe constraint Type[0] < Type[1].
-universe constraint CProp[0] < CProp[1].
universe constraint Type[0] ≤ CProp[0].
universe constraint CProp[0] ≤ Type[0].
+
universe constraint Type[1] ≤ CProp[1].
universe constraint CProp[1] ≤ Type[1].
+
+universe constraint Type[2] ≤ CProp[2].
+universe constraint CProp[2] ≤ Type[2].
+
+universe constraint Type[0] < Type[1].
+universe constraint CProp[0] < CProp[1].
+
+universe constraint Type[1] < Type[2].
+universe constraint CProp[1] < CProp[2].
\ No newline at end of file
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.
+ndefinition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
+ndefinition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
+ndefinition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
+
+nrecord equivalence_relation (A:Type[0]) : Type[1] ≝
+ { eq_rel:2> A → A → CProp[0];
+ refl: reflexive ? eq_rel;
+ sym: symmetric ? eq_rel;
+ trans: transitive ? eq_rel
+ }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 reflexive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x.P x x.
+ndefinition symmetric1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x,y.P x y → P y x.
+ndefinition transitive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀z,x,y. P x z → P z y → P x y.
+
+nrecord equivalence_relation1 (A:Type[1]) : Type[2] ≝
+ { eq_rel1:2> A → A → CProp[1];
+ refl1: reflexive1 ? eq_rel1;
+ sym1: symmetric1 ? eq_rel1;
+ trans1: transitive1 ? eq_rel1
+ }.
include "logic/connectives.ma".
include "properties/relations.ma".
-nrecord setoid : Type[1] ≝
- { carr:> Type;
- eq: carr → carr → CProp;
- refl: reflexive … eq;
- sym: symmetric … eq;
- trans: transitive … eq
- }.
+(*
+notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
+for @{ 'eqID $a $b }.
+
+notation > "hvbox(a break =_\ID b)" non associative with precedence 45
+for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
-ndefinition proofs: CProp → setoid.
-#P; napply mk_setoid;
-##[ napply P;
-##| #x; #y; napply True;
-##|##*: nwhd; nrepeat (#_); napply I;
-##]
-nqed.
+interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
+*)
-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'))
+nrecord setoid : Type[1] ≝
+ { carr:> Type[0];
+ eq: equivalence_relation carr
}.
-notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
-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)));
-##| nnormalize; #x; #a; napply (f_ok … x); napply refl
- | nnormalize; #x; #y; #H; #a; napply sym; napply H
- | nnormalize; #z; #x; #y; #H1; #H2; #a;
- napply trans; ##[##2: napply H1 | ##skip | napply H2]##]
-nqed.
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans" 'trans r = (trans ????? r).
-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);
- 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).
+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')
+ }.
-(*
-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')))
- }.*)
-
- *)
\ No newline at end of file
+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 ???).
(* *)
(**************************************************************************)
+include "properties/relations1.ma".
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
+nrecord setoid1: Type[2] ≝
+ { carr1:> Type[1];
+ eq1: equivalence_relation1 carr1
}.
-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'))
+ndefinition setoid1_of_setoid: setoid → setoid1.
+ #s; napply mk_setoid1
+ [ napply (carr s)
+ | napply (mk_equivalence_relation1 s)
+ [ napply eq
+ | napply refl
+ | napply sym
+ | napply trans]##]
+nqed.
+
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
+ on _s: setoid to setoid1.
+(*prefer coercion Type_OF_setoid.*)
+
+interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+
+notation > "hvbox(a break =_12 b)" non associative with precedence 45
+for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
+notation > "hvbox(a break =_1 b)" non associative with precedence 45
+for @{ eq_rel1 ? (eq1 ?) $a $b }.
+
+interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans1" 'trans r = (trans1 ????? r).
+interpretation "trans" 'trans r = (trans ????? r).
+
+nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
+ { fun11:1> A → B;
+ prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 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);
- |
- |
- |
+nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝
+ { fun21:2> A → B → C;
+ prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b')
+ }.
-*)
+interpretation "prop11" 'prop1 c = (prop11 ????? c).
+interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
+interpretation "refl1" 'refl = (refl1 ???).
(* *)
(**************************************************************************)
-include "logic/equality.ma".
+include "logic/cprop.ma".
-nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
+nrecord powerset (A: setoid) : Type[1] ≝ { mem_op: unary_morphism1 A CPROP }.
interpretation "powerset" 'powerset A = (powerset A).
-interpretation "subset construction" 'subset \eta.x = (mk_powerset ? x).
+interpretation "subset construction" 'subset \eta.x =
+ (mk_powerset ? (mk_unary_morphism1 ? CPROP x ?)).
-interpretation "mem" 'mem a S = (mem ? S a).
+interpretation "mem" 'mem a S = (mem_op ? S a).
-ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
+ndefinition subseteq ≝ λA:setoid.λU,V.∀a:A. a ∈ U → a ∈ V.
interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
napply H23; napply H12; nassumption;
nqed.
+ndefinition powerset_setoid1: setoid → setoid1.
+ #S; napply mk_setoid1
+ [ napply (Ω \sup S)
+ | napply mk_equivalence_relation1
+ [ #A; #B; napply (∀x. iff (x ∈ A) (x ∈ B))
+ | nnormalize; #x; #x0; napply mk_iff; #H; nassumption
+ | nnormalize; #x; #y; #H; #A; napply mk_iff; #K
+ [ napply (fi ?? (H ?)) | napply (if ?? (H ?)) ]
+ nassumption
+ | nnormalize; #A; #B; #C; #H1; #H2; #H3; napply mk_iff; #H4
+ [ napply (if ?? (H2 ?)); napply (if ?? (H1 ?)); nassumption
+ | napply (fi ?? (H1 ?)); napply (fi ?? (H2 ?)); nassumption]##]
+nqed.
+
+unification hint 0 (∀A.(λx,y.True) (Ω \sup A) (carr1 (powerset_setoid1 A))).
+
+ndefinition mem: ∀A:setoid. binary_morphism1 A (powerset_setoid1 A) CPROP.
+ #A; napply mk_binary_morphism1
+ [ napply (λa.λA.a ∈ A)
+ | #a; #a'; #B; #B'; #Ha; #HB; napply mk_iff; #H
+ [ napply (. (†Ha^-1)); (* CSC: notation for ∈ not working *)
+ napply (if ?? (HB ?)); nassumption
+ | napply (. (†Ha)); napply (fi ?? (HB ?)); nassumption]##]
+nqed.
+
+unification hint 0 (∀A,x,S. (λx,y.True) (mem_op A x S) (fun21 ??? (mem A) S x)).
+
ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
ndefinition intersects ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∧ x ∈ V }.
+ #a; #a'; #H; napply mk_iff; *; #H1; #H2
+ [ napply (. ((H^-1‡#)‡(H^-1‡#))); nnormalize; napply conj; nassumption
+ | napply (. ((H‡#)‡(H‡#))); nnormalize; napply conj; nassumption]
+nqed.
+
+(*interpretation "intersects" 'intersects U V = (intersects ? U V).*)
-interpretation "intersects" 'intersects U V = (intersects ? U V).
-
+(*
ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }.
interpretation "union" 'union U V = (union ? U V).
-ndefinition singleton ≝ λA.λa:A.{b | a=b}.
+ndefinition singleton ≝ λA:setoid.λa:A.{b | a=b}.
-interpretation "singleton" 'singl a = (singleton ? a).
+interpretation "singleton" 'singl a = (singleton ? a).*)
\ No newline at end of file
projects / helm.git / commitdiff