helm/software/matita/library/formal_topology/relations.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 "datatypes/subsets.ma".
  16
  17 record ssigma (A:Type) (S: powerset A) : Type ≝
  18  { witness:> A;
  19    proof:> witness ∈ S
  20  }.
  21
  22 coercion ssigma.
  23
  24 record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝
  25  { satisfy:2> U → V → CProp }.
  26
  27 notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)"  with precedence 45 for @{'satisfy $r $x $y}.
  28 notation > "hvbox (x \natur term 90 r y)"  with precedence 45 for @{'satisfy $r $x $y}.
  29 interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y).
  30
  31 definition composition:
  32  ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C.
  33   binary_relation ?? U1 U2 → binary_relation ?? U2 U3 →
  34    binary_relation ?? U1 U3.
  35  intros (A B C U1 U2 U3 R12 R23);
  36  constructor 1;
  37  intros (s1 s3);
  38  apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
  39 qed.
  40
  41 interpretation "binary relation composition" 'compose x y = (composition ______ x y).
  42
  43 definition equal_relations ≝
  44  λA,B,U,V.λr,r': binary_relation A B U V.
  45   ∀x,y. r x y ↔ r' x y.
  46
  47 interpretation "equal relation" 'eq x y = (equal_relations ____ x y).
  48
  49 lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V).
  50  intros 5; intros 2; split; intro; assumption.
  51 qed.
  52
  53 lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V).
  54  intros 7; intros 2; split; intro;
  55   [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
  56 qed.
  57
  58 lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V).
  59  intros 9; intros 2; split; intro;
  60   [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
  61   [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
  62   assumption.
  63 qed.
  64
  65 lemma associative_composition:
  66  ∀A,B,C,D.∀U1,U2,U3,U4.
  67   ∀r1:binary_relation A B U1 U2.
  68    ∀r2:binary_relation B C U2 U3.
  69     ∀r3:binary_relation C D U3 U4.
  70      (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
  71  intros 13;
  72  split; intro;
  73  cases H; clear H; cases H1; clear H1;
  74  [cases H; clear H | cases H2; clear H2]
  75  cases H1; clear H1;
  76  exists; try assumption;
  77  split; try assumption;
  78  exists; try assumption;
  79  split; assumption.
  80 qed.
  81
  82 lemma composition_morphism:
  83  ∀A,B,C.∀U1,U2,U3.
  84   ∀r1,r1':binary_relation A B U1 U2.
  85    ∀r2,r2':binary_relation B C U2 U3.
  86     r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
  87  intros 14; split; intro;
  88  cases H2; clear H2; cases H3; clear H3;
  89  [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
  90  [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
  91  exists; try assumption;
  92  split; assumption.
  93 qed.
  94
  95 definition binary_relation_setoid: ∀A,B. Ω \sup A → Ω \sup B → setoid.
  96  intros (A B U V);
  97  constructor 1;
  98   [ apply (binary_relation ?? U V)
  99   | constructor 1;
 100      [ apply equal_relations
 101      | apply refl_equal_relations
 102      | apply sym_equal_relations
 103      | apply trans_equal_relations
 104      ]]
 105 qed.
 106
 107 record sigma (A:Type) (P: A → Type) : Type ≝
 108  { s_witness:> A;
 109    s_proof:> P s_witness
 110  }.
 111
 112 interpretation "sigma" 'sigma \eta.x = (sigma _ x).
 113
 114 definition REL: category.
 115  constructor 1;
 116   [ apply (ΣA:Type.Ω \sup A)
 117   | intros; apply (binary_relation_setoid ?? (s_proof ?? s) (s_proof ?? s1))
 118   | intros; constructor 1; intros; apply (s=s1)
 119   | intros; constructor 1;
 120      [ apply composition
 121      | apply composition_morphism
 122      ]
 123   | intros; unfold mk_binary_morphism; simplify;
 124     apply associative_composition
 125   |6,7: intros 5; simplify; split; intro;
 126      [1,3: cases H; clear H; cases H1; clear H1;
 127        [ rewrite > H | rewrite < H2 ]
 128        assumption
 129      |*: exists; try assumption; split; first [ reflexivity | assumption ]]]
 130 qed.