matita/matita/lib/finite_lambda/reduction.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "finite_lambda/terms_and_types.ma".
  13
  14 (* some auxiliary lemmas *)
  15
  16 lemma nth_to_default: ∀A,l,n,d.
  17   |l| ≤ n → nth n A l d = d.
  18 #A #l elim l [//] #a #tl #Hind #n cases n
  19   [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
  20   |#m #d normalize #H @Hind @le_S_S_to_le @H
  21   ]
  22 qed.
  23
  24 lemma mem_nth: ∀A,l,n,d.
  25   n < |l|  → mem ? (nth n A l d) l.
  26 #A #l elim l
  27   [#n #d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
  28   |#a #tl #Hind * normalize
  29     [#_ #_ %1 //| #m #d #HSS %2 @Hind @le_S_S_to_le @HSS]
  30   ]
  31 qed.
  32
  33 lemma nth_map: ∀A,B,l,f,n,d1,d2.
  34   n < |l| → nth n B (map … f l) d1 = f (nth n A l d2).
  35 #n #B #l #f elim l
  36   [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le //
  37   |#a #tl #Hind #m #d1 #d2 cases m normalize //
  38    #m1 #H @Hind @le_S_S_to_le @H
  39   ]
  40 qed.
  41
  42
  43
  44 (* end of auxiliary lemmas *)
  45
  46 let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝
  47   match ty return (λty.FinSet_of_FType O D ty → T O D) with
  48   [atom o ⇒ λa.Val O D o a
  49   |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1
  50     (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2))
  51      (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a))
  52   ]
  53 .
  54
  55 lemma is_closed_to_T: ∀O,D,ty,a. is_closed O D 0 (to_T O D ty a).
  56 #O #D #ty elim ty //
  57 #ty1 #ty2 #Hind1 #Hind2 #a normalize @cvec #m #Hmem
  58 lapply (mem_map ????? Hmem) * #a1 * #H1 #H2 <H2 @Hind2
  59 qed.
  60
  61 axiom inj_to_T: ∀O,D,ty,a1,a2. to_T O D ty a1 = to_T O D ty a2 → a1 = a2.
  62 (* complicata
  63 #O #D #ty elim ty
  64   [#o normalize #a1 #a2 #H destruct //
  65   |#ty1 #ty2 #Hind1 #Hind2 * #l1 #Hl1 * #l2 #Hl2 normalize #H destruct -H
  66    cut (l1=l2) [2: #H generalize in match Hl1; >H //] -Hl1 -Hl2
  67    lapply e0 -e0 lapply l2 -l2 elim l1
  68     [#l2 cases l2 normalize [// |#a1 #tl1 #H destruct]
  69     |#a1 #tl1 #Hind #l2 cases l2
  70       [normalize #H destruct
  71       |#a2 #tl2 normalize #H @eq_f2
  72         [@Hind2 *)
  73
  74 let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝
  75   match l1 with
  76   [ nil ⇒  None ?
  77   | cons hd1 tl1 ⇒ match l2 with
  78     [ nil ⇒ None ?
  79     | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2
  80     ]
  81   ].
  82
  83 lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1.
  84   assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1
  85    ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2).
  86 #A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1
  87   [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/]
  88 qed.
  89
  90 lemma assoc_to_mem: ∀A,B,a,l1,l2,b.
  91   assoc A B a l1 l2 = Some ? b → mem ? b l2.
  92 #A #B #a #l1 elim l1
  93   [#l2 #b normalize #H destruct
  94   |#hd1 #tl1 #Hind *
  95     [#b normalize #H destruct
  96     |#hd2 #tl2 #b normalize cases (a==hd1) normalize
  97       [#H %1 destruct //|#H %2 @Hind @H]
  98     ]
  99   ]
 100 qed.
 101
 102 lemma assoc_to_mem2: ∀A,B,a,l1,l2,b.
 103   assoc A B a l1 l2 = Some ? b → ∃l21,l22.l2=l21@b::l22.
 104 #A #B #a #l1 elim l1
 105   [#l2 #b normalize #H destruct
 106   |#hd1 #tl1 #Hind *
 107     [#b normalize #H destruct
 108     |#hd2 #tl2 #b normalize cases (a==hd1) normalize
 109       [#H %{[]} %{tl2} destruct //
 110       |#H lapply (Hind … H) * #la * #lb #H1
 111        %{(hd2::la)} %{lb} >H1 //]
 112     ]
 113   ]
 114 qed.
 115
 116 lemma assoc_map: ∀A,B,C,a,l1,l2,f,b.
 117   assoc A B a l1 l2 = Some ? b → assoc A C a l1 (map ?? f l2) = Some ? (f b).
 118 #A #B #C #a #l1 elim l1
 119   [#l2 #f #b normalize #H destruct
 120   |#hd1 #tl1 #Hind *
 121     [#f #b normalize #H destruct
 122     |#hd2 #tl2 #f #b normalize cases (a==hd1) normalize
 123       [#H destruct // |#H @(Hind … H)]
 124     ]
 125   ]
 126 qed.
 127
 128 (*************************** One step reduction *******************************)
 129
 130 inductive red (O:Type[0]) (D:O→FinSet) : T O D  →T O D → Prop ≝
 131   | (* we only allow beta on closed arguments *)
 132     rbeta: ∀P,M,N. is_closed O D 0 N →
 133       red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
 134   | riota: ∀ty,v,a,M.
 135       assoc ?? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
 136       red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
 137   | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
 138   | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
 139   | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1)
 140   | rmem: ∀ty,M. red O D (Lambda O D ty M)
 141       (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
 142       (enum (FinSet_of_FType O D ty))))
 143   | rvec: ∀ty,N,N1,v,v1. red O D N N1 →
 144       red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
 145
 146 (*********************************** inversion ********************************)
 147 lemma red_vec: ∀O,D,ty,v,M.
 148   red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
 149       red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
 150 #O #D #ty #v #M #Hred inversion Hred
 151   [#ty1 #M0 #N #Hc #H destruct
 152   |#ty1 #v1 #a #M0 #_ #H destruct
 153   |#M0 #M1 #N #_ #_ #H destruct
 154   |#M0 #M1 #N #_ #_ #H destruct
 155   |#ty1 #M #M1 #_ #_ #H destruct
 156   |#ty1 #M0 #H destruct
 157   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
 158   ]
 159 qed.
 160
 161 lemma red_lambda: ∀O,D,ty,M,N.
 162   red O D (Lambda O D ty M) N →
 163       (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨
 164       N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
 165       (enum (FinSet_of_FType O D ty))).
 166 #O #D #ty #M #N #Hred inversion Hred
 167   [#ty1 #M0 #N #Hc #H destruct
 168   |#ty1 #v1 #a #M0 #_ #H destruct
 169   |#M0 #M1 #N #_ #_ #H destruct
 170   |#M0 #M1 #N #_ #_ #H destruct
 171   |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % //
 172   |#ty1 #M0 #H destruct #_ %2 //
 173   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 174   ]
 175 qed.
 176
 177 lemma red_val: ∀O,D,ty,a,N.
 178   red O D (Val O D ty a) N → False.
 179 #O #D #ty #M #N #Hred inversion Hred
 180   [#ty1 #M0 #N #Hc #H destruct
 181   |#ty1 #v1 #a #M0 #_ #H destruct
 182   |#M0 #M1 #N #_ #_ #H destruct
 183   |#M0 #M1 #N #_ #_ #H destruct
 184   |#ty1 #N1 #N2 #_ #_ #H destruct
 185   |#ty1 #M0 #H destruct #_
 186   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 187   ]
 188 qed.
 189
 190 lemma red_rel: ∀O,D,n,N.
 191   red O D (Rel O D n) N → False.
 192 #O #D #n #N #Hred inversion Hred
 193   [#ty1 #M0 #N #Hc #H destruct
 194   |#ty1 #v1 #a #M0 #_ #H destruct
 195   |#M0 #M1 #N #_ #_ #H destruct
 196   |#M0 #M1 #N #_ #_ #H destruct
 197   |#ty1 #N1 #N2 #_ #_ #H destruct
 198   |#ty1 #M0 #H destruct #_
 199   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 200   ]
 201 qed.
 202
 203 (*************************** multi step reduction *****************************)
 204 lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 →
 205   star ? (red O D) (App O D M N) (App O D M1 N).
 206 #O #D #M #N #N1 #H elim H //
 207 #P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
 208 qed.
 209
 210 lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 →
 211   star ? (red O D) (App O D M N) (App O D M N1).
 212 #O #D #M #N #N1 #H elim H //
 213 #P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
 214 qed.
 215
 216 lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 →
 217   star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
 218 #O #D #ty #N #N1 #v1 #v2 #H elim H //
 219 #P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
 220 qed.
 221
 222 lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| →
 223   (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
 224   star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)).
 225 #O #D #ty #v1 elim v1
 226   [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize //
 227   |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS
 228    #H @(trans_star … (Vec O D ty (v@N2::tl1)))
 229     [@star_red_vec @(H 0 N1) @le_S_S //
 230     |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS))
 231      #n #M #H1 @(H (S n)) @le_S_S @H1
 232     ]
 233   ]
 234 qed.
 235
 236 lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| →
 237   (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
 238   star ? (red O D) (Vec O D ty v1) (Vec O D ty v2).
 239 #O #D #ty #v1 #v2 @(star_red_vec1 … [ ])
 240 qed.
 241
 242 lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 →
 243   star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1).
 244 #O #D #ty #N #N1 #H elim H //
 245 #P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ
 246 qed.
 247
 248 (************************ reduction and substitution **************************)
 249
 250 lemma red_star_subst : ∀O,D,M,N,N1,i.
 251   star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
 252 #O #D #M #N #N1 #i #Hred lapply i -i @(T_elim … M) normalize
 253   [#o #a #i //
 254   |#i #n cases (leb n i) normalize // cases (eqb n i) normalize //
 255   |#P #Q #HindP #HindQ #n normalize
 256    @(trans_star … (App O D (subst O D P n N1) (subst O D Q n N)))
 257     [@star_red_appl @HindP |@star_red_appr @HindQ]
 258   |#ty #P #HindP #i @star_red_lambda @HindP
 259   |#ty #v #Hindv #i @star_red_vec2 [>length_map >length_map //]
 260    #j #Q inversion v [#_ normalize //] #a #tl #_ #Hv
 261    cases (true_or_false (leb (S j) (|a::tl|))) #Hcase
 262     [lapply (leb_true_to_le … Hcase) -Hcase #Hcase
 263      >(nth_map ?????? a Hcase) >(nth_map ?????? a Hcase) #_ @Hindv >Hv @mem_nth //
 264     |>nth_to_default
 265       [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //]
 266      >nth_to_default
 267       [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] //
 268     ]
 269   ]
 270 qed.
 271
 272 lemma red_star_subst2 : ∀O,D,M,M1,N,i. is_closed O D 0 N →
 273   red O D M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N).
 274 #O #D #M #M1 #N #i #HNc #Hred lapply i -i elim Hred
 275   [#ty #P #Q #HQc #i normalize @starl_to_star @sstepl
 276    [|@rbeta >(subst_closed … HQc) //] >(subst_closed … HQc) //
 277     lapply (subst_lemma ?? P ?? i 0 (is_closed_mono … HQc) HNc) //
 278     <plus_n_Sm <plus_n_O #H <H //
 279   |#ty #v #a #P #HP #i normalize >(subst_closed … (le_O_n …)) //
 280    @R_to_star @riota @assoc_map @HP
 281   |#P #P1 #Q #Hred #Hind #i normalize @star_red_appl @Hind
 282   |#P #P1 #Q #Hred #Hind #i normalize @star_red_appr @Hind
 283   |#ty #P #P1 #Hred #Hind #i normalize @star_red_lambda @Hind
 284   |#ty #P #i normalize @starl_to_star @sstepl [|@rmem]
 285    @star_to_starl @star_red_vec2 [>length_map >length_map >length_map //]
 286    #n #Q >length_map #H
 287    cut (∃a:(FinSet_of_FType O D ty).True)
 288     [lapply H -H lapply (enum_complete (FinSet_of_FType O D ty))
 289      cases (enum (FinSet_of_FType O D ty))
 290       [#x normalize #H @False_ind @(absurd … H) @lt_to_not_le //
 291       |#x #l #_ #_ %{x} //
 292       ]
 293     ] * #a #_
 294    >(nth_map ?????? a H) >(nth_map ?????? Q) [2:>length_map @H]
 295    >(nth_map ?????? a H)
 296    lapply (subst_lemma O D P (to_T O D ty
 297     (nth n (FinSet_of_FType O D ty) (enum (FinSet_of_FType O D ty)) a))
 298    N i 0 (is_closed_mono … (is_closed_to_T …)) HNc) // <plus_n_O #H1 >H1
 299    <plus_n_Sm <plus_n_O //
 300   |#ty #P #Q #v #v1 #Hred #Hind #n normalize
 301    <map_append <map_append @star_red_vec @Hind
 302   ]
 303 qed.
 304
 305
 306
 307
 308