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