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 (************************CSC
  87 nrecord function_space (A,B: setoid): Type[1] ≝
  88  { f:1> carr A → carr B}.;
  89    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  90  }.
  91
  92
  93 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
  94
  95 (*
  96 record function_space1 (A: setoid1) (B: setoid1): Type ≝
  97  { f1:1> A → B;
  98    f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
  99  }.
 100 *)
 101
 102 definition function_space_setoid: setoid → setoid → setoid.
 103  intros (A B);
 104  constructor 1;
 105   [ apply (function_space A B);
 106   | intros;
 107     apply (∀a:A. proofs (eq ? (f a) (f1 a)));
 108   | simplify;
 109     intros;
 110     apply (f_ok ? ? x);
 111     unfold carr; unfold proofs; simplify;
 112     apply (refl A)
 113   | simplify;
 114     intros;
 115     unfold carr; unfold proofs; simplify;
 116     apply (sym B);
 117     apply (f a)
 118   | simplify;
 119     intros;
 120     unfold carr; unfold proofs; simplify;
 121     apply (trans B ? (y a));
 122     [ apply (f a)
 123     | apply (f1 a)]]
 124 qed.
 125
 126 definition function_space_setoid1: setoid1 → setoid1 → setoid1.
 127  intros (A B);
 128  constructor 1;
 129   [ apply (function_space1 A B);
 130   | intros;
 131     apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
 132   |*: cases daemon] (* simplify;
 133     intros;
 134     apply (f1_ok ? ? x);
 135     unfold proofs; simplify;
 136     apply (refl1 A)
 137   | simplify;
 138     intros;
 139     unfold proofs; simplify;
 140     apply (sym1 B);
 141     apply (f a)
 142   | simplify;
 143     intros;
 144     unfold carr; unfold proofs; simplify;
 145     apply (trans1 B ? (y a));
 146     [ apply (f a)
 147     | apply (f1 a)]] *)
 148 qed.
 149
 150 interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
 151
 152 record isomorphism (A,B: setoid): Type ≝
 153  { map1:> function_space_setoid A B;
 154    map2:> function_space_setoid B A;
 155    inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
 156    inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
 157  }.
 158
 159 interpretation "isomorphism" 'iff x y = (isomorphism x y).
 160
 161 definition setoids: setoid1.
 162  constructor 1;
 163   [ apply setoid;
 164   | apply isomorphism;
 165   | intro;
 166     split;
 167      [1,2: constructor 1;
 168         [1,3: intro; assumption;
 169         |*: intros; assumption]
 170      |3,4:
 171        intros;
 172        simplify;
 173        unfold proofs; simplify;
 174        apply refl;]
 175   |*: cases daemon]
 176 qed.
 177
 178 definition setoid1_of_setoid: setoid → setoid1.
 179  intro;
 180  constructor 1;
 181   [ apply (carr s)
 182   | apply (eq s)
 183   | apply (refl s)
 184   | apply (sym s)
 185   | apply (trans s)]
 186 qed.
 187
 188 coercion setoid1_of_setoid.
 189
 190 (*
 191 record dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
 192  { dp:> ∀a:A.carr (B a);
 193    dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
 194  }.*)
 195
 196 record forall (A:setoid)  (B: A ⇒ CCProp): CProp ≝
 197  { fo:> ∀a:A.proofs (B a) }.
 198
 199 record subset (A: setoid) : CProp ≝
 200  { mem: A ⇒ CCProp }.
 201
 202 definition ssubset: setoid → setoid1.
 203  intro;
 204  constructor 1;
 205   [ apply (subset s);
 206   | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
 207   | simplify;
 208     intros;
 209     split;
 210     intro;
 211     assumption
 212   | simplify;
 213     cases daemon
 214   | cases daemon]
 215 qed.
 216
 217 definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp.
 218  intros;
 219  constructor 1;
 220   [ apply mem;
 221   | unfold function_space_setoid1; simplify;
 222     intros (b b');
 223     change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
 224     unfold proofs1; simplify; intros;
 225     unfold proofs1 in c; simplify in c;
 226     unfold ssubset in c; simplify in c;
 227     cases (c a); clear c;
 228     split;
 229     assumption]
 230 qed.
 231
 232 (*
 233 definition sand: CCProp ⇒ CCProp.
 234
 235 definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
 236  intro;
 237  constructor 1;
 238   [ intro;
 239     constructor 1;
 240      [ intro;
 241        constructor 1;
 242        constructor 1;
 243        intro;
 244        apply (mem ? c c2 ∧ mem ? c1 c2);
 245      |
 246   |
 247   |
 248 *)
 249 *******************)