helm/software/matita/nlibrary/sets/setoids1.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 "sets/setoids.ma".
  16
  17 (*
  18 definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
  19 definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
  20 definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
  21
  22 record setoid1 : Type ≝
  23  { carr1:> Type;
  24    eq1: carr1 → carr1 → CProp;
  25    refl1: reflexive1 ? eq1;
  26    sym1: symmetric1 ? eq1;
  27    trans1: transitive1 ? eq1
  28  }.
  29
  30 definition proofs1: CProp → setoid1.
  31  intro;
  32  constructor 1;
  33   [ apply A
  34   | intros;
  35     apply True
  36   | intro;
  37     constructor 1
  38   | intros 3;
  39     constructor 1
  40   | intros 5;
  41     constructor 1]
  42 qed.
  43
  44 ndefinition CCProp: setoid1.
  45  constructor 1;
  46   [ apply CProp
  47   | apply iff
  48   | intro;
  49     split;
  50     intro;
  51     assumption
  52   | intros 3;
  53     cases H; clear H;
  54     split;
  55     assumption
  56   | intros 5;
  57     cases H; cases H1; clear H H1;
  58     split;
  59     intros;
  60     [ apply (H4 (H2 H))
  61     | apply (H3 (H5 H))]]
  62 qed.
  63
  64 record function_space1 (A: setoid1) (B: setoid1): Type ≝
  65  { f1:1> A → B;
  66    f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
  67  }.
  68
  69 definition function_space_setoid1: setoid1 → setoid1 → setoid1.
  70  intros (A B);
  71  constructor 1;
  72   [ apply (function_space1 A B);
  73   | intros;
  74     apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
  75   |*: cases daemon] (* simplify;
  76     intros;
  77     apply (f1_ok ? ? x);
  78     unfold proofs; simplify;
  79     apply (refl1 A)
  80   | simplify;
  81     intros;
  82     unfold proofs; simplify;
  83     apply (sym1 B);
  84     apply (f a)
  85   | simplify;
  86     intros;
  87     unfold carr; unfold proofs; simplify;
  88     apply (trans1 B ? (y a));
  89     [ apply (f a)
  90     | apply (f1 a)]] *)
  91 qed.
  92
  93 interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
  94
  95 definition setoids: setoid1.
  96  constructor 1;
  97   [ apply setoid;
  98   | apply isomorphism;
  99   | intro;
 100     split;
 101      [1,2: constructor 1;
 102         [1,3: intro; assumption;
 103         |*: intros; assumption]
 104      |3,4:
 105        intros;
 106        simplify;
 107        unfold proofs; simplify;
 108        apply refl;]
 109   |*: cases daemon]
 110 qed.
 111
 112 definition setoid1_of_setoid: setoid → setoid1.
 113  intro;
 114  constructor 1;
 115   [ apply (carr s)
 116   | apply (eq s)
 117   | apply (refl s)
 118   | apply (sym s)
 119   | apply (trans s)]
 120 qed.
 121
 122 coercion setoid1_of_setoid.
 123
 124 record forall (A:setoid)  (B: A ⇒ CCProp): CProp ≝
 125  { fo:> ∀a:A.proofs (B a) }.
 126
 127 record subset (A: setoid) : CProp ≝
 128  { mem: A ⇒ CCProp }.
 129
 130 definition ssubset: setoid → setoid1.
 131  intro;
 132  constructor 1;
 133   [ apply (subset s);
 134   | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
 135   | simplify;
 136     intros;
 137     split;
 138     intro;
 139     assumption
 140   | simplify;
 141     cases daemon
 142   | cases daemon]
 143 qed.
 144
 145 definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp.
 146  intros;
 147  constructor 1;
 148   [ apply mem;
 149   | unfold function_space_setoid1; simplify;
 150     intros (b b');
 151     change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
 152     unfold proofs1; simplify; intros;
 153     unfold proofs1 in c; simplify in c;
 154     unfold ssubset in c; simplify in c;
 155     cases (c a); clear c;
 156     split;
 157     assumption]
 158 qed.
 159
 160 definition sand: CCProp ⇒ CCProp.
 161
 162 definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
 163  intro;
 164  constructor 1;
 165   [ intro;
 166     constructor 1;
 167      [ intro;
 168        constructor 1;
 169        constructor 1;
 170        intro;
 171        apply (mem ? c c2 ∧ mem ? c1 c2);
 172      |
 173   |
 174   |
 175
 176 *)