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