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