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 record iff (A,B: CProp) : CProp ≝
  18  { if: A → B;
  19    fi: B → A
  20  }.
  21
  22 notation > "hvbox(a break \liff b)"
  23   left associative with precedence 25
  24 for @{ 'iff $a $b }.
  25
  26 notation "hvbox(a break \leftrightarrow b)"
  27   left associative with precedence 25
  28 for @{ 'iff $a $b }.
  29
  30 interpretation "logical iff" 'iff x y = (iff x y).
  31
  32 record setoid : Type ≝
  33  { carr:> Type;
  34    eq: carr → carr → CProp;
  35    refl: reflexive ? eq;
  36    sym: symmetric ? eq;
  37    trans: transitive ? eq
  38  }.
  39
  40 definition proofs: CProp → setoid.
  41  intro;
  42  constructor 1;
  43   [ apply A
  44   | intros;
  45     alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
  46     apply True
  47   | intro;
  48     constructor 1
  49   | intros 3;
  50     constructor 1
  51   | intros 5;
  52     constructor 1]
  53 qed.
  54
  55 record setoid1 : Type ≝
  56  { carr1:> Type;
  57    eq1: carr1 → carr1 → CProp;
  58    refl1: reflexive ? eq1;
  59    sym1: symmetric ? eq1;
  60    trans1: transitive ? eq1
  61  }.
  62
  63 definition CCProp: setoid1.
  64  constructor 1;
  65   [ apply CProp
  66   | apply iff
  67   | intro;
  68     split;
  69     intro;
  70     assumption
  71   | intros 3;
  72     cases H; clear H;
  73     split;
  74     assumption
  75   | intros 5;
  76     cases H; cases H1; clear H H1;
  77     split;
  78     intros;
  79     [ apply (H4 (H2 H))
  80     | apply (H3 (H5 H))]]
  81 qed.
  82
  83 record function_space (A,B: setoid): Type ≝
  84  { f:1> A → B;
  85    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  86  }.
  87
  88 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
  89 interpretation "function_space" 'Imply a b = (function_space a b).
  90
  91 record function_space1 (A: setoid1) (B: setoid1): Type ≝
  92  { f1:1> A → B;
  93    f1_ok: ∀a,a':A. proofs (eq1 ? a a') → proofs (eq1 ? (f1 a) (f1 a'))
  94  }.
  95
  96 definition function_space_setoid: setoid → setoid → setoid.
  97  intros (A B);
  98  constructor 1;
  99   [ apply (A ⇒ B);
 100   | intros;
 101     apply (∀a:A. proofs (eq ? (f a) (f1 a)));
 102   | simplify;
 103     intros;
 104     apply (f_ok ? ? x);
 105     unfold carr; unfold proofs; simplify;
 106     apply (refl A)
 107   | simplify;
 108     intros;
 109     unfold carr; unfold proofs; simplify;
 110     apply (sym B);
 111     apply (f a)
 112   | simplify;
 113     intros;
 114     unfold carr; unfold proofs; simplify;
 115     apply (trans B ? (y a));
 116     [ apply (f a)
 117     | apply (f1 a)]]
 118 qed.
 119
 120 interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b).
 121
 122 definition function_space_setoid1: setoid1 → setoid1 → setoid.
 123  intros (A B);
 124  constructor 1;
 125   [ apply (function_space1 A B);
 126   | intros;
 127     apply (∀a:A. proofs (eq1 ? (f a) (f1 a)));
 128   | simplify;
 129     intros;
 130     apply (f1_ok ? ? x);
 131     unfold proofs; simplify;
 132     apply (refl1 A)
 133   | simplify;
 134     intros;
 135     unfold proofs; simplify;
 136     apply (sym1 B);
 137     apply (f a)
 138   | simplify;
 139     intros;
 140     unfold carr; unfold proofs; simplify;
 141     apply (trans1 B ? (y a));
 142     [ apply (f a)
 143     | apply (f1 a)]]
 144 qed.
 145
 146 record isomorphism (A,B: setoid): Type ≝
 147  { map1:> A ⇒ B;
 148    map2:> B ⇒ A;
 149    inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
 150    inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
 151  }.
 152
 153 interpretation "isomorphism" 'iff x y = (isomorphism x y).
 154
 155 axiom daemon: False.
 156
 157 definition setoids: setoid1.
 158  constructor 1;
 159   [ apply setoid;
 160   | apply isomorphism;
 161   | intro;
 162     split;
 163      [1,2: constructor 1;
 164         [1,3: intro; assumption;
 165         |*: intros; assumption]
 166      |3,4:
 167        intros;
 168        simplify;
 169        unfold carr; unfold proofs; simplify;
 170        apply refl;]
 171   |*: elim daemon]
 172 qed.
 173
 174 definition setoid1_of_setoid: setoid → setoid1.
 175  intro;
 176  constructor 1;
 177   [ apply (carr s)
 178   | apply (eq s)
 179   | apply (refl s)
 180   | apply (sym s)
 181   | apply (trans s)
 182   ]
 183 qed.
 184
 185 coercion setoid1_of_setoid.
 186
 187 (*
 188 record dependent_product (A:setoid1)  (B: function_space1 A setoids): Type ≝
 189  { dp:> ∀a:A.carr (B a);
 190    dp_ok: ∀a,a':A. ∀p:proofs (eq1 ? a a'). proofs (eq1 ? (dp a) (map2 ?? (f1_ok A ? B ?? p) (dp a')))
 191  }.
 192 *)
 193
 194 record forall (A:setoid)  (B: function_space1 A CCProp): CProp ≝
 195  { fo:> ∀a:A.proofs (B a)
 196  }.
 197
 198 record subset (A: setoid) : CProp ≝
 199  { mem: function_space1 A CCProp
 200  }.
 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     elim daemon
 214   | elim daemon]
 215 qed.
 216
 217 definition mmem: ∀A:setoid. function_space_setoid1 (ssubset A) (function_space_setoid1 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 proofs; simplify; intros;
 225     unfold proofs 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.