helm/software/matita/nlibrary/topology/igt.ma

   1 include "logic/connectives.ma".
   2 include "properties/relations.ma".
   3
   4 nrecord iff (A,B: CProp) : CProp ≝
   5  { if: A → B;
   6    fi: B → A
   7  }.
   8
   9 notation > "hvbox(a break \liff b)"
  10   left associative with precedence 25
  11 for @{ 'iff $a $b }.
  12
  13 notation "hvbox(a break \leftrightarrow b)"
  14   left associative with precedence 25
  15 for @{ 'iff $a $b }.
  16
  17 interpretation "logical iff" 'iff x y = (iff x y).
  18
  19 nrecord setoid : Type[1] ≝
  20  { carr:> Type;
  21    eq: carr → carr → CProp;
  22    refl: reflexive ? eq;
  23    sym: symmetric ? eq;
  24    trans: transitive ? eq
  25  }.
  26
  27 ndefinition proofs: CProp → setoid.
  28 #P; napply (mk_setoid ?????);
  29 ##[ napply P;
  30 ##| #x; #y; napply True;
  31 ##|##*: nwhd; nrepeat (#_); napply I;
  32 ##]
  33 nqed.
  34
  35 (*
  36 definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
  37 definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
  38 definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
  39
  40 record setoid1 : Type ≝
  41  { carr1:> Type;
  42    eq1: carr1 → carr1 → CProp;
  43    refl1: reflexive1 ? eq1;
  44    sym1: symmetric1 ? eq1;
  45    trans1: transitive1 ? eq1
  46  }.
  47
  48 definition proofs1: CProp → setoid1.
  49  intro;
  50  constructor 1;
  51   [ apply A
  52   | intros;
  53     apply True
  54   | intro;
  55     constructor 1
  56   | intros 3;
  57     constructor 1
  58   | intros 5;
  59     constructor 1]
  60 qed.
  61 *)
  62
  63 (*
  64 ndefinition CCProp: setoid1.
  65  constructor 1;
  66   [ apply CProp
  67   | apply iff
  68   | intro;
  69     split;
  70     intro;
  71     assumption
  72   | intros 3;
  73     cases H; clear H;
  74     split;
  75     assumption
  76   | intros 5;
  77     cases H; cases H1; clear H H1;
  78     split;
  79     intros;
  80     [ apply (H4 (H2 H))
  81     | apply (H3 (H5 H))]]
  82 qed.
  83
  84 *)
  85
  86 nrecord function_space (A,B: setoid): Type[1] ≝
  87  { f:1> carr A → carr B}.;
  88    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  89  }.
  90
  91
  92 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
  93
  94 (*
  95 record function_space1 (A: setoid1) (B: setoid1): Type ≝
  96  { f1:1> A → B;
  97    f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
  98  }.
  99 *)
 100
 101 definition function_space_setoid: setoid → setoid → setoid.
 102  intros (A B);
 103  constructor 1;
 104   [ apply (function_space A B);
 105   | intros;
 106     apply (∀a:A. proofs (eq ? (f a) (f1 a)));
 107   | simplify;
 108     intros;
 109     apply (f_ok ? ? x);
 110     unfold carr; unfold proofs; simplify;
 111     apply (refl A)
 112   | simplify;
 113     intros;
 114     unfold carr; unfold proofs; simplify;
 115     apply (sym B);
 116     apply (f a)
 117   | simplify;
 118     intros;
 119     unfold carr; unfold proofs; simplify;
 120     apply (trans B ? (y a));
 121     [ apply (f a)
 122     | apply (f1 a)]]
 123 qed.
 124
 125 definition function_space_setoid1: setoid1 → setoid1 → setoid1.
 126  intros (A B);
 127  constructor 1;
 128   [ apply (function_space1 A B);
 129   | intros;
 130     apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
 131   |*: cases daemon] (* simplify;
 132     intros;
 133     apply (f1_ok ? ? x);
 134     unfold proofs; simplify;
 135     apply (refl1 A)
 136   | simplify;
 137     intros;
 138     unfold proofs; simplify;
 139     apply (sym1 B);
 140     apply (f a)
 141   | simplify;
 142     intros;
 143     unfold carr; unfold proofs; simplify;
 144     apply (trans1 B ? (y a));
 145     [ apply (f a)
 146     | apply (f1 a)]] *)
 147 qed.
 148
 149 interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
 150
 151 record isomorphism (A,B: setoid): Type ≝
 152  { map1:> function_space_setoid A B;
 153    map2:> function_space_setoid B A;
 154    inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
 155    inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
 156  }.
 157
 158 interpretation "isomorphism" 'iff x y = (isomorphism x y).
 159
 160 definition setoids: setoid1.
 161  constructor 1;
 162   [ apply setoid;
 163   | apply isomorphism;
 164   | intro;
 165     split;
 166      [1,2: constructor 1;
 167         [1,3: intro; assumption;
 168         |*: intros; assumption]
 169      |3,4:
 170        intros;
 171        simplify;
 172        unfold proofs; simplify;
 173        apply refl;]
 174   |*: cases daemon]
 175 qed.
 176
 177 definition setoid1_of_setoid: setoid → setoid1.
 178  intro;
 179  constructor 1;
 180   [ apply (carr s)
 181   | apply (eq s)
 182   | apply (refl s)
 183   | apply (sym s)
 184   | apply (trans s)]
 185 qed.
 186
 187 coercion setoid1_of_setoid.
 188
 189 (*
 190 record dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
 191  { dp:> ∀a:A.carr (B a);
 192    dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
 193  }.*)
 194
 195 record forall (A:setoid)  (B: A ⇒ CCProp): CProp ≝
 196  { fo:> ∀a:A.proofs (B a) }.
 197
 198 record subset (A: setoid) : CProp ≝
 199  { mem: A ⇒ CCProp }.
 200
 201 definition ssubset: setoid → setoid1.
 202  intro;
 203  constructor 1;
 204   [ apply (subset s);
 205   | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
 206   | simplify;
 207     intros;
 208     split;
 209     intro;
 210     assumption
 211   | simplify;
 212     cases daemon
 213   | cases daemon]
 214 qed.
 215
 216 definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp.
 217  intros;
 218  constructor 1;
 219   [ apply mem;
 220   | unfold function_space_setoid1; simplify;
 221     intros (b b');
 222     change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
 223     unfold proofs1; simplify; intros;
 224     unfold proofs1 in c; simplify in c;
 225     unfold ssubset in c; simplify in c;
 226     cases (c a); clear c;
 227     split;
 228     assumption]
 229 qed.
 230
 231 (*
 232 definition sand: CCProp ⇒ CCProp.
 233
 234 definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
 235  intro;
 236  constructor 1;
 237   [ intro;
 238     constructor 1;
 239      [ intro;
 240        constructor 1;
 241        constructor 1;
 242        intro;
 243        apply (mem ? c c2 ∧ mem ? c1 c2);
 244      |
 245   |
 246   |
 247 *)