From: Claudio Sacerdoti Coen Date: Sun, 31 Aug 2008 23:43:25 +0000 (+0000) Subject: Relations are now closer to Sambin's ones. I.e. they range over Types X-Git-Tag: make_still_working~4829 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=42e87a2db149c53be4001e0f3c46ad2fa0a9579e;p=helm.git Relations are now closer to Sambin's ones. I.e. they range over Types and not (sub)sets. --- diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma index e67b2ce7c..033788e92 100644 --- a/helm/software/matita/library/formal_topology/relations.ma +++ b/helm/software/matita/library/formal_topology/relations.ma @@ -14,61 +14,54 @@ include "datatypes/subsets.ma". -record ssigma (A:Type) (S: powerset A) : Type ≝ - { witness:> A; - proof:> witness ∈ S - }. - -coercion ssigma. - -record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝ - { satisfy:2> U → V → CProp }. +record binary_relation (A,B: Type) : Type ≝ + { satisfy:2> A → B → CProp }. notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)" with precedence 45 for @{'satisfy $r $x $y}. notation > "hvbox (x \natur term 90 r y)" with precedence 45 for @{'satisfy $r $x $y}. -interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y). +interpretation "relation applied" 'satisfy r x y = (satisfy __ r x y). definition composition: - ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C. - binary_relation ?? U1 U2 → binary_relation ?? U2 U3 → - binary_relation ?? U1 U3. - intros (A B C U1 U2 U3 R12 R23); + ∀A,B,C. + binary_relation A B → binary_relation B C → + binary_relation A C. + intros (A B C R12 R23); constructor 1; intros (s1 s3); apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3); qed. -interpretation "binary relation composition" 'compose x y = (composition ______ x y). +interpretation "binary relation composition" 'compose x y = (composition ___ x y). definition equal_relations ≝ - λA,B,U,V.λr,r': binary_relation A B U V. + λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y. -interpretation "equal relation" 'eq x y = (equal_relations ____ x y). +interpretation "equal relation" 'eq x y = (equal_relations __ x y). -lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V). - intros 5; intros 2; split; intro; assumption. +lemma refl_equal_relations: ∀A,B. reflexive ? (equal_relations A B). + intros 3; intros 2; split; intro; assumption. qed. -lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V). - intros 7; intros 2; split; intro; +lemma sym_equal_relations: ∀A,B. symmetric ? (equal_relations A B). + intros 5; intros 2; split; intro; [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption. qed. -lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V). - intros 9; intros 2; split; intro; +lemma trans_equal_relations: ∀A,B. transitive ? (equal_relations A B). + intros 7; intros 2; split; intro; [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ] [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ] assumption. qed. lemma associative_composition: - ∀A,B,C,D.∀U1,U2,U3,U4. - ∀r1:binary_relation A B U1 U2. - ∀r2:binary_relation B C U2 U3. - ∀r3:binary_relation C D U3 U4. + ∀A,B,C,D. + ∀r1:binary_relation A B. + ∀r2:binary_relation B C. + ∀r3:binary_relation C D. (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3). - intros 13; + intros 9; split; intro; cases H; clear H; cases H1; clear H1; [cases H; clear H | cases H2; clear H2] @@ -80,11 +73,11 @@ lemma associative_composition: qed. lemma composition_morphism: - ∀A,B,C.∀U1,U2,U3. - ∀r1,r1':binary_relation A B U1 U2. - ∀r2,r2':binary_relation B C U2 U3. + ∀A,B,C. + ∀r1,r1':binary_relation A B. + ∀r2,r2':binary_relation B C. r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'. - intros 14; split; intro; + intros 11; split; intro; cases H2; clear H2; cases H3; clear H3; [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ] [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ] @@ -92,10 +85,10 @@ lemma composition_morphism: split; assumption. qed. -definition binary_relation_setoid: ∀A,B. Ω \sup A → Ω \sup B → setoid. - intros (A B U V); +definition binary_relation_setoid: Type → Type → setoid. + intros (A B); constructor 1; - [ apply (binary_relation ?? U V) + [ apply (binary_relation A B) | constructor 1; [ apply equal_relations | apply refl_equal_relations @@ -104,18 +97,11 @@ definition binary_relation_setoid: ∀A,B. Ω \sup A → Ω \sup B → setoid. ]] qed. -record sigma (A:Type) (P: A → Type) : Type ≝ - { s_witness:> A; - s_proof:> P s_witness - }. - -interpretation "sigma" 'sigma \eta.x = (sigma _ x). - definition REL: category. constructor 1; - [ apply (ΣA:Type.Ω \sup A) - | intros; apply (binary_relation_setoid ?? (s_proof ?? s) (s_proof ?? s1)) - | intros; constructor 1; intros; apply (s=s1) + [ apply Type + | intros; apply (binary_relation_setoid T T1) + | intros; constructor 1; intros; apply (eq ? o1 o2); | intros; constructor 1; [ apply composition | apply composition_morphism @@ -124,22 +110,16 @@ definition REL: category. apply associative_composition |6,7: intros 5; simplify; split; intro; [1,3: cases H; clear H; cases H1; clear H1; - [ rewrite > H | rewrite < H2 ] + [ alias id "eq_elim_r''" = "cic:/matita/logic/equality/eq_elim_r''.con". + apply (eq_elim_r'' ? w ?? x H); assumption + | alias id "eq_rect" = "cic:/matita/logic/equality/eq_rect.con". + apply (eq_rect ? w ?? y H2); assumption ] assumption - |*: exists; try assumption; split; first [ reflexivity | assumption ]]] + |*: exists; try assumption; split; + alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)". + first [ apply refl_eq | assumption ]]] qed. -definition elements: objs REL → Type ≝ - λb:ΣA.Ω\sup A.ssigma (s_witness ?? b) (s_proof ?? b). - -coercion elements. - -definition carrier: objs REL → Type ≝ - λb:ΣA.Ω\sup A.s_witness ?? b. - -interpretation "REL carrier" 'card c = (carrier c). - -definition subset: ∀b:objs REL. Ω \sup (carrier b) ≝ - λb:ΣA.Ω\sup A.s_proof ?? b. +definition full_subset: ∀s:REL. Ω \sup s ≝ λs.{x | True}. -coercion subset. +coercion full_subset. \ No newline at end of file