matita/matita/lib/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 "lambda/par_reduction.ma".
  13 include "basics/star.ma".
  14
  15 (*
  16 inductive T : Type[0] ≝
  17   | Sort: nat → T
  18   | Rel: nat → T
  19   | App: T → T → T
  20   | Lambda: T → T → T (* type, body *)
  21   | Prod: T → T → T (* type, body *)
  22   | D: T →T
  23 . *)
  24
  25 inductive red : T →T → Prop ≝
  26   | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N])
  27   | rdapp: ∀M,N. red (App (D M) N) (D (App M N))
  28   | rdlam: ∀M,N. red (Lambda M (D N)) (D (Lambda M N))
  29   | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
  30   | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1)
  31   | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
  32   | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1)
  33   | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
  34   | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
  35   | d: ∀M,M1. red M M1 → red (D M) (D M1).
  36
  37 lemma red_to_pr: ∀M,N. red M N → pr M N.
  38 #M #N #redMN (elim redMN) /2/
  39 qed.
  40
  41 lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N.
  42 #M #P #redMP (inversion redMP)
  43   [#P1 #M1 #N1 #eqH destruct
  44   |#M1 #N1 #eqH destruct
  45   |#M1 #N1 #eqH destruct
  46   |4,5,6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
  47   |#Q1 #M1 #red1 #_ #eqH destruct #eqP @(ex_intro … M1) /2/
  48   ]
  49 qed.
  50
  51 lemma red_lambda : ∀M,N,P. red (Lambda M N) P →
  52  (∃M1. P = (Lambda M1 N) ∧ red M M1) ∨
  53  (∃N1. P = (Lambda M N1) ∧ red N N1) ∨
  54  (∃Q. N = D Q ∧ P = D (Lambda M Q)).
  55 #M #N #P #redMNP (inversion redMNP)
  56   [#P1 #M1 #N1 #eqH destruct
  57   |#M1 #N1 #eqH destruct
  58   |#M1 #N1 #eqH destruct #eqP %2 (@(ex_intro … N1)) % //
  59   |4,5,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
  60   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %1
  61    (@(ex_intro … M1)) % //
  62   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
  63    (@(ex_intro … N1)) % //
  64   |#Q1 #M1 #red1 #_ #eqH destruct
  65   ]
  66 qed.
  67
  68 lemma red_prod : ∀M,N,P. red (Prod M N) P →
  69  (∃M1. P = (Prod M1 N) ∧ red M M1) ∨
  70  (∃N1. P = (Prod M N1) ∧ red N N1).
  71 #M #N #P #redMNP (inversion redMNP)
  72   [#P1 #M1 #N1 #eqH destruct
  73   |2,3: #M1 #N1 #eqH destruct
  74   |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
  75   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
  76    (@(ex_intro … M1)) % //
  77   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
  78    (@(ex_intro … N1)) % //
  79   |#Q1 #M1 #red1 #_ #eqH destruct
  80   ]
  81 qed.
  82
  83 lemma red_app : ∀M,N,P. red (App M N) P →
  84  (∃M1,N1. M =  (Lambda M1 N1) ∧ P = N1[0:=N]) ∨
  85  (∃M1. M =  (D M1) ∧ P = D (App M1 N)) ∨
  86  (∃M1. P = (App M1 N) ∧ red M M1) ∨
  87  (∃N1. P = (App M N1) ∧ red N N1).
  88 #M #N #P #redMNP (inversion redMNP)
  89   [#P1 #M1 #N1 #eqH destruct #eqP %1 %1 %1
  90    @(ex_intro … P1) @(ex_intro … M1) % //
  91   |#M1 #N1 #eqH destruct #eqP %1 %1 %2 /3/
  92   |#M1 #N1 #eqH destruct
  93   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
  94    (@(ex_intro … M1)) % //
  95   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
  96    (@(ex_intro … N1)) % //
  97   |6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
  98   |#Q1 #M1 #red1 #_ #eqH destruct
  99   ]
 100 qed.
 101
 102 definition reduct ≝ λn,m. red m n.
 103
 104 definition SN ≝ WF ? reduct.
 105
 106 definition NF ≝ λM. ∀N. ¬ (reduct N M).
 107
 108 theorem NF_to_SN: ∀M. NF M → SN M.
 109 #M #nfM % #a #red @False_ind /2/
 110 qed.
 111
 112 lemma NF_Sort: ∀i. NF (Sort i).
 113 #i #N % #redN (inversion redN)
 114   [1: #P #N #M #H destruct
 115   |2,3 :#N #M #H destruct
 116   |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
 117   |#M #N #_ #_ #H destruct
 118   ]
 119 qed.
 120
 121 lemma NF_Rel: ∀i. NF (Rel i).
 122 #i #N % #redN (inversion redN)
 123   [1: #P #N #M #H destruct
 124   |2,3 :#N #M #H destruct
 125   |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
 126   |#M #N #_ #_ #H destruct
 127   ]
 128 qed.
 129
 130 lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N].
 131 #N @Telim_size #P (cases P)
 132   [1,2:#j #Hind #M1 #i #r1 @False_ind /2/
 133   |#P #Q #Hind #M1 #i #r1 (cases (red_app … r1))
 134     [*
 135       [*
 136         [* #M2 * #N2 * #eqP #eqM1 >eqP normalize
 137          >eqM1 >(plus_n_O i) >(subst_lemma N2) <(plus_n_O i)
 138          (cut (i+1 =S i)) [//] #Hcut >Hcut @rbeta
 139         |* #M2 * #eqP #eqM1 >eqM1 >eqP normalize @rdapp
 140         ]
 141       |* #M2 * #eqM1 #rP >eqM1 normalize @rappl @Hind /2/
 142       ]
 143     |* #N2 * #eqM1 #rQ >eqM1 normalize @rappr @Hind /2/
 144     ]
 145   |#P #Q #Hind #M1 #i #r1 (cases (red_lambda …r1))
 146     [*
 147       [* #P1 * #eqM1 #redP >eqM1 normalize @rlaml @Hind /2/
 148       |* #Q1 * #eqM1 #redP >eqM1 normalize @rlamr @Hind /2/
 149       ]
 150     |* #M2 * #eqQ #eqM1 >eqM1 >eqQ normalize @rdlam
 151     ]
 152   |#P #Q #Hind #M1 #i #r1 (cases (red_prod …r1))
 153     [* #P1 * #eqM1 #redP >eqM1 normalize @rprodl @Hind /2/
 154     |* #P1 * #eqM1 #redP >eqM1 normalize @rprodr @Hind /2/
 155     ]
 156   |#P #Hind #M1 #i #r1 (cases (red_d …r1))
 157    #P1 * #eqM1 #redP >eqM1 normalize @d @Hind /2/
 158   ]
 159 qed.
 160
 161 lemma red_lift: ∀N,N1,n. red N N1 → ∀k. red (lift N k n) (lift N1 k n).
 162 #N #N1 #n #r1 (elim r1) normalize /2/
 163 qed.
 164
 165 (* star red *)
 166 lemma star_appl: ∀M,M1,N. star … red M M1 →
 167   star … red (App M N) (App M1 N).
 168 #M #M1 #N #star1 (elim star1) //
 169 #B #C #starMB #redBC #H @(inj … H) /2/
 170 qed.
 171
 172 lemma star_appr: ∀M,N,N1. star … red N N1 →
 173   star … red (App M N) (App M N1).
 174 #M #N #N1 #star1 (elim star1) //
 175 #B #C #starMB #redBC #H @(inj … H) /2/
 176 qed.
 177
 178 lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
 179   star … red (App M N) (App M1 N1).
 180 #M #M1 #N #N1 #redM #redN @(trans_star ??? (App M1 N)) /2/
 181 qed.
 182
 183 lemma star_laml: ∀M,M1,N. star … red M M1 →
 184   star … red (Lambda M N) (Lambda M1 N).
 185 #M #M1 #N #star1 (elim star1) //
 186 #B #C #starMB #redBC #H @(inj … H) /2/
 187 qed.
 188
 189 lemma star_lamr: ∀M,N,N1. star … red N N1 →
 190   star … red (Lambda M N) (Lambda M N1).
 191 #M #N #N1 #star1 (elim star1) //
 192 #B #C #starMB #redBC #H @(inj … H) /2/
 193 qed.
 194
 195 lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
 196   star … red (Lambda M N) (Lambda M1 N1).
 197 #M #M1 #N #N1 #redM #redN @(trans_star ??? (Lambda M1 N)) /2/
 198 qed.
 199
 200 lemma star_prodl: ∀M,M1,N. star … red M M1 →
 201   star … red (Prod M N) (Prod M1 N).
 202 #M #M1 #N #star1 (elim star1) //
 203 #B #C #starMB #redBC #H @(inj … H) /2/
 204 qed.
 205
 206 lemma star_prodr: ∀M,N,N1. star … red N N1 →
 207   star … red (Prod M N) (Prod M N1).
 208 #M #N #N1 #star1 (elim star1) //
 209 #B #C #starMB #redBC #H @(inj … H) /2/
 210 qed.
 211
 212 lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
 213   star … red (Prod M N) (Prod M1 N1).
 214 #M #M1 #N #N1 #redM #redN @(trans_star ??? (Prod M1 N)) /2/
 215 qed.
 216
 217 lemma star_d: ∀M,M1. star … red M M1 →
 218   star … red (D M) (D M1).
 219 #M #M1 #redM (elim redM) // #B #C #starMB #redBC #H @(inj … H) /2/
 220 qed.
 221
 222 lemma red_subst1 : ∀M,N,N1,i. red N N1 →
 223  (star … red) M[i≝N] M[i≝N1].
 224 #M (elim M)
 225   [//
 226   |#i #P #Q #n #r1 (cases (true_or_false (leb i n)))
 227     [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
 228       [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
 229       |#eqin >eqin >subst_rel2 >subst_rel2 @R_to_star /2/
 230       ]
 231     |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
 232      >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
 233     ]
 234   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_app /2/
 235   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_lam /2/
 236   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_prod /2/
 237   |#P #Hind #M #N #i #r1 normalize @star_d /2/
 238   ]
 239 qed.
 240
 241 lemma SN_d : ∀M. SN M → SN (D M).
 242 #M #snM (elim snM) #b #H #Hind % #a #redd (cases (red_d … redd))
 243 #Q * #eqa #redbQ >eqa @Hind //
 244 qed.
 245
 246 lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M.
 247 #N * #b #H #M #red @H //.
 248 qed.
 249
 250 lemma SN_star: ∀M,N. (star … red) N M → SN N → SN M.
 251 #M #N #rstar (elim rstar) //
 252 #Q #P #HbQ  #redQP #snNQ #snN @(SN_step …redQP) /2/
 253 qed.
 254
 255 lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
 256 ∃M1.subterm N1 M1 ∧ red M M1.
 257 #M #N #subN (elim subN) /4/
 258 (* trsansitive case *)
 259 #P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP))
 260 #B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
 261 @(ex_intro … C) /3/
 262 qed.
 263
 264 axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 →
 265 ∃M1.subterm N1 M1 ∧ red M M1.
 266
 267 lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N.
 268 #M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN
 269 (cases (sub_red … subNM ? redN)) #M1 *
 270 #subN1M1 #redMM1 @(HindM … redMM1) //
 271 qed.
 272
 273 lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N.
 274 #M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H
 275 lapply (H Hstar) #Hstari (elim Hstari) //
 276 #M #N #_ #subNM #snM @(SN_subterm …subNM) //
 277 qed.
 278
 279 definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M.
 280
 281 definition SH ≝ WF ? shrink.
 282
 283 lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N.
 284 #M #snM (elim snM) #M
 285 #snM #HindM #N #subNM (cases (star_case ???? subNM))
 286   [#eqNM >eqNM % /2/
 287   |#subsNM % #N1 *
 288     [#redN (cases (sub_star_red … subNM ? redN)) #M1 *
 289      #subN1M1 #redMM1 @(HindM M1) /2/
 290     |#subN1 @(HindM N) /2/
 291     ]
 292   ]
 293 qed.
 294
 295 theorem SN_to_SH: ∀N. SN N → SH N.
 296 #N #snN (elim snN) (@Telim_size)
 297 #b #Hsize #snb #Hind % #a * /2/ #subab @Hsize;
 298   [(elim subab)
 299     [#c #subac @size_subterm //
 300     |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm //
 301     ]
 302   |@SN_step @(SN_subterm_star b);
 303     [% /2/ |@TC_to_star @subab] % @snb
 304   |#a1 #reda1 cases(sub_star_red b a ?? reda1);
 305     [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ]
 306   ]
 307 qed.
 308
 309 lemma SH_to_SN: ∀N. SH N → SN N.
 310 @WF_antimonotonic /2/ qed.
 311
 312 lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
 313 #N #snN (elim snN) #P #shP #HindP #M #snM
 314 (* for M we proceed by induction on SH *)
 315 (lapply (SN_to_SH ? snM)) #shM (elim shM)
 316 #Q #shQ #HindQ % #a #redH (cases (red_lambda … redH))
 317   [*
 318     [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
 319      @SH_to_SN % /2/
 320     |* #S * #eqa #redQS >eqa @(HindQ S) /2/
 321     ]
 322   |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
 323   ]
 324 qed.
 325
 326 (*
 327 lemma SH_Lambda: ∀N.SH N → ∀M.SH M → SN (Lambda N M).
 328 #N #snN (elim snN) #P #snP #HindP #M #snM (elim snM)
 329 #Q #snQ #HindQ % #a #redH (cases (red_lambda … redH))
 330   [*
 331     [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) /2/
 332      % /2/
 333     |* #S * #eqa #redQS >eqa @(HindQ S) /2/
 334     ]
 335   |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
 336   ]
 337 qed. *)
 338
 339 lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M).
 340 #N #snN (elim snN) #P #shP #HindP #M #snM (elim snM)
 341 #Q #snQ #HindQ % #a #redH (cases (red_prod … redH))
 342   [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
 343    % /2/
 344   |* #S * #eqa #redQS >eqa @(HindQ S) /2/
 345   ]
 346 qed.
 347
 348 lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M.
 349 #i #N (cut (∀P.SN P → ∀M.P=M[i ≝ N] → SN M));
 350   [#P #H (elim H) #Q #snQ #Hind #M #eqM % #M1 #redM
 351    @(Hind M1[i:=N]) // >eqM /2/
 352   |#Hcut #M #snM @(Hcut … snM) //
 353 qed.
 354
 355 lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
 356   SN M[0:=N] → SN (App (Lambda P M) N).
 357 #P #snP (elim snP) #A #snA #HindA
 358 #N #snN (elim snN) #B #snB #HindB
 359 #M #snM1 (cut (SN M)) [@(SN_subst … snM1)] #snM
 360 (generalize in match snM1) (elim snM)
 361 #C #snC #HindC #snC1 % #Q #redQ (cases (red_app … redQ))
 362   [*
 363     [*
 364       [* #M2 * #N2 * #eqlam destruct #eqQ //
 365       |* #M2 * #eqlam destruct
 366       ]
 367     |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam))
 368       [*
 369         [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/
 370         |* #M3 * #eqM2 #r2 >eqM2 @HindC //
 371          @(SN_step … snC1) /2/
 372         ]
 373       |* #M3 * #eqC #eqM2 (* TODO *)
 374       ]
 375     ]
 376   |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1)
 377    @red_subst1 //
 378   ]
 379
 380
 381
 382
 383
 384