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