helm/software/matita/library/datatypes/subsets.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/cprop_connectives.ma".
  16
  17 record powerset (A: Type) : Type ≝ { char: A → CProp }.
  18
  19 interpretation "powerset" 'powerset A = (powerset A).
  20
  21 interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
  22
  23 definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
  24
  25 interpretation "mem" 'mem a S = (mem _ S a).
  26
  27 definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
  28
  29 interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
  30
  31 definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
  32
  33 interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
  34
  35 definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
  36
  37 interpretation "intersects" 'intersects U V = (intersects _ U V).
  38
  39 definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
  40
  41 interpretation "union" 'union U V = (union _ U V).
  42
  43 record ssigma (A:Type) (S: powerset A) : Type ≝
  44  { witness:> A;
  45    proof:> witness ∈ S
  46  }.
  47
  48 coercion ssigma.
  49
  50 record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝
  51  { satisfy:2> U → V → CProp }.
  52
  53 (*notation < "hvbox (x  (\circ term 19 r \frac \nbsp \circ) y)"  with precedence 45 for @{'satisfy $r $x $y}.*)
  54 notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)"  with precedence 45 for @{'satisfy $r $x $y}.
  55 notation > "hvbox (x \natur term 90 r y)"  with precedence 45 for @{'satisfy $r $x $y}.
  56 interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y).
  57
  58 definition composition:
  59  ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C.
  60   binary_relation ?? U1 U2 → binary_relation ?? U2 U3 →
  61    binary_relation ?? U1 U3.
  62  intros (A B C U1 U2 U3 R12 R23);
  63  constructor 1;
  64  intros (s1 s3);
  65  apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
  66 qed.
  67
  68 interpretation "binary relation composition" 'compose x y = (composition ______ x y).
  69
  70 definition equal_relations ≝
  71  λA,B,U,V.λr,r': binary_relation A B U V.
  72   ∀x,y. r x y ↔ r' x y.
  73
  74 interpretation "equal relation" 'eq x y = (equal_relations ____ x y).
  75
  76 lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V).
  77  intros 5; intros 2; split; intro; assumption.
  78 qed.
  79
  80 lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V).
  81  intros 7; intros 2; split; intro;
  82   [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
  83 qed.
  84
  85 lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V).
  86  intros 9; intros 2; split; intro;
  87   [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
  88   [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
  89   assumption.
  90 qed.
  91
  92 lemma equal_morphism:
  93  ∀A,B,U,V.∀r1,r1',r2,r2':binary_relation A B U V.
  94   r1' = r1 → r2 = r2' → r1 = r2 → r1' = r2'.
  95  intros 13;
  96  split; intro;
  97   [ apply (if ?? (H1 ??));
  98     apply (if ?? (H2 ??));
  99     apply (if ?? (H ??));
 100     assumption
 101   | apply (fi ?? (H ??));
 102     apply (fi ?? (H2 ??));
 103     apply (fi ?? (H1 ??));
 104     assumption
 105   ]
 106 qed.
 107
 108 lemma associative_composition:
 109  ∀A,B,C,D.∀U1,U2,U3,U4.
 110   ∀r1:binary_relation A B U1 U2.
 111    ∀r2:binary_relation B C U2 U3.
 112     ∀r3:binary_relation C D U3 U4.
 113      (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
 114  intros 13;
 115  split; intro;
 116  cases H; clear H; cases H1; clear H1;
 117  [cases H; clear H | cases H2; clear H2]
 118  cases H1; clear H1;
 119  exists; try assumption;
 120  split; try assumption;
 121  exists; try assumption;
 122  split; assumption.
 123 qed.
 124
 125 lemma composition_morphism:
 126  ∀A,B,C.∀U1,U2,U3.
 127   ∀r1,r1':binary_relation A B U1 U2.
 128    ∀r2,r2':binary_relation B C U2 U3.
 129     r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
 130  intros 14; split; intro;
 131  cases H2; clear H2; cases H3; clear H3;
 132  [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
 133  [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
 134  exists; try assumption;
 135  split; assumption.
 136 qed.
 137
 138 include "logic/equality.ma".
 139
 140 definition singleton ≝ λA:Type.λa:A.{b | a=b}.
 141
 142 interpretation "singleton" 'singl a = (singleton _ a).