matita/matita/lib/lambda/terms/sequential_reduction.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "lambda/terms/multiplicity.ma".
  16
  17 include "lambda/notation/relations/seqred_2.ma".
  18
  19 (* SEQUENTIAL REDUCTION (SINGLE STEP) ***************************************)
  20
  21 (* Note: the application "(A B)" is represented by "@B.A" following:
  22          F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
  23          Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
  24 *)
  25 inductive sred: relation term ≝
  26 | sred_beta   : ∀B,A. sred (@B.𝛌.A) ([↙B]A)
  27 | sred_abst   : ∀A1,A2. sred A1 A2 → sred (𝛌.A1) (𝛌.A2)
  28 | sred_appl_sn: ∀B1,B2,A. sred B1 B2 → sred (@B1.A) (@B2.A)
  29 | sred_appl_dx: ∀B,A1,A2. sred A1 A2 → sred (@B.A1) (@B.A2)
  30 .
  31
  32 interpretation "sequential reduction"
  33    'SeqRed M N = (sred M N).
  34
  35 lemma sred_inv_vref: ∀M,N. M ↦ N → ∀i. #i = M → ⊥.
  36 #M #N * -M -N
  37 [ #B #A #i #H destruct
  38 | #A1 #A2 #_ #i #H destruct
  39 | #B1 #B2 #A #_ #i #H destruct
  40 | #B #A1 #A2 #_ #i #H destruct
  41 ]
  42 qed-.
  43
  44 lemma sred_inv_abst: ∀M,N. M ↦ N → ∀C1. 𝛌.C1 = M →
  45                      ∃∃C2. C1 ↦ C2 & 𝛌.C2 = N.
  46 #M #N * -M -N
  47 [ #B #A #C1 #H destruct
  48 | #A1 #A2 #HA12 #C1 #H destruct /2 width=3/
  49 | #B1 #B2 #A #_ #C1 #H destruct
  50 | #B #A1 #A2 #_ #C1 #H destruct
  51 ]
  52 qed-.
  53
  54 lemma sred_inv_appl: ∀M,N. M ↦ N → ∀D,C. @D.C = M →
  55                      ∨∨ (∃∃C0.  𝛌.C0 = C & [↙D] C0 = N)
  56                       | (∃∃D0. D ↦ D0 & @D0.C = N)
  57                       | (∃∃C0. C ↦ C0 & @D.C0 = N).
  58 #M #N * -M -N
  59 [ #B #A #D #C #H destruct /3 width=3/
  60 | #A1 #A2 #_ #D #C #H destruct
  61 | #B1 #B2 #A #HB12 #D #C #H destruct /3 width=3/
  62 | #B #A1 #A2 #HA12 #D #C #H destruct /3 width=3/
  63 ]
  64 qed-.
  65
  66 lemma sred_fwd_mult: ∀M,N. M ↦ N → ♯{N} < ♯{M} * ♯{M}.
  67 #M #N #H elim H -M -N
  68 [ #B #A @(le_to_lt_to_lt … (♯{A}*♯{B})) //
  69   normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *)
  70 | //
  71 | #B #D #A #_ #IHBD
  72   @(lt_to_le_to_lt … (♯{B}*♯{B}+♯{A})) [ /2 width=1/ ] -D
  73 | #B #A #C #_ #IHAC
  74   @(lt_to_le_to_lt … (♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] -C
  75 ]
  76 @(transitive_le … (♯{B}*♯{B}+♯{A}*♯{A})) [ /2 width=1/ ]
  77 >distributive_times_plus normalize /2 width=1/
  78 qed-.
  79
  80 lemma sred_lift: liftable sred.
  81 #h #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
  82 #B #A #d <dsubst_lift_le //
  83 qed.
  84
  85 lemma sred_inv_lift: deliftable_sn sred.
  86 #h #N1 #N2 #H elim H -N1 -N2
  87 [ #D #C #d #M1 #H
  88   elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
  89   elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
  90 | #C1 #C2 #_ #IHC12 #d #M1 #H
  91   elim (lift_inv_abst … H) -H #A1 #HAC1 #H
  92   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
  93   @(ex2_intro … (𝛌.A2)) // /2 width=1/
  94 | #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
  95   elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
  96   elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
  97   @(ex2_intro … (@B2.A)) // /2 width=1/
  98 | #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
  99   elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
 100   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
 101   @(ex2_intro … (@B.A2)) // /2 width=1/
 102 ]
 103 qed-.
 104
 105 lemma sred_dsubst: dsubstable_dx sred.
 106 #D1 #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
 107 #D2 #A #d >dsubst_dsubst_ge //
 108 qed.