matita/matita/contribs/lambda/labelled_hap_computation.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 "labelled_sequential_computation.ma".
  16 include "labelled_hap_reduction.ma".
  17
  18 (* KASHIMA'S "HAP" COMPUTATION (LABELLED MULTISTEP) *************************)
  19
  20 (* Note: this is the "head in application" computation of:
  21          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
  22 *)
  23 definition lhap: pseq → relation term ≝ lstar … lhap1.
  24
  25 interpretation "labelled 'hap' computation"
  26    'HApStar M p N = (lhap p M N).
  27
  28 notation "hvbox( M break ⓗ⇀* [ term 46 p ] break term 46 N )"
  29    non associative with precedence 45
  30    for @{ 'HApStar $M $p $N }.
  31
  32 lemma lhap1_lhap: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
  33 /2 width=1/
  34 qed.
  35
  36 lemma lhap_inv_nil: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → ◊ = s → M1 = M2.
  37 /2 width=5 by lstar_inv_nil/
  38 qed-.
  39
  40 lemma lhap_inv_cons: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → ∀q,r. q::r = s →
  41                      ∃∃M. M1 ⓗ⇀[q] M & M ⓗ⇀*[r] M2.
  42 /2 width=3 by lstar_inv_cons/
  43 qed-.
  44
  45 lemma lhap_inv_lhap1: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
  46 /2 width=1 by lstar_inv_step/
  47 qed-.
  48
  49 lemma lhap_lift: ∀s. liftable (lhap s).
  50 /2 width=1/
  51 qed.
  52
  53 lemma lhap_inv_lift: ∀s. deliftable_sn (lhap s).
  54 /3 width=3 by lstar_deliftable_sn, lhap1_inv_lift/
  55 qed-.
  56
  57 lemma lhap_dsubst: ∀s. dsubstable_dx (lhap s).
  58 /2 width=1/
  59 qed.
  60
  61 theorem lhap_mono: ∀s. singlevalued … (lhap s).
  62 /3 width=7 by lstar_singlevalued, lhap1_mono/
  63 qed-.
  64
  65 theorem lhap_trans: ∀s1,M1,M. M1 ⓗ⇀*[s1] M →
  66                     ∀s2,M2. M ⓗ⇀*[s2] M2 → M1 ⓗ⇀*[s1@s2] M2.
  67 /2 width=3 by lstar_trans/
  68 qed-.
  69
  70 lemma lhap_appl: ∀s,B,A1,A2. A1 ⓗ⇀*[s] A2 → @B.A1 ⓗ⇀*[dx:::s] @B.A2.
  71 #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
  72 qed.
  73
  74 lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2.
  75 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
  76 #a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/
  77 qed.
  78
  79 lemma lhap_inv_head: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_head s.
  80 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
  81 #p #s #M1 #M #HM1 #_ #IHM2
  82 lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/
  83 qed-.
  84
  85 lemma lhap_inv_lsreds: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
  86 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
  87 #p #s #M1 #M #HM1 #_ #IHM2
  88 lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/
  89 qed-.
  90
  91 lemma lhap_fwd_le: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s.
  92 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 /3 width=3/
  93 #a1 #s #M1 #M #HM1 #IHM1
  94 generalize in match HM1; -HM1
  95 cases IHM1 -s -M -M2 //
  96 #a #M0 #M #HM0 #s #M2 #_ #HM10 #H -M2
  97 lapply (lhap1_fwd_le … HM10 … HM0) -M -M0 -M1 /2 width=1/
  98 qed-.