matita/matita/contribs/lambda/st_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_hap_computation.ma".
  16
  17 (* KASHIMA'S "ST" COMPUTATION ***********************************************)
  18
  19 (* Note: this is the "standard" computation of:
  20          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
  21 *)
  22 inductive st: relation term ≝
  23 | st_vref: ∀s,M,i. M ⓗ⇀*[s] #i → st M (#i)
  24 | st_abst: ∀s,M,A1,A2. M ⓗ⇀*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
  25 | st_appl: ∀s,M,B1,B2,A1,A2. M ⓗ⇀*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
  26 .
  27
  28 interpretation "'st' computation"
  29     'Std M N = (st M N).
  30
  31 notation "hvbox( M ⓢ⥤* break term 46 N )"
  32    non associative with precedence 45
  33    for @{ 'Std $M $N }.
  34
  35 axiom st_refl: reflexive … st.
  36
  37 axiom st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ⥤* N2.
  38
  39 axiom st_lift: liftable st.
  40
  41 axiom st_inv_lift: deliftable_sn st.
  42
  43 axiom st_dsubst: dsubstable st.
  44
  45 lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⥤* N →
  46                            ∃∃r. M ⇀*[r] N & is_le r.
  47 #M #N #H elim H -M -N
  48 [ #s #M #i #H
  49   lapply (lhap_inv_lsreds … H)
  50   lapply (lhap_inv_head … H) -H #H
  51   lapply (is_head_is_le … H) -H /2 width=3/
  52 | #s #M #A1 #A2 #H #_ * #r #HA12 #Hr
  53   lapply (lhap_inv_lsreds … H) #HM
  54   lapply (lhap_inv_head … H) -H #Hs
  55   lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
  56   @(ex2_intro … HM) -M -A2 /3 width=1/
  57 | #s #M #B1 #B2 #A1 #A2 #H #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
  58   lapply (lhap_inv_lsreds … H) #HM
  59   lapply (lhap_inv_head … H) -H #Hs
  60   lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
  61   lapply (lsreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM
  62   @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/
  63 ]
  64 qed-.