helm/software/matita/contribs/ng_assembly/universe/universe.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 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/list.ma".
  24 include "common/nat_lemmas.ma".
  25 include "common/prod.ma".
  26
  27 nlet rec nmember_natList (elem:nat) (l:ne_list nat) on l ≝
  28  match l with
  29   [ ne_nil h ⇒ ⊖(eq_nat elem h)
  30   | ne_cons h t ⇒ match eq_nat elem h with
  31    [ true ⇒ false | false ⇒ nmember_natList elem t ]
  32   ].
  33
  34 (* elem presente una ed una sola volta in l *)
  35 nlet rec member_natList (elem:nat) (l:ne_list nat) on l ≝
  36  match l with
  37   [ ne_nil h ⇒ eq_nat elem h
  38   | ne_cons h t ⇒ match eq_nat elem h with
  39     [ true ⇒ nmember_natList elem t | false ⇒ member_natList elem t ]
  40   ].
  41
  42 (* costruttore di un sottouniverso:
  43    S_EL cioe' uno qualsiasi degli elementi del sottouniverso
  44 *)
  45 ninductive S_UN (l:ne_list nat) : Type ≝
  46  S_EL : Πx:nat.((member_natList x l) = true) → S_UN l.
  47
  48 ndefinition getelem : ∀l.∀e:S_UN l.nat.
  49  #l; #s; nelim s;
  50  #u; #dim;
  51  napply u.
  52 nqed.
  53
  54 ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_nat (getelem ? x) (getelem ? y).
  55
  56 ndefinition getdim : ∀l.∀e:S_UN l.member_natList (getelem ? e) l = true.
  57  #l; #s; nelim s;
  58  #u; #dim;
  59  napply dim.
  60 nqed.
  61
  62 nlemma SUN_destruct_1
  63  : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
  64  #l; #e1; #e2; #dim1; #dim2; #H;
  65  nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a ]);
  66  nrewrite < H;
  67  nnormalize;
  68  napply refl_eq.
  69 nqed.
  70
  71 (* destruct universale *)
  72 ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
  73  #l; #x; nelim x;
  74  #u1; #dim1;
  75  #y; nelim y;
  76  #u2; #dim2;
  77  #P;
  78  nchange with (? → (match eq_nat u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
  79  #H;
  80  nrewrite > (SUN_destruct_1 l … H);
  81  nrewrite > (eq_to_eqnat u2 u2 (refl_eq …));
  82  nnormalize;
  83  napply (λx.x).
  84 nqed.
  85
  86 (* eq_to_eqxx universale *)
  87 nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
  88  #l; #x; nelim x;
  89  #u1; #dim1;
  90  #y; nelim y;
  91  #u2; #dim2;
  92  nchange with (? → eq_nat u1 u2 = true);
  93  #H; napply (eq_to_eqnat u1 u2);
  94  napply (SUN_destruct_1 l … H).
  95 nqed.
  96
  97 (* neqxx_to_neq universale *)
  98 nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
  99  #l; #n1; #n2; #H;
 100  napply (not_to_not (n1 = n2) (eq_SUN l n1 n2 = true) …);
 101  ##[ ##1: napply (eq_to_eqSUN l n1 n2)
 102  ##| ##2: napply (eqfalse_to_neqtrue … H)
 103  ##]
 104 nqed.
 105
 106 (* perche' non si riesce a dimstrare ??? *
 107 nlemma SUN_construct
 108  : ∀l.∀u.
 109    ∀dim1,dim2:(member_natList u l = true).
 110    ((S_EL l u dim1) = (S_EL l u dim2)).
 111  #l; #u; #dim1; #dim2;
 112  nchange with (S_EL l u dim1 = S_EL l u dim1);
 113  napply refl_eq.
 114 nqed.
 115 *)
 116 naxiom SUN_construct
 117  : ∀l.∀u.
 118    ∀dim1,dim2:(member_natList u l = true).
 119    ((S_EL l u dim1) = (S_EL l u dim2)).
 120
 121 nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
 122  #l; #x; nelim x;
 123  #u1; #dim1;
 124  #y; nelim y;
 125  #u2; #dim2;
 126  nchange with (u1 = u2 → ?);
 127  #H;
 128  nrewrite > H in dim1:(%) ⊢ %;
 129  #dim1;
 130  napply (SUN_construct l u2 dim1 dim2).
 131 nqed.
 132
 133 (* eqxx_to_eq universale *)
 134 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
 135  #l; #x; nelim x;
 136  #u1; #dim1;
 137  #y; nelim y;
 138  #u2; #dim2;
 139  nchange with ((eq_nat u1 u2 = true) → ?);
 140  #H;
 141  nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim1) (S_EL l u2 dim2) (eqnat_to_eq u1 u2 H));
 142  napply refl_eq.
 143 nqed.
 144
 145 (* neq_to_neqxx universale *)
 146 nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
 147  #l; #n1; #n2; #H;
 148  napply (neqtrue_to_eqfalse (eq_SUN l n1 n2));
 149  napply (not_to_not (eq_SUN l n1 n2 = true) (n1 = n2) ? H);
 150  napply (eqSUN_to_eq l n1 n2).
 151 nqed.
 152
 153 (* decidibilita' universale *)
 154 nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
 155  #l; #x; #y; nnormalize;
 156  napply (or2_elim (eq_SUN l x y = true) (eq_SUN l x y = false) ? (decidable_bexpr ?));
 157  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqSUN_to_eq l … H))
 158  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqSUN_to_neq l … H))
 159  ##]
 160 nqed.
 161
 162 (* simmetria di uguaglianza universale *)
 163 nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
 164  #l; #n1; #n2;
 165  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_SUN l n1 n2));
 166  ##[ ##1: #H; nrewrite > H; napply refl_eq
 167  ##| ##2: #H; nrewrite > (neq_to_neqSUN l n1 n2 H);
 168           napply (symmetric_eq ? (eq_SUN l n2 n1) false);
 169           napply (neq_to_neqSUN l n2 n1 (symmetric_neq ? n1 n2 H))
 170  ##]
 171 nqed.
 172
 173 (* scheletro di funzione generica ad 1 argomento *)
 174 nlet rec farg1_auxT (T:Type) (l:ne_list nat) on l ≝
 175  match l with
 176   [ ne_nil _ ⇒ T
 177   | ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
 178   ].
 179
 180 nlemma farg1_auxDim : ∀h,t,x.eq_nat x h = false → member_natList x (h§§t) = true → member_natList x t = true.
 181  #h; #t; #x; #H; #H1;
 182  nnormalize in H1:(%);
 183  nrewrite > H in H1:(%);
 184  nnormalize;
 185  napply (λx.x).
 186 nqed.
 187
 188 nlet rec farg1 (T:Type) (l:ne_list nat) on l ≝
 189  match l with
 190   [ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
 191   | ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
 192    match eq_nat (getelem ? x) h
 193     return λy.eq_nat (getelem ? x) h = y → ?
 194    with
 195     [ true ⇒ λp:(eq_nat (getelem ? x) h = true).fst … arg
 196     | false ⇒ λp:(eq_nat (getelem ? x) h = false).
 197      farg1 T t
 198       (snd … arg)
 199       (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
 200     ] (refl_eq ? (eq_nat (getelem ? x) h))
 201   ].
 202
 203 (* scheletro di funzione generica a 2 argomenti *)
 204 nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
 205  match l with
 206   [ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
 207   | ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
 208    match eq_nat (getelem ? x) h
 209     return λy.eq_nat (getelem ? x) h = y → ?
 210    with
 211     [ true ⇒ λp:(eq_nat (getelem ? x) h = true).farg1 T lfix (fst … arg)
 212     | false ⇒ λp:(eq_nat (getelem ? x) h = false).
 213      farg2 T t lfix
 214       (snd … arg)
 215       (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
 216     ] (refl_eq ? (eq_nat (getelem ? x) h))
 217   ].
 218
 219 (* esempio0: universo ottale *)
 220 ndefinition oct0 ≝ O.
 221 ndefinition oct1 ≝ S O.
 222 ndefinition oct2 ≝ S (S O).
 223 ndefinition oct3 ≝ S (S (S O)).
 224 ndefinition oct4 ≝ S (S (S (S O))).
 225 ndefinition oct5 ≝ S (S (S (S (S O)))).
 226 ndefinition oct6 ≝ S (S (S (S (S (S O))))).
 227 ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).
 228
 229 ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».
 230
 231 ndefinition uoct0 ≝ S_EL oct_UN oct0 (refl_eq …).
 232 ndefinition uoct1 ≝ S_EL oct_UN oct1 (refl_eq …).
 233 ndefinition uoct2 ≝ S_EL oct_UN oct2 (refl_eq …).
 234 ndefinition uoct3 ≝ S_EL oct_UN oct3 (refl_eq …).
 235 ndefinition uoct4 ≝ S_EL oct_UN oct4 (refl_eq …).
 236 ndefinition uoct5 ≝ S_EL oct_UN oct5 (refl_eq …).
 237 ndefinition uoct6 ≝ S_EL oct_UN oct6 (refl_eq …).
 238 ndefinition uoct7 ≝ S_EL oct_UN oct7 (refl_eq …).
 239
 240 (* esempio1: NOT ottale *)
 241 ndefinition octNOT ≝
 242  farg1 (S_UN oct_UN) oct_UN
 243   (pair … uoct7 (pair … uoct6 (pair … uoct5 (pair … uoct4 (pair … uoct3 (pair … uoct2 (pair … uoct1 uoct0))))))).
 244
 245 (* esempio2: AND ottale *)
 246 ndefinition octAND0 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 uoct0)))))).
 247 ndefinition octAND1 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 uoct1)))))).
 248 ndefinition octAND2 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct0 (pair … uoct0 (pair … uoct2 uoct2)))))).
 249 ndefinition octAND3 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct0 (pair … uoct1 (pair … uoct2 uoct3)))))).
 250 ndefinition octAND4 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct4 (pair … uoct4 (pair … uoct4 uoct4)))))).
 251 ndefinition octAND5 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct4 (pair … uoct5 (pair … uoct4 uoct5)))))).
 252 ndefinition octAND6 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct4 (pair … uoct4 (pair … uoct6 uoct6)))))).
 253 ndefinition octAND7 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct4 (pair … uoct5 (pair … uoct6 uoct7)))))).
 254
 255 ndefinition octAND ≝
 256  farg2 (S_UN oct_UN) oct_UN oct_UN
 257   (pair … octAND0 (pair … octAND1 (pair … octAND2 (pair … octAND3 (pair … octAND4 (pair … octAND5 (pair … octAND6 octAND7))))))).
 258
 259 (* ora e' possibile fare
 260    octNOT uoctX
 261    octAND uoctX uoctY
 262 *)