matita/matita/contribs/lambda/labelled_hap_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 "pointer_order.ma".
  16 include "labelled_sequential_reduction.ma".
  17
  18 (* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************)
  19
  20 (* Note: this is one step of the "head in application" computation of:
  21          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
  22 *)
  23 inductive lhap1: ptr → relation term ≝
  24 | hap1_beta: ∀B,A. lhap1 (◊) (@B.𝛌.A) ([⬐B]A)
  25 | hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2)
  26 .
  27
  28 interpretation "labelled 'hap' reduction"
  29    'HAp M p N = (lhap1 p M N).
  30
  31 notation "hvbox( M break ⓗ⇀ [ term 46 p ] break term 46 N )"
  32    non associative with precedence 45
  33    for @{ 'HAp $M $p $N }.
  34
  35 lemma lhap1_inv_nil: ∀p,M,N. M ⓗ⇀[p] N → ◊ = p →
  36                      ∃∃B,A. @B.𝛌.A = M & [⬐B]A = N.
  37 #p #M #N * -p -M -N
  38 [ #B #A #_ /2 width=4/
  39 | #p #B #A1 #A2 #_ #H destruct
  40 ]
  41 qed-.
  42
  43 lemma lhap1_inv_cons: ∀p,M,N. M ⓗ⇀[p] N → ∀c,q. c::q = p →
  44                       ∃∃B,A1,A2. dx = c & A1 ⓗ⇀[q] A2 & @B.A1 = M & @B.A2 = N.
  45 #p #M #N * -p -M -N
  46 [ #B #A #c #q #H destruct
  47 | #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/
  48 ]
  49 qed-.
  50
  51 lemma lhap1_inv_abst_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀A. 𝛌.A = M → ⊥.
  52 #p #M #N * -p -M -N
  53 [ #B #A #A0 #H destruct
  54 | #p #B #A1 #A2 #_ #A0 #H destruct
  55 ]
  56 qed-.
  57
  58 lemma lhap1_inv_appl_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀B,A. @B.A = M →
  59                          (∃∃C. ◊ = p & 𝛌.C = A & [⬐B]C = N) ∨
  60                          ∃∃q,C. A ⓗ⇀[q] C & dx::q = p & @B.C = N.
  61 #p #M #N * -p -M -N
  62 [ #B #A #B0 #A0 #H destruct /3 width=3/
  63 | #p #B #A1 #A2 #HA12 #B0 #A0 #H destruct /3 width=5/
  64 ]
  65 qed-.
  66
  67 lemma lhap1_inv_abst_dx: ∀p,M,N. M ⓗ⇀[p] N → ∀C. 𝛌.C = N →
  68                          ∃∃B,A. ◊ = p & @B.𝛌.A = M & 𝛌.C = [⬐B]A.
  69 #p #M #N * -p -M -N
  70 [ #B #A #C #H /2 width=4/
  71 | #p #B #A1 #A2 #_ #C #H destruct
  72 ]
  73 qed-.
  74
  75 lemma lhap1_lift: ∀p. liftable (lhap1 p).
  76 #p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
  77 #B #A #d <dsubst_lift_le //
  78 qed.
  79
  80 lemma lhap1_inv_lift: ∀p. deliftable_sn (lhap1 p).
  81 #p #h #N1 #N2 #H elim H -p -N1 -N2
  82 [ #D #C #d #M1 #H
  83   elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
  84   elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
  85 | #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
  86   elim (lift_inv_appl … H) -H #B #A1 #H1 #H2 #H destruct
  87   elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #H destruct (**) (* simplify line *)
  88   @(ex2_intro … (@B.A2)) // /2 width=1/
  89 ]
  90 qed-.
  91
  92 lemma lhap1_dsubst: ∀p. dsubstable_dx (lhap1 p).
  93 #p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
  94 #D2 #A #d >dsubst_dsubst_ge //
  95 qed.
  96
  97 lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N.
  98 #p #H @(in_head_ind … H) -p
  99 [ #M #N #H elim (lsred_inv_nil … H ?) -H //
 100 | #p #_ #IHp #M #N #H
 101   elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] /3 width=1/ (**) (* simplify line *)
 102 ]
 103 qed.
 104
 105 lemma lhap1_inv_head: ∀p,M,N. M ⓗ⇀[p] N → in_head p.
 106 #p #M #N #H elim H -p -M -N // /2 width=1/
 107 qed-.
 108
 109 lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N.
 110 #p #M #N #H elim H -p -M -N // /2 width=1/
 111 qed-.
 112
 113 lemma lhap1_fwd_le: ∀p1,M1,M. M1 ⓗ⇀[p1] M → ∀p2,M2. M ⓗ⇀[p2] M2 → p1 ≤ p2.
 114 #p1 #M1 #M #H elim H -p1 -M1 -M //
 115 #p1 #B #A1 #A2 #HA12 #IHA12 #p2 #M2 #H
 116 elim (lhap1_inv_appl_sn … H ???) -H [5: // |2,3: skip ] * (**) (* simplify line *)
 117 [ -IHA12 #C2 #Hp2 #HAC2 #_
 118   elim (lhap1_inv_abst_dx … HA12 … HAC2) -A2 #B1 #C1 #Hp1 #_ #_ //
 119 | -HA12 /3 width=2/
 120 ]
 121 qed-.
 122
 123 theorem lhap1_mono: ∀p. singlevalued … (lhap1 p).
 124 #p #M #N1 #H elim H -p -M -N1
 125 [ #B #A #N2 #H
 126   elim (lhap1_inv_nil … H ?) -H // #D #C #H #HN2 destruct //
 127 | #p #B #A1 #A2 #_ #IHA12 #N2 #H
 128   elim (lhap1_inv_cons … H ???) -H [4: // |2,3: skip ] (**) (* simplify line *)
 129   #D #C1 #C2 #_ #HC12 #H #HN2 destruct /3 width=1/
 130 ]
 131 qed-.