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. eq ? a a' → 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: setoid) (B: setoid1): Type ≝
  92  { f1:1> A → B;
  93    f1_ok: ∀a,a':A. eq ? a a' → 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. eq ? (f a) (f1 a));
 102   | simplify;
 103     intros;
 104     apply (f_ok ? ? x);
 105     apply (refl A)
 106   | simplify;
 107     intros;
 108     apply (sym B);
 109     apply (H a)
 110   | simplify;
 111     intros;
 112     apply (trans B ? (y a));
 113     [ apply (H a)
 114     | apply (H1 a)]]
 115 qed.
 116
 117 interpretation "function_space_setoid" 'Imply a b = (function_space_setoid a b).
 118
 119 record isomorphism (A,B: setoid): Type ≝
 120  { map1:> A ⇒ B;
 121    map2:> B ⇒ A;
 122    inv1: ∀a:A. eq ? (map2 (map1 a)) a;
 123    inv2: ∀b:B. eq ? (map1 (map2 b)) b
 124  }.
 125
 126 interpretation "isomorphism" 'iff x y = (isomorphism x y).
 127
 128 axiom daemon: False.
 129
 130 definition setoids: setoid1.
 131  constructor 1;
 132   [ apply setoid;
 133   | apply isomorphism;
 134   | intro;
 135     split;
 136      [1,2: constructor 1;
 137         [1,3: intro; assumption;
 138         |*: intros; assumption]
 139      |3,4:
 140        intros;
 141        simplify;
 142        apply refl;]
 143   |*: elim daemon]
 144 qed.
 145
 146 record dependent_product (A:setoid)  (B: function_space1 A setoids): Type ≝
 147  { dp:> ∀a:A.carr (B a);
 148    dp_ok: ∀a,a':A. ∀p:eq ? a a'. eq ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a'))
 149  }.
 150
 151 record forall (A:setoid)  (B: function_space1 A CCProp): Type ≝
 152  { fo:> ∀a:A.proofs (B a)
 153  }.
 154
 155 record subset (A: setoid) : Type ≝
 156  { mem: function_space1 A CCProp
 157  }.
 158
 159 definition subset_eq ≝ λA:setoid.λU,V: subset A. ∀a:A. mem ? U a \liff mem ? V a.
 160
 161 lemma mem_ok:
 162  ∀A:setoid.∀a,a':A.∀U,V: subset A.
 163   eq ? a a' → subset_eq ? U V → mem ? U a \liff mem ? V a'.
 164  intros;
 165  cases (H1 a);
 166  split; intro H4;
 167   [ lapply (H2 H4); clear H2 H3 H4;
 168     apply (if ?? (f1_ok ?? (mem ? V) ?? H));
 169     assumption
 170   | apply H3; clear H2 H3;
 171     apply (fi ?? (f1_ok ?? (mem ? V) ?? H));
 172     apply H4;]
 173 qed.
 174