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 definition reduct ≝ λn,m. red m n.
  69
  70 definition SN ≝ WF ? reduct.
  71
  72 definition NF ≝ λM. ∀N. ¬ (reduct N M).
  73
  74 theorem NF_to_SN: ∀M. NF M → SN M.
  75 #M #nfM % #a #red @False_ind /2/
  76 qed.
  77
  78 lemma NF_Sort: ∀i. NF (Sort i).
  79 #i #N % #redN (inversion redN)
  80   [1: #P #N #M #H destruct
  81   |2,3 :#N #M #H destruct
  82   |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
  83   |#M #N #_ #_ #H destruct
  84   ]
  85 qed.
  86
  87 lemma NF_Rel: ∀i. NF (Rel i).
  88 #i #N % #redN (inversion redN)
  89   [1: #P #N #M #H destruct
  90   |2,3 :#N #M #H destruct
  91   |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
  92   |#M #N #_ #_ #H destruct
  93   ]
  94 qed.
  95
  96 lemma SN_d : ∀M. SN M → SN (D M).
  97 #M #snM (elim snM) #b #H #Hind % #a #redd (cases (red_d … redd))
  98 #Q * #eqa #redbQ >eqa @Hind //
  99 qed.
 100
 101 lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M.
 102 #N * #b #H #M #red @H //.
 103 qed.
 104
 105 lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
 106 ∃M1.subterm N1 M1 ∧ red M M1.
 107 #M #N #subN (elim subN) /4/
 108 (* trsansitive case *)
 109 #P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP))
 110 #B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
 111 @(ex_intro … C) /3/
 112 qed.
 113
 114 axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 →
 115 ∃M1.subterm N1 M1 ∧ red M M1.
 116
 117 lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N.
 118 #M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN
 119 (cases (sub_red … subNM ? redN)) #M1 *
 120 #subN1M1 #redMM1 @(HindM … redMM1) //
 121 qed.
 122
 123 lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N.
 124 #M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H
 125 lapply (H Hstar) #Hstari (elim Hstari) //
 126 #M #N #_ #subNM #snM @(SN_subterm …subNM) //
 127 qed.
 128
 129 definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M.
 130
 131 definition SH ≝ WF ? shrink.
 132
 133 lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N.
 134 #M #snM (elim snM) #M
 135 #snM #HindM #N #subNM (cases (star_case ???? subNM))
 136   [#eqNM >eqNM % /2/
 137   |#subsNM % #N1 *
 138     [#redN (cases (sub_star_red … subNM ? redN)) #M1 *
 139      #subN1M1 #redMM1 @(HindM M1) /2/
 140     |#subN1 @(HindM N) /2/
 141     ]
 142   ]
 143 qed.
 144
 145 theorem SN_to_SH: ∀N. SN N → SH N.
 146 #N #snN (elim snN) (@Telim_size)
 147 #b #Hsize #snb #Hind % #a * /2/ #subab @Hsize;
 148   [(elim subab)
 149     [#c #subac @size_subterm //
 150     |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm //
 151     ]
 152   |@SN_step @(SN_subterm_star b);
 153     [% /2/ |@TC_to_star @subab] % @snb
 154   |#a1 #reda1 cases(sub_star_red b a ?? reda1);
 155     [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ]
 156   ]
 157 qed.
 158
 159 lemma SH_to_SN: ∀N. SH N → SN N.
 160 @WF_antimonotonic /2/ qed.
 161
 162 lemma SH_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
 163 #N #snN (elim snN) #P #shP #HindP #M #snM
 164 (* for M we proceed by induction on SH *)
 165 (lapply (SN_to_SH ? snM)) #shM (elim shM)
 166 #Q #shQ #HindQ % #a #redH (cases (red_lambda … redH))
 167   [*
 168     [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
 169      @SH_to_SN % /2/
 170     |* #S * #eqa #redQS >eqa @(HindQ S) /2/
 171     ]
 172   |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
 173   ]
 174 qed.
 175
 176 (*
 177 lemma SH_Lambda: ∀N.SH N → ∀M.SH M → SN (Lambda N M).
 178 #N #snN (elim snN) #P #snP #HindP #M #snM (elim snM)
 179 #Q #snQ #HindQ % #a #redH (cases (red_lambda … redH))
 180   [*
 181     [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) /2/
 182      % /2/
 183     |* #S * #eqa #redQS >eqa @(HindQ S) /2/
 184     ]
 185   |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
 186   ]
 187 qed. *)
 188
 189
 190
 191
 192
 193