matita/matita/contribs/lambda/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 "labelled_sequential_reduction.ma".
  16
  17 (* KASHIMA'S "HAP" COMPUTATION (SINGLE STEP) ********************************)
  18
  19 (* Note: this is one step of the "head in application" computation of:
  20          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
  21 *)
  22 inductive hap1: relation term ≝
  23 | hap1_beta: ∀B,A. hap1 (@B.𝛌.A) ([⬐B]A)
  24 | hap1_appl: ∀B,A1,A2. hap1 A1 A2 → hap1 (@B.A1) (@B.A2)
  25 .
  26
  27 lemma hap1_lift: liftable hap1.
  28 #h #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
  29 #B #A #d <dsubst_lift_le //
  30 qed.
  31
  32 lemma hap1_inv_lift: deliftable hap1.
  33 #h #N1 #N2 #H elim H -N1 -N2
  34 [ #D #C #d #M1 #H
  35   elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
  36   elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
  37 | #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
  38   elim (lift_inv_appl … H) -H #B #A1 #H1 #H2 #H destruct
  39   elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #H destruct (**) (* simplify line *)
  40   @(ex2_1_intro … (@B.A2)) // /2 width=1/
  41 ]
  42 qed-.
  43
  44 lemma hap1_dsubstable: dsubstable_dx hap1.
  45 #D1 #M1 #M2 #H elim H -M1 -M2 normalize /2 width=1/
  46 #D2 #A #d >dsubst_dsubst_ge //
  47 qed.
  48
  49 lemma hap1_lsred: ∀M,N. hap1 M N →
  50                   ∃∃p. in_spine p & M ⇀[p] N.
  51 #M #N #H elim H -M -N /2 width=3/
  52 #B #A1 #A2 #_ * /3 width=3/
  53 qed-.