helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.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 "relations.ma".
  16 include "o-algebra.ma".
  17
  18 definition SUBSETS: objs1 SET → OAlgebra.
  19  intro A; constructor 1;
  20   [ apply (Ω \sup A);
  21   | apply subseteq;
  22   | apply overlaps;
  23   | apply big_intersects;
  24   | apply big_union;
  25   | apply ({x | True});
  26     simplify; intros; apply (refl1 ? (eq1 CPROP));
  27   | apply ({x | False});
  28     simplify; intros; apply (refl1 ? (eq1 CPROP));
  29   | intros; whd; intros; assumption
  30   | intros; whd; split; assumption
  31   | intros; apply transitive_subseteq_operator; [2: apply f; | skip | assumption]
  32   | intros; cases f; exists [apply w] assumption
  33   | intros; intros 2; apply (f ? f1 i);
  34   | intros; intros 2; apply f;
  35     (* senza questa change, universe inconsistency *)
  36     whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
  37     exists; [apply i] assumption;
  38   | intros 3; cases f;
  39   | intros 3; constructor 1;
  40   | intros; cases f; exists; [apply w]
  41      [ assumption
  42      | whd; intros; cases i; simplify; assumption]
  43   | intros; split; intro;
  44      [ cases f; cases x1;
  45        (* senza questa change, universe inconsistency *)
  46        change in ⊢ (? ? (λ_:%.?)) with (carr I);
  47        exists [apply w1] exists [apply w] assumption;
  48      | cases e; cases x; exists; [apply w1]
  49         [ assumption
  50         | (* senza questa change, universe inconsistency *)
  51           whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
  52           exists; [apply w] assumption]]
  53   | intros; intros 2; cases (f (singleton ? a) ?);
  54      [ exists; [apply a] [assumption | change with (a = a); apply refl1;]
  55      | change in x1 with (a = w); change with (mem A a q); apply (. (x1 \sup -1‡#));
  56        assumption]]
  57 qed.
  58
  59 definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (SUBSETS o1) (SUBSETS o2).
  60  intros;
  61  constructor 1;
  62   [ constructor 1;
  63      [ apply (λU.image ?? t U);
  64      | intros; apply (#‡e); ]
  65   | constructor 1;
  66      [ apply (λU.minus_star_image ?? t U);
  67      | intros; apply (#‡e); ]
  68   | constructor 1;
  69      [ apply (λU.star_image ?? t U);
  70      | intros; apply (#‡e); ]
  71   | constructor 1;
  72      [ apply (λU.minus_image ?? t U);
  73      | intros; apply (#‡e); ]
  74   | intros; split; intro;
  75      [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
  76        change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
  77        intros 4; apply f; exists; [apply a] split; assumption;
  78      | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
  79        change with (∀a. a ∈ image ?? t p → a ∈ q);
  80        intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
  81   | intros; split; intro;
  82      [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q);
  83        change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
  84        intros 4; apply f; exists; [apply a] split; assumption;
  85      | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
  86        change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
  87        intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
  88   | intros; split; intro; cases f; clear f;
  89      [ cases x; cases x2; clear x x2; exists; [apply w1]
  90         [ assumption;
  91         | exists; [apply w] split; assumption]
  92      | cases x1; cases x2; clear x1 x2; exists; [apply w1]
  93         [ exists; [apply w] split; assumption;
  94         | assumption; ]]]
  95 qed.
  96
  97 lemma orelation_of_relation_preserves_equality:
  98  ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. eq1 ? t t' → orelation_of_relation ?? t = orelation_of_relation ?? t'.
  99  intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
 100  simplify; whd in o1 o2;
 101   [ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a);
 102     apply (. #‡(e‡#));
 103   | change with (a1 ∈ minus_star_image ?? t' a → a1 ∈ minus_star_image ?? t a);
 104     apply (. #‡(e ^ -1‡#));
 105   | change with (a1 ∈ minus_image ?? t a → a1 ∈ minus_image ?? t' a);
 106     apply (. #‡(e‡#));
 107   | change with (a1 ∈ minus_image ?? t' a → a1 ∈ minus_image ?? t a);
 108     apply (. #‡(e ^ -1‡#));
 109   | change with (a1 ∈ image ?? t a → a1 ∈ image ?? t' a);
 110     apply (. #‡(e‡#));
 111   | change with (a1 ∈ image ?? t' a → a1 ∈ image ?? t a);
 112     apply (. #‡(e ^ -1‡#));
 113   | change with (a1 ∈ star_image ?? t a → a1 ∈ star_image ?? t' a);
 114     apply (. #‡(e‡#));
 115   | change with (a1 ∈ star_image ?? t' a → a1 ∈ star_image ?? t a);
 116     apply (. #‡(e ^ -1‡#)); ]
 117 qed.
 118
 119 lemma hint: ∀o1,o2:OA. Type_OF_setoid2 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
 120  intros; apply t;
 121 qed.
 122 coercion hint.
 123
 124 lemma orelation_of_relation_preserves_identity:
 125  ∀o1:REL. orelation_of_relation ?? (id1 ? o1) = id2 OA (SUBSETS o1).
 126  intros; split; intro; split; whd; intro;
 127   [ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros;
 128     apply (f a1); change with (a1 = a1); apply refl1;
 129   | change with (a1 ∈ a → ∀x. x ♮(id1 REL o1) a1→x∈a); intros;
 130     change in f1 with (x = a1); apply (. f1 ^ -1‡#); apply f;
 131   | alias symbol "and" = "and_morphism".
 132     change with ((∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a) → a1 ∈ a);
 133     intro; cases e; clear e; cases x; clear x; change in f with (a1=w);
 134     apply (. f^-1‡#); apply f1;
 135   | change with (a1 ∈ a → ∃y: carr o1.a1 ♮(id1 REL o1) y ∧ y∈a);
 136     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
 137   | change with ((∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a) → a1 ∈ a);
 138     intro; cases e; clear e; cases x; clear x; change in f with (w=a1);
 139     apply (. f‡#); apply f1;
 140   | change with (a1 ∈ a → ∃x: carr o1.x ♮(id1 REL o1) a1∧x∈a);
 141     intro; exists; [apply a1]; split; [ change with (a1=a1); apply refl1; | apply f]
 142   | change with ((∀y.a1 ♮(id1 REL o1) y→y∈a) → a1 ∈ a); intros;
 143     apply (f a1); change with (a1 = a1); apply refl1;
 144   | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
 145     change in f1 with (a1 = y); apply (. f1‡#); apply f;]
 146 qed.
 147
 148 lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid2 (arrows2 OA S T).
 149  intros; apply c;
 150 qed.
 151 coercion hint2.
 152
 153 (* CSC: ???? forse un uncertain mancato *)
 154 lemma orelation_of_relation_preserves_composition:
 155  ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
 156   orelation_of_relation ?? (G ∘ F) =
 157    comp2 OA (SUBSETS o1) (SUBSETS o2) (SUBSETS o3)
 158     ?? (*(orelation_of_relation ?? F) (orelation_of_relation ?? G)*).
 159  [ apply (orelation_of_relation ?? F); | apply (orelation_of_relation ?? G); ]
 160  intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros;
 161   [ whd; intros; apply f; exists; [ apply x] split; assumption;
 162   | cases f1; clear f1; cases x1; clear x1; apply (f w); assumption;
 163   | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ]
 164     split; [ assumption | exists; [apply w] split; assumption ]
 165   | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
 166     split; [ exists; [apply w] split; assumption | assumption ]
 167   | cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ]
 168     split; [ assumption | exists; [apply w] split; assumption ]
 169   | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
 170     split; [ exists; [apply w] split; assumption | assumption ]
 171   | whd; intros; apply f; exists; [ apply y] split; assumption;
 172   | cases f1; clear f1; cases x; clear x; apply (f w); assumption;]
 173 qed.