helm/software/matita/contribs/ng_assembly/common/meta_type.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/string_lemmas.ma".
  24
  25 nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  26  match l with
  27   [ nil ⇒ true
  28   | cons h t ⇒ match f elem h with
  29    [ true ⇒ false | false ⇒ nmember_list T elem f t ]
  30   ].
  31
  32 (* elem presente una ed una sola volta in l *)
  33 nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  34  match l with
  35   [ nil ⇒ false
  36   | cons h t ⇒ match f elem h with
  37     [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
  38   ].
  39
  40 (* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
  41 ninductive UN : Type ≝
  42   uq0 : UN | uq1 : UN | uq2 : UN | uq3 : UN
  43 | uo0 : UN | uo1 : UN | uo2 : UN | uo3 : UN | uo4 : UN | uo5 : UN | uo6 : UN | uo7 : UN
  44 | ux0 : UN | ux1 : UN | ux2 : UN | ux3 : UN | ux4 : UN | ux5 : UN | ux6 : UN | ux7 : UN
  45 | ux8 : UN | ux9 : UN | uxA : UN | uxB : UN | uxC : UN | uxD : UN | uxE : UN | uxF : UN
  46 .
  47
  48 (* funzione di uguaglianza sugli atomi *)
  49 ndefinition eq_UN ≝
  50 λu1,u2.match u1 with
  51  [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
  52  | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
  53  | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
  54  | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
  55  | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
  56  | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
  57  | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
  58  | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
  59  | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
  60  | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
  61  | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
  62  | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
  63  | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
  64  | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
  65  | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
  66  | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
  67  | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
  68  | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
  69  | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
  70  | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
  71  | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
  72  | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
  73  | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
  74  | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
  75  | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
  76  | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
  77  | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
  78  | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
  79  ].
  80
  81 (* costruttore di un sottouniverso:
  82    S_EL cioe' uno qualsiasi degli elementi del sottouniverso
  83    S_KO cioe' il caso impossibile
  84 *)
  85 ninductive S_UN (l:list UN) : Type ≝
  86   S_EL : Πe:UN.(member_list UN e eq_UN l) = true → S_UN l
  87 | S_KO : False → S_UN l.
  88
  89 (* sottoinsieme degli esadecimali *)
  90 ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
  91
  92 (* getter del testimone di esistenza *)
  93 ndefinition getelem : ∀l.∀e:S_UN l.UN.
  94  #l; #s; nelim s;
  95  ##[ ##1: #u; #H; napply u
  96  ##| ##2: #H; nelim H
  97  ##]
  98 nqed.
  99
 100 (* getter della dimostrazione di appartenenza *)
 101 ndefinition getdim : ∀l.∀e:S_UN l.member_list UN ? eq_UN l = true.
 102  ##[ ##2: nelim e;
 103           ##[ ##1: #u; #H; napply u
 104           ##| ##2: #H; nelim H
 105           ##]
 106  ##| ##1: #l; #s; nelim s;
 107           ##[ ##1: #u; #m; napply m
 108           ##| ##2: #H; nelim H
 109           ##]
 110  ##]
 111 nqed.
 112
 113 (* costruttore universale di una funzione ad un solo argomento: esadecimali → esadecimali *)
 114 ndefinition f1_EX_UN
 115  : ∀e:S_UN EX_UN.
 116    ∀f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN.
 117    S_UN EX_UN.
 118  #input; #f1; #f2; #f3; #f4; #f5; #f6; #f7; #f8; #f9; #f10; #f11; #f12; #f13; #f14; #f15; #f16;
 119  nelim input;
 120  ##[ ##2: #H; nelim H
 121  ##| ##1: #u; #H; nelim u in H:(%); #H;
 122           ##[ ##13: napply f1 ##| ##14: napply f2 ##| ##15: napply f3 ##| ##16: napply f4
 123           ##| ##17: napply f5 ##| ##18: napply f6 ##| ##19: napply f7 ##| ##20: napply f8
 124           ##| ##21: napply f9 ##| ##22: napply f10 ##| ##23: napply f11 ##| ##24: napply f12
 125           ##| ##25: napply f13 ##| ##26: napply f14 ##| ##27: napply f15 ##| ##28: napply f16
 126           ##| ##*: nnormalize in H:(%); napply (S_KO EX_UN (bool_destruct false true False H))
 127           ##]
 128  ##]
 129 nqed.
 130
 131 (* esempio: successore esadecimale *)
 132 ndefinition succ_EX_UN ≝
 133 λe:S_UN EX_UN.f1_EX_UN
 134  (S_EL EX_UN ux1 (refl_eq …)) (S_EL EX_UN ux2 (refl_eq …))
 135  (S_EL EX_UN ux3 (refl_eq …)) (S_EL EX_UN ux4 (refl_eq …))
 136  (S_EL EX_UN ux5 (refl_eq …)) (S_EL EX_UN ux6 (refl_eq …))
 137  (S_EL EX_UN ux7 (refl_eq …)) (S_EL EX_UN ux8 (refl_eq …))
 138  (S_EL EX_UN ux9 (refl_eq …)) (S_EL EX_UN uxA (refl_eq …))
 139  (S_EL EX_UN uxB (refl_eq …)) (S_EL EX_UN uxC (refl_eq …))
 140  (S_EL EX_UN uxD (refl_eq …)) (S_EL EX_UN uxE (refl_eq …))
 141  (S_EL EX_UN uxF (refl_eq …)) (S_EL EX_UN ux0 (refl_eq …)).
 142
 143 (* destruct universale per accedere ai due testimoni di esistenza *)
 144 nlemma same_UN_1 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
 145  #l; #e1; #e2; #dim1; #dim2; #H;
 146  nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a | S_KO _ ⇒ False ]);
 147  nrewrite < H;
 148  nnormalize;
 149  napply refl_eq.
 150 nqed.
 151
 152 (* destruct universale che funziona su qualsiasi sottouniverso *)
 153 ndefinition destruct_UN
 154  : ∀l.∀e1,e2:S_UN l.∀P:Prop.
 155    e1 = e2 → match eq_UN (getelem ? e1) (getelem ? e2) with [ true ⇒ P → P | false ⇒ P ].
 156  #l; #e1; nelim e1;
 157  ##[ ##2: #H; nelim H
 158  ##| ##1: #u1; #dim1; #e2; ncases e2;
 159           ##[ ##2: #H; nelim H
 160           ##| ##1: #u2; #dim2; #P; #H;
 161                    nchange with (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]);
 162                    nrewrite > (same_UN_1 l … H);
 163                    nelim u2;
 164                    nnormalize;
 165                    napply (λx.x)
 166           ##]
 167  ##]
 168 nqed.
 169
 170 nlemma eqUN_to_eq : ∀l.∀e1,e2:S_UN l.eq_UN (getelem ? e1) (getelem ? e2) = true → (getelem ? e1) = (getelem ? e2).
 171  #l; #e1; nelim e1;
 172  ##[ ##2: #H; nelim H
 173  ##| ##1: #u1; #dim1; #e2; ncases e2;
 174           ##[ ##2: #H; nelim H;
 175           ##| ##1: #u2; #dim2; #H; nelim u1;
 176                    ##[ ##1: nelim u2; ##[ ##1:
 177
 178
 179 ndefinition decidable_UN : ∀l.∀e1,e2:S_UN l.decidable (e1 = e2).
 180  #l; #e1; ncases e1;
 181  ##[ ##2: #H; nelim H
 182  ##| ##1: #u1; #dim1; #e2; ncases e2;
 183           ##[ ##2: #H; nelim H
 184           ##| ##1: #u2; #dim2; nnormalize;
 185                    napply (or2_intro2 (? = ?) (? ≠ ?) ?);
 186                    nnormalize;
 187                    #H;
 188                    nchange with (match S_EL l u1 dim1
 189                                   return λx.eq_UN x u2 → Prop
 190                                  with
 191                                   [ S_EL x _ ⇒ λp:(False
 192                                   | S_KO H ⇒ True
 193                                   ] (refl_eq ? (eq_UN u1 u2);
 194                    nletin K ≝ (same_UN_1 l … H);
 195                    nelim u1 in dim1:(%) H:(%) K:(%);
 196                    #dim1; #H; #K;
 197                    napply (destruct_UN l … H);
 198
 199
 200
 201
 202
 203
 204
 205
 206
 207