matita/matita/projdat/coerc.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 "projdat/basic_type.ma".
  16
  17
  18 theorem base_iff: ∀b,y:bool. if b then y else y = y.
  19 * normalize // qed.
  20
  21 theorem base_iff2: ∀b. if b then true else false = b.
  22 * normalize // qed.
  23
  24 theorem hp_tesi: ∀D:DeqSet. ∀x,y:D. ∀b:bool. if (x==y) then b else false=true→b=true.
  25 #D #x #y #b elim b #Hp // normalize in Hp; > base_iff in Hp; // qed.
  26
  27 theorem hp_tesi2: ∀D:DeqSet. ∀x,y:D. ∀b:bool. if (x==y) then b else false=true→(x==y)=true.
  28 #D #x #y #b #Hp lapply (hp_tesi … Hp) #Hp2
  29 destruct >base_iff2 in Hp; // qed.
  30
  31 (******************************************************************************)
  32 (*                       Coercizione per i dati lista                         *)
  33 (******************************************************************************)
  34
  35 let rec eqb_lD (T:DeqSet) (x,y:list T) on x : bool ≝
  36   match x with
  37   [ nil ⇒
  38     match y with
  39     [ nil ⇒ true
  40     | _ ⇒ false]
  41   | cons a b ⇒
  42     match y with
  43     [ nil ⇒ false
  44     | cons c d ⇒ (eqb T a c)∧(eqb_lD T b d)]].
  45
  46 lemma eqb_same_D: ∀D:DeqSet. ∀x:D. (eqb D x x)=true.
  47 #D #same @(proj2 … (eqb_true D ? ? ) …) // qed.
  48
  49 theorem listD_elim2 :
  50 ∀D:DeqSet.
  51  ∀R:list D→ list D → Prop.
  52   (∀n:list D. R [] n)
  53   → (∀n,r. R (r::n) [])
  54   → (∀n,m,r,u. R n m → R (r::n) (u::m))
  55   → ∀n,m. R n m.
  56 #D
  57 #R #ROn #RSO #RSS #n (elim n) // #n0 #lN0 #Rn0m #m (cases m) /2/ qed.
  58
  59 lemma list_destr_l: ∀D:DeqSet. ∀a,b:D.∀r,s:list D. (a=b)∧(r=s)→(a::r)=(b::s).
  60 #D #x #y #r #s #Hp
  61 lapply (proj1 (x=y) (r=s) Hp)
  62      lapply (proj2 (x=y) (r=s) Hp)
  63 #H #H2 >H >H2 // qed.
  64
  65 lemma list_destr_r: ∀D:DeqSet. ∀a,b:D.∀r,s:list D. (a::r)=(b::s)→(a=b)∧(r=s).
  66 #D #x #y *
  67   [ *
  68     [ #Hp %
  69
  70       [destruct @refl
  71       |//
  72       ]
  73     | #d #lD #hp destruct
  74     ]
  75   | #d #lD #s #hp destruct % @refl] qed.
  76
  77 lemma obv_eqb: ∀D:DeqSet.∀x:D. (x==x)=true.
  78 #D #l @(proj2 … (eqb_true ???) ) // qed.
  79
  80 lemma obv_eb_l: ∀D. ∀e,l. (eqb_lD D (e::l) (e::l)=true).
  81 #D #x#y normalize elim y normalize >obv_eqb //
  82 #X #lX normalize #Hp >obv_eqb normalize @Hp qed.
  83
  84 lemma liD_right: ∀D:DeqSet. ∀x,y:list D. (x=y)→(eqb_lD D x y)=true.
  85 #D
  86 @listD_elim2
  87 [ #n #asmpt <asmpt //
  88 | #L #r #Hp>Hp //
  89 | #l1 #l2 #e1 #e2 #Hp #eI lapply(list_destr_r D e1 e2 l1 l2 eI)
  90   #HpE lapply (proj1 ? ? HpE) lapply (proj2 ? ? HpE) -HpE
  91   #ls lapply (Hp ls) -Hp
  92   #eqv #hp destruct
  93    destruct
  94   normalize >obv_eqb normalize @eqv] qed.
  95
  96 lemma lid_left_1: ∀D:DeqSet. ∀x,y:D. ∀l1,l2:list D. ((x==y)=true)∧(l1=l2)→(x::l1=y::l2).
  97 #D #x #y #L #M * #Hp lapply (proj1 … (eqb_true D ? ? ) Hp) -Hp #Hp #LH destruct // qed.
  98
  99 lemma tesi3: ∀D:DeqSet. ∀x,y:D. ∀M. (x=y)→(x::M=y::M).
 100 #T#a #b #L #hp destruct // qed.
 101
 102 lemma liD_left: ∀D:DeqSet. ∀x,y:list D. (eqb_lD D x y)=true→(x=y).
 103 #D @listD_elim2
 104   [ * normalize // #hp #HHp #abs destruct
 105   | #L #el normalize #abs destruct
 106   | #L #M #x #y #Hp normalize #N lapply (hp_tesi2… N) #Hp2
 107     lapply(hp_tesi D … N) -N #N lapply(Hp N)
 108     -Hp -N #HP destruct @tesi3 @(proj1 … (eqb_true D ? ? )) //] qed.
 109
 110 lemma biimplication_lD: ∀D:DeqSet. ∀x,y:list D. iff ((eqb_lD D x y)=true) (x=y).
 111 #D #x #y %
 112   [ @liD_left | @liD_right ]
 113 qed.
 114
 115
 116 definition DeqList ≝ λT:DeqSet. mk_DeqSet (list T) (eqb_lD T) (biimplication_lD T).
 117
 118 unification hint  0 ≔ C1:DeqSet;
 119     X ≟ DeqList C1
 120 (* ---------------------------------------- *) ⊢
 121     DeqList C1 ≡ carr X.
 122
 123 unification hint  0 ≔ C1:DeqSet,b1:list C1,b2: list C1;
 124     X ≟ DeqList C1
 125 (* ---------------------------------------- *) ⊢
 126     eqb_lD C1 b1 b2 ≡ eqb X b1 b2.
 127
 128
 129 (******************************************************************************)
 130 (*                           Coercizione per i dati Σ                         *)
 131 (******************************************************************************)
 132
 133 definition Sig_fst  ≝ λA:Type[0].λP:A→Prop.λx:Sig A P.
 134   match x with [mk_Sig a h ⇒ a].
 135
 136 definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
 137   match x return λx.P (Sig_fst A P x) with [mk_Sig a h ⇒ h].
 138
 139 definition Sig_eq  ≝ λA:DeqSet.λP:A→Prop. λx,y:Sig A P.
 140   ((Sig_fst A P x)==(Sig_fst A P y)).
 141
 142 lemma biimplication_Sig: ∀A:DeqSet.∀P:A→Prop. ∀x,y:Sig A P.
 143   (Sig_eq A P x y)=true↔(x=y).
 144 #A #P * #a1 #p1
 145       * #a2 #p2
 146       %
 147       [ normalize #Hp
 148         lapply (proj1 … (eqb_true A ? ?) Hp)
 149         -Hp
 150         #Hp destruct //
 151       | #Hp destruct normalize //] qed.
 152
 153 definition DeqSig ≝ λT:DeqSet.λP:T→Prop. mk_DeqSet (Sig T P) (Sig_eq T P) (biimplication_Sig T P).
 154
 155 unification hint  0 ≔ C1:DeqSet,C2:C1→Prop;
 156     X ≟ DeqSig C1 C2
 157 (* ---------------------------------------- *) ⊢
 158     DeqSig C1 C2 ≡ carr X.
 159
 160 unification hint  0 ≔ C1:DeqSet,C2:C1→Prop,b1:Sig C1 C2,b2:Sig C1 C2;
 161     X ≟ DeqSig C1 C2
 162 (* ---------------------------------------- *) ⊢
 163     Sig_eq C1 C2 b1 b2 ≡ eqb X b1 b2.
 164
 165 definition mk_DeqSig : ∀T:DeqSet.∀P:T→Prop.∀x:T. (P x)→(DeqSig T P) ≝
 166 λT,P,x,p. mk_Sig T P x p.
 167
 168
 169 (******************************************************************************)
 170 (*                        Coercizione per i dati Cast                         *)
 171 (******************************************************************************)
 172
 173 lemma eqc_b: ∀n1,hs. (eq_c (CBool n1) (CBool hs))=(beqb n1 hs).
 174 #n1 #hs normalize // qed.
 175
 176 lemma eqc_n: ∀n1,hs. (eq_c (CNat n1) (CNat hs))=(eqb n1 hs).
 177 #n1 #hs normalize // qed.
 178
 179
 180 theorem dimplication_cast: ∀a,b. eq_c a b=true → a = b.
 181 * #n1
 182   [* normalize #n2 [#Hp @eq_f @eqb_true_to_eq //
 183                    |#Hp @False_ind /2/]
 184   |*  [normalize #n2 #abs @False_ind /2/
 185                    | #b >eqc_b #hp @eq_f @(\P hp)]
 186   ] qed.
 187
 188 theorem eimplication_cast: ∀a,b. a = b →eq_c a b=true.
 189 *
 190   [ #n * #m #Hp
 191     [ normalize @eq_to_eqb_true destruct //
 192     | <Hp normalize //]
 193   | #b * #c #Hp
 194     [ >Hp normalize //
 195     | destruct @(proj2 … (beqb_true …) ) //
 196   ]
 197 qed.
 198
 199
 200 theorem biimplication_cast: ∀a,b. iff (eq_c a b=true) (a = b).
 201 #A #B % [ @dimplication_cast | @eimplication_cast ] qed.
 202
 203 definition DeqCoer ≝ mk_DeqSet coerc eq_c biimplication_cast.
 204
 205 unification hint  0 ≔ ;
 206     X ≟ DeqCoer
 207 (* ---------------------------------------- *) ⊢
 208     coerc ≡ carr X.
 209
 210 unification hint  0 ≔ b1,b2:coerc;
 211     X ≟ DeqCoer
 212 (* ---------------------------------------- *) ⊢
 213     eq_c b1 b2 ≡ eqb X b1 b2.
 214
 215 (******************************************************************************)
 216 (*                        Coercizione per i dati Type                         *)
 217 (******************************************************************************)
 218
 219 theorem biimplication_type: ∀a,b. iff (eqb_type a b=true) (a=b).
 220 *  *  % //
 221   [ normalize #abs  @False_ind /2/
 222   | #Hp >Hp //
 223   | normalize #abs  @False_ind /2/
 224   | #Hp >Hp //] qed.
 225
 226 definition DeqType ≝ mk_DeqSet type eqb_type biimplication_type.
 227
 228 unification hint  0 ≔ ;
 229     X ≟ DeqType
 230 (* ---------------------------------------- *) ⊢
 231     type ≡ carr X.
 232
 233 unification hint  0 ≔ b1,b2:type;
 234     X ≟ DeqType
 235 (* ---------------------------------------- *) ⊢
 236     eqb_type b1 b2 ≡ eqb X b1 b2.
 237
 238 (******************************************************************************)
 239 (*                    Coercizione per i dati naturali                         *)
 240 (******************************************************************************)
 241
 242 definition eqb_nat ≝λx,y:nat. eqb x y.
 243 theorem biimplication_nat: ∀a,b. iff (eqb_nat a b=true) (a = b).
 244 #A #B % [ @eqb_true_to_eq | @eq_to_eqb_true ] qed.
 245
 246 definition DeqNat ≝ mk_DeqSet ℕ eqb_nat biimplication_nat.
 247
 248 unification hint  0 ≔ ;
 249     X ≟ DeqNat
 250 (* ---------------------------------------- *) ⊢
 251     nat ≡ carr X.
 252
 253 unification hint  0 ≔ b1,b2:nat;
 254     X ≟ DeqNat
 255 (* ---------------------------------------- *) ⊢
 256     eqb_nat b1 b2 ≡ eqb X b1 b2.