1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "pointer_order.ma".
16 include "labelled_sequential_reduction.ma".
18 (* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************)
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).
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)
28 interpretation "labelled 'hap' reduction"
29 'HAp M p N = (lhap1 p M N).
31 notation "hvbox( M break ⓗ⇀ [ term 46 p ] break term 46 N )"
32 non associative with precedence 45
33 for @{ 'HAp $M $p $N }.
35 lemma lhap1_inv_nil: ∀p,M,N. M ⓗ⇀[p] N → ◊ = p →
36 ∃∃B,A. @B.𝛌.A = M & [⬐B]A = N.
38 [ #B #A #_ /2 width=4/
39 | #p #B #A1 #A2 #_ #H destruct
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.
46 [ #B #A #c #q #H destruct
47 | #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/
51 lemma lhap1_lift: ∀p. liftable (lhap1 p).
52 #p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
53 #B #A #d <dsubst_lift_le //
56 lemma lhap1_inv_lift: ∀p. deliftable_sn (lhap1 p).
57 #p #h #N1 #N2 #H elim H -p -N1 -N2
59 elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
60 elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
61 | #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
62 elim (lift_inv_appl … H) -H #B #A1 #H1 #H2 #H destruct
63 elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #H destruct (**) (* simplify line *)
64 @(ex2_intro … (@B.A2)) // /2 width=1/
68 lemma lhap1_dsubst: ∀p. dsubstable_dx (lhap1 p).
69 #p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
70 #D2 #A #d >dsubst_dsubst_ge //
73 lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N.
74 #p #H @(in_head_ind … H) -p
75 [ #M #N #H elim (lsred_inv_nil … H ?) -H //
77 elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] /3 width=1/ (**) (* simplify line *)
81 lemma lhap1_inv_head: ∀p,M,N. M ⓗ⇀[p] N → in_head p.
82 #p #M #N #H elim H -p -M -N // /2 width=1/
85 lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N.
86 #p #M #N #H elim H -p -M -N // /2 width=1/
89 theorem lhap1_mono: ∀p. singlevalued … (lhap1 p).
90 #p #M #N1 #H elim H -p -M -N1
92 elim (lhap1_inv_nil … H ?) -H // #D #C #H #HN2 destruct //
93 | #p #B #A1 #A2 #_ #IHA12 #N2 #H
94 elim (lhap1_inv_cons … H ???) -H [4: // |2,3: skip ] (**) (* simplify line *)
95 #D #C1 #C2 #_ #HC12 #H #HN2 destruct /3 width=1/