helm/software/matita/library/formal_topology/basic_pairs.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 include "logic/cprop_connectives.ma".
  17 include "formal_topology/categories.ma".
  18
  19 record basic_pair: Type ≝
  20  { carr1: Type;
  21    carr2: Type;
  22    concr: Ω \sup carr1;
  23    form: Ω \sup carr2;
  24    rel: binary_relation ?? concr form
  25  }.
  26
  27 notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
  28 notation "⊩" with precedence 60 for @{'Vdash}.
  29
  30 interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
  31 interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
  32
  33 alias symbol "eq" = "equal relation".
  34 alias symbol "compose" = "binary relation composition".
  35 record relation_pair (BP1,BP2: basic_pair): Type ≝
  36  { concr_rel: binary_relation ?? (concr BP1) (concr BP2);
  37    form_rel: binary_relation ?? (form BP1) (form BP2);
  38    commute: concr_rel ∘ ⊩ = ⊩ ∘ form_rel
  39  }.
  40
  41 notation "hvbox (r \sub \c)"  with precedence 90 for @{'concr_rel $r}.
  42 notation "hvbox (r \sub \f)"  with precedence 90 for @{'form_rel $r}.
  43
  44 interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
  45 interpretation "formal relation" 'form_rel r = (form_rel __ r).
  46
  47
  48 definition relation_pair_equality:
  49  ∀o1,o2. equivalence_relation (relation_pair o1 o2).
  50  intros;
  51  constructor 1;
  52   [ apply (λr,r'. r \sub\c ∘ ⊩ = r' \sub\c ∘ ⊩);
  53   | simplify;
  54     intros;
  55     apply refl_equal_relations;
  56   | simplify;
  57     intros;
  58     apply sym_equal_relations;
  59     assumption
  60   | simplify;
  61     intros;
  62     apply (trans_equal_relations ??????? H);
  63     assumption
  64   ]
  65 qed.
  66
  67 definition relation_pair_setoid: basic_pair → basic_pair → setoid.
  68  intros;
  69  constructor 1;
  70   [ apply (relation_pair b b1)
  71   | apply relation_pair_equality
  72   ]
  73 qed.
  74
  75 definition eq' ≝
  76  λo1,o2.λr,r':relation_pair o1 o2.⊩ ∘ r \sub\f = ⊩ ∘ r' \sub\f.
  77
  78 alias symbol "eq" = "setoid eq".
  79 lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → eq' ?? r r'.
  80  intros 7 (o1 o2 r r' H c1 f2);
  81  split; intro;
  82   [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
  83     lapply (if ?? (H c1 f2) H2) as H3;
  84     apply (if ?? (commute ?? r' c1 f2) H3);
  85   | lapply (fi ?? (commute ?? r' c1 f2) H1) as H2;
  86     lapply (fi ?? (H c1 f2) H2) as H3;
  87     apply (if ?? (commute ?? r c1 f2) H3);
  88   ]
  89 qed.
  90
  91
  92 definition id: ∀o:basic_pair. relation_pair o o.
  93  intro;
  94  constructor 1;
  95   [1,2: constructor 1;
  96     intros;
  97     apply (s=s1)
  98   | simplify; intros;
  99     split;
 100     intro;
 101     cases H;
 102     cases H1; clear H H1;
 103      [ exists [ apply y ]
 104        split
 105         [ rewrite > H2; assumption
 106         | reflexivity ]
 107      | exists [ apply x ]
 108        split
 109         [2: rewrite < H3; assumption
 110         | reflexivity ]]]
 111 qed.
 112
 113 definition relation_pair_composition:
 114  ∀o1,o2,o3. binary_morphism (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
 115  intros;
 116  constructor 1;
 117   [ intros (r r1);
 118     constructor 1;
 119      [ apply (r \sub\c ∘ r1 \sub\c)
 120      | apply (r \sub\f ∘ r1 \sub\f)
 121      | lapply (commute ?? r) as H;
 122        lapply (commute ?? r1) as H1;
 123        apply (equal_morphism ???? (r\sub\c ∘ (r1\sub\c ∘ ⊩)) ? ((⊩ ∘ r\sub\f) ∘ r1\sub\f));
 124         [1,2: apply associative_composition]
 125        apply (equal_morphism ???? (r\sub\c ∘ (⊩ ∘ r1\sub\f)) ? ((r\sub\c ∘ ⊩) ∘ r1\sub\f));
 126         [1,2: apply composition_morphism; first [assumption | apply refl_equal_relations]
 127         | apply sym_equal_relations;
 128           apply associative_composition
 129         ]]
 130   | intros;
 131     alias symbol "eq" = "equal relation".
 132     change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩);
 133     apply (equal_morphism ???? (a\sub\c ∘ (b\sub\c ∘ ⊩)) ? (a'\sub\c ∘ (b'\sub\c ∘ ⊩)));
 134      [ apply associative_composition
 135      | apply sym_equal_relations; apply associative_composition]
 136     apply (equal_morphism ???? (a\sub\c ∘ (b'\sub\c ∘ ⊩)) ? (a' \sub \c∘(b' \sub \c∘⊩)));
 137      [2: apply refl_equal_relations;
 138      |1: apply composition_morphism;
 139           [ apply refl_equal_relations
 140           | assumption]]
 141     apply (equal_morphism ???? (a\sub\c ∘ (⊩ ∘ b'\sub\f)) ? (a'\sub\c ∘ (⊩ ∘ b'\sub\f)));
 142      [1,2: apply composition_morphism;
 143        [1,3: apply refl_equal_relations
 144        | apply (commute ?? b');
 145        | apply sym_equal_relations; apply (commute ?? b');]]
 146     apply (equal_morphism ???? ((a\sub\c ∘ ⊩) ∘ b'\sub\f) ? ((a'\sub\c ∘ ⊩) ∘ b'\sub\f));
 147      [2: apply associative_composition
 148      |1: apply sym_equal_relations; apply associative_composition]
 149     apply composition_morphism;
 150      [ assumption
 151      | apply refl_equal_relations]]
 152 qed.
 153
 154 definition BP: category.
 155  constructor 1;
 156   [ apply basic_pair
 157   | apply relation_pair_setoid
 158   | apply id
 159   | apply relation_pair_composition
 160   | intros;
 161     change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ =
 162                  (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩));
 163     apply composition_morphism;
 164      [2: apply refl_equal_relations]
 165     apply associative_composition
 166   | intros;
 167     change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
 168     apply composition_morphism;
 169      [2: apply refl_equal_relations]
 170     intros 2; unfold id; simplify;
 171     split; intro;
 172      [ cases H; cases H1; rewrite > H2; assumption
 173      | exists; [assumption] split; [reflexivity| assumption]]
 174   | intros;
 175     change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
 176     apply composition_morphism;
 177      [2: apply refl_equal_relations]
 178     intros 2; unfold id; simplify;
 179     split; intro;
 180      [ cases H; cases H1; rewrite < H3; assumption
 181      | exists; [assumption] split; [assumption|reflexivity]]
 182   ]
 183 qed.