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