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