'DSubst D d M = (dsubst D d M).
(* Note: the notation with "/" does not work *)
-notation "hvbox( [ term 46 d â¬\90 break term 46 D ] break term 46 M )"
+notation "hvbox( [ term 46 d â\86\99 break term 46 D ] break term 46 M )"
non associative with precedence 46
for @{ 'DSubst $D $d $M }.
-notation > "hvbox( [ â¬\90 term 46 D ] break term 46 M )"
+notation > "hvbox( [ â\86\99 term 46 D ] break term 46 M )"
non associative with precedence 46
for @{ 'DSubst $D 0 $M }.
-lemma dsubst_vref_lt: â\88\80i,d,D. i < d â\86\92 [d â¬\90 D] #i = #i.
+lemma dsubst_vref_lt: â\88\80i,d,D. i < d â\86\92 [d â\86\99 D] #i = #i.
normalize /2 width=1/
qed.
-lemma dsubst_vref_eq: ∀d,D. [d ⬐ D] #d = ↑[d]D.
+lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
normalize //
qed.
-lemma dsubst_vref_gt: â\88\80i,d,D. d < i â\86\92 [d â¬\90 D] #i = #(i-1).
+lemma dsubst_vref_gt: â\88\80i,d,D. d < i â\86\92 [d â\86\99 D] #i = #(i-1).
normalize /2 width=1/
qed.
theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
- [d2 â¬\90 â\86\91[d1 - d2, h] D] â\86\91[d1 + 1, h] M = â\86\91[d1, h] [d2 â¬\90 D] M.
+ [d2 â\86\99 â\86\91[d1 - d2, h] D] â\86\91[d1 + 1, h] M = â\86\91[d1, h] [d2 â\86\99 D] M.
#h #D #M elim M -M
[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
[ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
qed.
theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
- [d2 â¬\90 D] ↑[d1, h + 1] M = ↑[d1, h] M.
+ [d2 â\86\99 D] ↑[d1, h + 1] M = ↑[d1, h] M.
#h #D #M elim M -M
[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
[ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
qed.
theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
- [d2 â¬\90 D] â\86\91[d1, h] M = â\86\91[d1, h] [d2 - h â¬\90 D] M.
+ [d2 â\86\99 D] â\86\91[d1, h] M = â\86\91[d1, h] [d2 - h â\86\99 D] M.
#h #D #M elim M -M
[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
[ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
qed.
theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
- [d2 â¬\90 D2] [d1 â¬\90 D1] M = [d1 â¬\90 [d2 - d1 â¬\90 D2] D1] [d2 + 1 â¬\90 D2] M.
+ [d2 â\86\99 D2] [d1 â\86\99 D1] M = [d1 â\86\99 [d2 - d1 â\86\99 D2] D1] [d2 + 1 â\86\99 D2] M.
#D1 #D2 #M elim M -M
[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
[ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
qed.
theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
- [d2 â¬\90 [d1 - d2 -1 â¬\90 D1] D2] [d1 â¬\90 D1] M = [d1 - 1 â¬\90 D1] [d2 â¬\90 D2] M.
+ [d2 â\86\99 [d1 - d2 -1 â\86\99 D1] D2] [d1 â\86\99 D1] M = [d1 - 1 â\86\99 D1] [d2 â\86\99 D2] M.
#D1 #D2 #M #d1 #d2 #Hd21
lapply (ltn_to_ltO … Hd21) #Hd1
>dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
qed.
definition dsubstable_dx: predicate (relation term) ≝ λR.
- â\88\80D,M1,M2. R M1 M2 â\86\92 â\88\80d. R ([d â¬\90 D] M1) ([d â¬\90 D] M2).
-
+ â\88\80D,M1,M2. R M1 M2 â\86\92 â\88\80d. R ([d â\86\99 D] M1) ([d â\86\99 D] M2).
+(*
definition dsubstable_sn: predicate (relation term) ≝ λR.
- â\88\80D1,D2. R D1 D2 â\86\92 â\88\80M,d. R ([d â¬\90 D1] M) ([d â¬\90 D2] M).
-
+ â\88\80D1,D2. R D1 D2 â\86\92 â\88\80M,d. R ([d â\86\99 D1] M) ([d â\86\99 D2] M).
+*)
definition dsubstable: predicate (relation term) ≝ λR.
- â\88\80D1,D2. R D1 D2 â\86\92 â\88\80M1,M2. R M1 M2 â\86\92 â\88\80d. R ([d â¬\90 D1] M1) ([d â¬\90 D2] M2).
+ â\88\80D1,D2. R D1 D2 â\86\92 â\88\80M1,M2. R M1 M2 â\86\92 â\88\80d. R ([d â\86\99 D1] M1) ([d â\86\99 D2] M2).
lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
#R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
qed.
-
+(*
lemma star_dsubstable_sn: ∀R. dsubstable_sn R → dsubstable_sn (star … R).
#R #HR #D1 #D2 #H elim H -D2 // /3 width=3/
qed.
-
+*)
lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) →
∀l. dsubstable_dx (lstar T … R l).
#T #R #HR #l #D #M1 #M2 #H
interpretation "labelled 'hap' computation"
'HApStar M p N = (lhap p M N).
-notation "hvbox( M break â\93\97â\87\80* [ term 46 p ] break term 46 N )"
+notation "hvbox( M break â\93\97â\86¦* [ term 46 p ] break term 46 N )"
non associative with precedence 45
for @{ 'HApStar $M $p $N }.
-lemma lhap_step_rc: â\88\80p,M1,M2. M1 â\93\97â\87\80[p] M2 â\86\92 M1 â\93\97â\87\80*[p::◊] M2.
+lemma lhap_step_rc: â\88\80p,M1,M2. M1 â\93\97â\86¦[p] M2 â\86\92 M1 â\93\97â\86¦*[p::◊] M2.
/2 width=1/
qed.
-lemma lhap_inv_nil: â\88\80s,M1,M2. M1 â\93\97â\87\80*[s] M2 → ◊ = s → M1 = M2.
+lemma lhap_inv_nil: â\88\80s,M1,M2. M1 â\93\97â\86¦*[s] M2 → ◊ = s → M1 = M2.
/2 width=5 by lstar_inv_nil/
qed-.
-lemma lhap_inv_cons: â\88\80s,M1,M2. M1 â\93\97â\87\80*[s] M2 → ∀q,r. q::r = s →
- â\88\83â\88\83M. M1 â\93\97â\87\80[q] M & M â\93\97â\87\80*[r] M2.
+lemma lhap_inv_cons: â\88\80s,M1,M2. M1 â\93\97â\86¦*[s] M2 → ∀q,r. q::r = s →
+ â\88\83â\88\83M. M1 â\93\97â\86¦[q] M & M â\93\97â\86¦*[r] M2.
/2 width=3 by lstar_inv_cons/
qed-.
-lemma lhap_inv_step_rc: â\88\80p,M1,M2. M1 â\93\97â\87\80*[p::â\97\8a] M2 â\86\92 M1 â\93\97â\87\80[p] M2.
+lemma lhap_inv_step_rc: â\88\80p,M1,M2. M1 â\93\97â\86¦*[p::â\97\8a] M2 â\86\92 M1 â\93\97â\86¦[p] M2.
/2 width=1 by lstar_inv_step/
qed-.
-lemma lhap_inv_pos: â\88\80s,M1,M2. M1 â\93\97â\87\80*[s] M2 → 0 < |s| →
- â\88\83â\88\83p,r,M. p::r = s & M1 â\93\97â\87\80[p] M & M â\93\97â\87\80*[r] M2.
+lemma lhap_inv_pos: â\88\80s,M1,M2. M1 â\93\97â\86¦*[s] M2 → 0 < |s| →
+ â\88\83â\88\83p,r,M. p::r = s & M1 â\93\97â\86¦[p] M & M â\93\97â\86¦*[r] M2.
/2 width=1 by lstar_inv_pos/
qed-.
/2 width=3 by lstar_ltransitive/
qed-.
-lemma lhap_step_dx: â\88\80s,M1,M. M1 â\93\97â\87\80*[s] M →
- â\88\80p,M2. M â\93\97â\87\80[p] M2 â\86\92 M1 â\93\97â\87\80*[s@p::◊] M2.
+lemma lhap_step_dx: â\88\80s,M1,M. M1 â\93\97â\86¦*[s] M →
+ â\88\80p,M2. M â\93\97â\86¦[p] M2 â\86\92 M1 â\93\97â\86¦*[s@p::◊] M2.
#s #M1 #M #HM1 #p #M2 #HM2
@(lhap_trans … HM1) /2 width=1/
qed-.
-lemma head_lsreds_lhap: â\88\80s,M1,M2. M1 â\87\80*[s] M2 â\86\92 is_head s â\86\92 M1 â\93\97â\87\80*[s] M2.
+lemma head_lsreds_lhap: â\88\80s,M1,M2. M1 â\86¦*[s] M2 â\86\92 is_head s â\86\92 M1 â\93\97â\86¦*[s] M2.
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
#a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/
qed.
-lemma lhap_inv_head: â\88\80s,M1,M2. M1 â\93\97â\87\80*[s] M2 → is_head s.
+lemma lhap_inv_head: â\88\80s,M1,M2. M1 â\93\97â\86¦*[s] M2 → is_head s.
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
#p #s #M1 #M #HM1 #_ #IHM2
lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/
qed-.
-lemma lhap_inv_lsreds: â\88\80s,M1,M2. M1 â\93\97â\87\80*[s] M2 â\86\92 M1 â\87\80*[s] M2.
+lemma lhap_inv_lsreds: â\88\80s,M1,M2. M1 â\93\97â\86¦*[s] M2 â\86\92 M1 â\86¦*[s] M2.
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
#p #s #M1 #M #HM1 #_ #IHM2
lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/
R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
*)
inductive lhap1: ptr → relation term ≝
-| hap1_beta: â\88\80B,A. lhap1 (â\97\8a) (@B.ð\9d\9b\8c.A) ([â¬\90B]A)
+| hap1_beta: â\88\80B,A. lhap1 (â\97\8a) (@B.ð\9d\9b\8c.A) ([â\86\99B]A)
| hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2)
.
interpretation "labelled 'hap' reduction"
'HAp M p N = (lhap1 p M N).
-notation "hvbox( M break â\93\97â\87\80 [ term 46 p ] break term 46 N )"
+notation "hvbox( M break â\93\97â\86¦ [ term 46 p ] break term 46 N )"
non associative with precedence 45
for @{ 'HAp $M $p $N }.
-lemma lhap1_inv_nil: â\88\80p,M,N. M â\93\97â\87\80[p] N → ◊ = p →
- â\88\83â\88\83B,A. @B.ð\9d\9b\8c.A = M & [â¬\90B]A = N.
+lemma lhap1_inv_nil: â\88\80p,M,N. M â\93\97â\86¦[p] N → ◊ = p →
+ â\88\83â\88\83B,A. @B.ð\9d\9b\8c.A = M & [â\86\99B]A = N.
#p #M #N * -p -M -N
[ #B #A #_ /2 width=4/
| #p #B #A1 #A2 #_ #H destruct
]
qed-.
-lemma lhap1_inv_cons: â\88\80p,M,N. M â\93\97â\87\80[p] N → ∀c,q. c::q = p →
- â\88\83â\88\83B,A1,A2. dx = c & A1 â\93\97â\87\80[q] A2 & @B.A1 = M & @B.A2 = N.
+lemma lhap1_inv_cons: â\88\80p,M,N. M â\93\97â\86¦[p] N → ∀c,q. c::q = p →
+ â\88\83â\88\83B,A1,A2. dx = c & A1 â\93\97â\86¦[q] A2 & @B.A1 = M & @B.A2 = N.
#p #M #N * -p -M -N
[ #B #A #c #q #H destruct
| #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/
#D2 #A #d >dsubst_dsubst_ge //
qed.
-lemma head_lsred_lhap1: â\88\80p. in_head p â\86\92 â\88\80M,N. M â\87\80[p] N â\86\92 M â\93\97â\87\80[p] N.
+lemma head_lsred_lhap1: â\88\80p. in_head p â\86\92 â\88\80M,N. M â\86¦[p] N â\86\92 M â\93\97â\86¦[p] N.
#p #H @(in_head_ind … H) -p
[ #M #N #H elim (lsred_inv_nil … H ?) -H //
| #p #_ #IHp #M #N #H
]
qed.
-lemma lhap1_inv_head: â\88\80p,M,N. M â\93\97â\87\80[p] N → in_head p.
+lemma lhap1_inv_head: â\88\80p,M,N. M â\93\97â\86¦[p] N → in_head p.
#p #M #N #H elim H -p -M -N // /2 width=1/
qed-.
-lemma lhap1_inv_lsred: â\88\80p,M,N. M â\93\97â\87\80[p] N â\86\92 M â\87\80[p] N.
+lemma lhap1_inv_lsred: â\88\80p,M,N. M â\93\97â\86¦[p] N â\86\92 M â\86¦[p] N.
#p #M #N #H elim H -p -M -N // /2 width=1/
qed-.
interpretation "labelled sequential computation"
'SeqRedStar M s N = (lsreds s M N).
-notation "hvbox( M break â\87\80* [ term 46 s ] break term 46 N )"
+notation "hvbox( M break â\86¦* [ term 46 s ] break term 46 N )"
non associative with precedence 45
for @{ 'SeqRedStar $M $s $N }.
-lemma lsreds_step_rc: â\88\80p,M1,M2. M1 â\87\80[p] M2 â\86\92 M1 â\87\80*[p::◊] M2.
+lemma lsreds_step_rc: â\88\80p,M1,M2. M1 â\86¦[p] M2 â\86\92 M1 â\86¦*[p::◊] M2.
/2 width=1/
qed.
-lemma lsreds_inv_nil: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → ◊ = s → M1 = M2.
+lemma lsreds_inv_nil: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → ◊ = s → M1 = M2.
/2 width=5 by lstar_inv_nil/
qed-.
-lemma lsreds_inv_cons: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → ∀q,r. q::r = s →
- â\88\83â\88\83M. M1 â\87\80[q] M & M â\87\80*[r] M2.
+lemma lsreds_inv_cons: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → ∀q,r. q::r = s →
+ â\88\83â\88\83M. M1 â\86¦[q] M & M â\86¦*[r] M2.
/2 width=3 by lstar_inv_cons/
qed-.
-lemma lsreds_inv_step_rc: â\88\80p,M1,M2. M1 â\87\80*[p::â\97\8a] M2 â\86\92 M1 â\87\80[p] M2.
+lemma lsreds_inv_step_rc: â\88\80p,M1,M2. M1 â\86¦*[p::â\97\8a] M2 â\86\92 M1 â\86¦[p] M2.
/2 width=1 by lstar_inv_step/
qed-.
-lemma lsreds_inv_pos: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → 0 < |s| →
- â\88\83â\88\83p,r,M. p::r = s & M1 â\87\80[p] M & M â\87\80*[r] M2.
+lemma lsreds_inv_pos: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → 0 < |s| →
+ â\88\83â\88\83p,r,M. p::r = s & M1 â\86¦[p] M & M â\86¦*[r] M2.
/2 width=1 by lstar_inv_pos/
qed-.
qed-.
(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
+lemma lsreds_fwd_mult: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
#p #s #M1 #M #HM1 #_ #IHM2
lapply (lsred_fwd_mult … HM1) -p #HM1
Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
*)
inductive lsred: ptr → relation term ≝
-| lsred_beta : â\88\80B,A. lsred (â\97\8a) (@B.ð\9d\9b\8c.A) ([â¬\90B]A)
+| lsred_beta : â\88\80B,A. lsred (â\97\8a) (@B.ð\9d\9b\8c.A) ([â\86\99B]A)
| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (sn::p) (𝛌.A1) (𝛌.A2)
| lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A)
| lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2)
'SeqRed M p N = (lsred p M N).
(* Note: we do not use → since it is reserved by CIC *)
-notation "hvbox( M break â\87\80 [ term 46 p ] break term 46 N )"
+notation "hvbox( M break â\86¦ [ term 46 p ] break term 46 N )"
non associative with precedence 45
for @{ 'SeqRed $M $p $N }.
-lemma lsred_inv_vref: â\88\80p,M,N. M â\87\80[p] N → ∀i. #i = M → ⊥.
+lemma lsred_inv_vref: â\88\80p,M,N. M â\86¦[p] N → ∀i. #i = M → ⊥.
#p #M #N * -p -M -N
[ #B #A #i #H destruct
| #p #A1 #A2 #_ #i #H destruct
]
qed-.
-lemma lsred_inv_nil: â\88\80p,M,N. M â\87\80[p] N → ◊ = p →
- â\88\83â\88\83B,A. @B. ð\9d\9b\8c.A = M & [â¬\90B] A = N.
+lemma lsred_inv_nil: â\88\80p,M,N. M â\86¦[p] N → ◊ = p →
+ â\88\83â\88\83B,A. @B. ð\9d\9b\8c.A = M & [â\86\99B] A = N.
#p #M #N * -p -M -N
[ #B #A #_ destruct /2 width=4/
| #p #A1 #A2 #_ #H destruct
]
qed-.
-lemma lsred_inv_sn: â\88\80p,M,N. M â\87\80[p] N → ∀q. sn::q = p →
- (â\88\83â\88\83A1,A2. A1 â\87\80[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨
- â\88\83â\88\83B1,B2,A. B1 â\87\80[q] B2 & @B1.A = M & @B2.A = N.
+lemma lsred_inv_sn: â\88\80p,M,N. M â\86¦[p] N → ∀q. sn::q = p →
+ (â\88\83â\88\83A1,A2. A1 â\86¦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨
+ â\88\83â\88\83B1,B2,A. B1 â\86¦[q] B2 & @B1.A = M & @B2.A = N.
#p #M #N * -p -M -N
[ #B #A #q #H destruct
| #p #A1 #A2 #HA12 #q #H destruct /3 width=5/
]
qed-.
-lemma lsred_inv_dx: â\88\80p,M,N. M â\87\80[p] N → ∀q. dx::q = p →
- â\88\83â\88\83B,A1,A2. A1 â\87\80[q] A2 & @B.A1 = M & @B.A2 = N.
+lemma lsred_inv_dx: â\88\80p,M,N. M â\86¦[p] N → ∀q. dx::q = p →
+ â\88\83â\88\83B,A1,A2. A1 â\86¦[q] A2 & @B.A1 = M & @B.A2 = N.
#p #M #N * -p -M -N
[ #B #A #q #H destruct
| #p #A1 #A2 #_ #q #H destruct
]
qed-.
-lemma lsred_fwd_mult: â\88\80p,M,N. M â\87\80[p] N → #{N} < #{M} * #{M}.
+lemma lsred_fwd_mult: â\88\80p,M,N. M â\86¦[p] N → #{N} < #{M} * #{M}.
#p #M #N #H elim H -p -M -N
[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) //
normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "lift.ma".
+
+(* LENGTH *******************************************************************)
+
+(* Note: this gives the number of abstractions and applications in M *)
+let rec length M on M ≝ match M with
+[ VRef i ⇒ 0
+| Abst A ⇒ length A + 1
+| Appl B A ⇒ (length B) + (length A) + 1
+].
+
+interpretation "term length"
+ 'card M = (length M).
+
+lemma length_lift: ∀h,M,d. |↑[d, h] M| = |M|.
+#h #M elim M -M normalize //
+qed.
(* RELOCATION ***************************************************************)
-(* Policy: depth (level) metavariables: d, e
- height metavariables : h, k
+(* Policy: level metavariables : d, e
+ height metavariables: h, k
*)
(* Note: indexes start at zero *)
let rec lift h d M on M ≝ match M with
#d #h #i #H elim (le_to_or_lt_eq … H) -H
normalize // /3 width=1/
qed.
-
+(*
lemma lift_vref_pred: ∀d,i. d < i → ↑[d, 1] #(i-1) = #i.
#d #i #Hdi >lift_vref_ge /2 width=1/
<plus_minus_m_m // /2 width=2/
qed.
-
+*)
lemma lift_id: ∀M,d. ↑[d, 0] M = M.
#M elim M -M
[ #i #d elim (lt_or_ge i d) /2 width=1/
#h #M elim M -M normalize //
qed.
-theorem mult_dsubst: â\88\80D,M,d. #{[d â¬\90 D] M} ≤ #{M} * #{D}.
+theorem mult_dsubst: â\88\80D,M,d. #{[d â\86\99 D] M} ≤ #{M} * #{D}.
#D #M elim M -M
[ #i #d elim (lt_or_eq_or_gt i d) #Hid
[ >(dsubst_vref_lt … Hid) normalize //
(* *)
(**************************************************************************)
-include "size.ma".
+include "length.ma".
include "labelled_sequential_reduction.ma".
(* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
| pred_vref: ∀i. pred (#i) (#i)
| pred_abst: ∀A1,A2. pred A1 A2 → pred (𝛌.A1) (𝛌.A2)
| pred_appl: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.A1) (@B2.A2)
-| pred_beta: â\88\80B1,B2,A1,A2. pred B1 B2 â\86\92 pred A1 A2 â\86\92 pred (@B1.ð\9d\9b\8c.A1) ([â¬\90B2]A2)
+| pred_beta: â\88\80B1,B2,A1,A2. pred B1 B2 â\86\92 pred A1 A2 â\86\92 pred (@B1.ð\9d\9b\8c.A1) ([â\86\99B2]A2)
.
interpretation "parallel reduction"
'ParRed M N = (pred M N).
-notation "hvbox( M ⥤ break term 46 N )"
+notation "hvbox( M â¤\87 break term 46 N )"
non associative with precedence 45
for @{ 'ParRed $M $N }.
#M elim M -M // /2 width=1/
qed.
-lemma pred_inv_vref: â\88\80M,N. M ⥤ N → ∀i. #i = M → #i = N.
+lemma pred_inv_vref: â\88\80M,N. M â¤\87 N → ∀i. #i = M → #i = N.
#M #N * -M -N //
[ #A1 #A2 #_ #i #H destruct
| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
]
qed-.
-lemma pred_inv_abst: â\88\80M,N. M ⥤ N → ∀A. 𝛌.A = M →
- â\88\83â\88\83C. A ⥤ C & 𝛌.C = N.
+lemma pred_inv_abst: â\88\80M,N. M â¤\87 N → ∀A. 𝛌.A = M →
+ â\88\83â\88\83C. A â¤\87 C & 𝛌.C = N.
#M #N * -M -N
[ #i #A0 #H destruct
| #A1 #A2 #HA12 #A0 #H destruct /2 width=3/
]
qed-.
-lemma pred_inv_appl: â\88\80M,N. M ⥤ N → ∀B,A. @B.A = M →
- (â\88\83â\88\83D,C. B ⥤ D & A ⥤ C & @D.C = N) ∨
- â\88\83â\88\83A0,D,C0. B ⥤ D & A0 ⥤ C0 & ð\9d\9b\8c.A0 = A & [â¬\90D]C0 = N.
+lemma pred_inv_appl: â\88\80M,N. M â¤\87 N → ∀B,A. @B.A = M →
+ (â\88\83â\88\83D,C. B â¤\87 D & A â¤\87 C & @D.C = N) ∨
+ â\88\83â\88\83A0,D,C0. B â¤\87 D & A0 â¤\87 C0 & ð\9d\9b\8c.A0 = A & [â\86\99D]C0 = N.
#M #N * -M -N
[ #i #B0 #A0 #H destruct
| #A1 #A2 #_ #B0 #A0 #H destruct
elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro â\80¦ ([â¬\90B2]A2)) /2 width=1/
+ @(ex2_intro â\80¦ ([â\86\99B2]A2)) /2 width=1/
]
qed-.
lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
(∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *)
- B ⥤ B1 â\86\92 B ⥤ B2 â\86\92 ð\9d\9b\8c.C ⥤ M1 â\86\92 C ⥤ C2 →
- â\88\83â\88\83M. @B1.M1 ⥤ M & [â¬\90B2]C2 ⥤ M.
+ B â¤\87 B1 â\86\92 B â¤\87 B2 â\86\92 ð\9d\9b\8c.C â¤\87 M1 â\86\92 C â¤\87 C2 →
+ â\88\83â\88\83M. @B1.M1 â¤\87 M & [â\86\99B2]C2 â¤\87 M.
#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
elim (IH B … HB1 … HB2) -HB1 -HB2 //
qed-.
theorem pred_conf: confluent … pred.
-#M @(f_ind … size … M) -M #n #IH * normalize
+#M @(f_ind … length … M) -M #n #IH * normalize
[ /2 width=3 by pred_conf1_vref/
| /3 width=4 by pred_conf1_abst/
| #B #A #H #M1 #H1 #M2 #H2 destruct
]
qed-.
-lemma lsred_pred: â\88\80p,M,N. M â\87\80[p] N â\86\92 M ⥤ N.
+lemma lsred_pred: â\88\80p,M,N. M â\86¦[p] N â\86\92 M â¤\87 N.
#p #M #N #H elim H -p -M -N /2 width=1/
qed.
T, U : arbitrary small type
c : pointer step
-d, e : variable reference depth
+d, e : variable reference level
h : relocation height
-i, j : de Bruijn index
+i, j : variable reference depth (de Bruijn index)
k : relocation height
l : arbitrary list
m, n : measures on terms
non associative with precedence 90
for @{'false}.
-(* relations *)
-
-definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
- ∀a1. R a0 a1 → ∀a2. R a0 a2 →
- ∃∃a. R a1 a & R a2 a.
-
-(* Note: confluent1 would be redundant if \Pi-reduction where enabled *)
-definition confluent: ∀A. predicate (relation A) ≝ λA,R.
- ∀a0. confluent1 … R a0.
-
(* arithmetics *)
lemma lt_refl_false: ∀n. n < n → ⊥.
--- /dev/null
+#!/bin/sh
+for MA in `find -name "*.ma"`; do
+ echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new
+ if diff ${MA} ${MA}.new > /dev/null;
+ then rm -f ${MA}.new;
+ else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA};
+ fi
+done
+
+unset MA
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "lift.ma".
-
-(* SIZE *********************************************************************)
-
-(* Note: this gives the number of abstractions and applications in M *)
-let rec size M on M ≝ match M with
-[ VRef i ⇒ 0
-| Abst A ⇒ size A + 1
-| Appl B A ⇒ (size B) + (size A) + 1
-].
-
-interpretation "term size"
- 'card M = (size M).
-
-lemma size_lift: ∀h,M,d. |↑[d, h] M| = |M|.
-#h #M elim M -M normalize //
-qed.
R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
*)
inductive st: relation term ≝
-| st_vref: â\88\80s,M,i. M â\93\97â\87\80*[s] #i → st M (#i)
-| st_abst: â\88\80s,M,A1,A2. M â\93\97â\87\80*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
-| st_appl: â\88\80s,M,B1,B2,A1,A2. M â\93\97â\87\80*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
+| st_vref: â\88\80s,M,i. M â\93\97â\86¦*[s] #i → st M (#i)
+| st_abst: â\88\80s,M,A1,A2. M â\93\97â\86¦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
+| st_appl: â\88\80s,M,B1,B2,A1,A2. M â\93\97â\86¦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
.
interpretation "'st' computation"
'Std M N = (st M N).
-notation "hvbox( M â\93¢â¥¤* break term 46 N )"
+notation "hvbox( M â\93¢â¤\87* break term 46 N )"
non associative with precedence 45
for @{ 'Std $M $N }.
-lemma st_inv_lref: â\88\80M,N. M â\93¢â¥¤* N → ∀j. #j = N →
- â\88\83s. M â\93\97â\87\80*[s] #j.
+lemma st_inv_lref: â\88\80M,N. M â\93¢â¤\87* N → ∀j. #j = N →
+ â\88\83s. M â\93\97â\86¦*[s] #j.
#M #N * -M -N
[ /2 width=2/
| #s #M #A1 #A2 #_ #_ #j #H destruct
]
qed-.
-lemma st_inv_abst: â\88\80M,N. M â\93¢â¥¤* N → ∀C2. 𝛌.C2 = N →
- â\88\83â\88\83s,C1. M â\93\97â\87\80*[s] ð\9d\9b\8c.C1 & C1 â\93¢â¥¤* C2.
+lemma st_inv_abst: â\88\80M,N. M â\93¢â¤\87* N → ∀C2. 𝛌.C2 = N →
+ â\88\83â\88\83s,C1. M â\93\97â\86¦*[s] ð\9d\9b\8c.C1 & C1 â\93¢â¤\87* C2.
#M #N * -M -N
[ #s #M #i #_ #C2 #H destruct
| #s #M #A1 #A2 #HM #A12 #C2 #H destruct /2 width=4/
]
qed-.
-lemma st_inv_appl: â\88\80M,N. M â\93¢â¥¤* N → ∀D2,C2. @D2.C2 = N →
- â\88\83â\88\83s,D1,C1. M â\93\97â\87\80*[s] @D1.C1 & D1 â\93¢â¥¤* D2 & C1 â\93¢â¥¤* C2.
+lemma st_inv_appl: â\88\80M,N. M â\93¢â¤\87* N → ∀D2,C2. @D2.C2 = N →
+ â\88\83â\88\83s,D1,C1. M â\93\97â\86¦*[s] @D1.C1 & D1 â\93¢â¤\87* D2 & C1 â\93¢â¤\87* C2.
#M #N * -M -N
[ #s #M #i #_ #D2 #C2 #H destruct
| #s #M #A1 #A2 #_ #_ #D2 #C2 #H destruct
#M elim M -M /2 width=2/ /2 width=4/ /2 width=6/
qed.
-lemma st_step_sn: â\88\80N1,N2. N1 â\93¢â¥¤* N2 â\86\92 â\88\80s,M. M â\93\97â\87\80*[s] N1 â\86\92 M â\93¢â¥¤* N2.
+lemma st_step_sn: â\88\80N1,N2. N1 â\93¢â¤\87* N2 â\86\92 â\88\80s,M. M â\93\97â\86¦*[s] N1 â\86\92 M â\93¢â¤\87* N2.
#N1 #N2 #H elim H -N1 -N2
[ #r #N #i #HN #s #M #HMN
lapply (lhap_trans … HMN … HN) -N /2 width=2/
]
qed-.
-lemma st_step_rc: â\88\80s,M1,M2. M1 â\93\97â\87\80*[s] M2 â\86\92 M1 â\93¢â¥¤* M2.
+lemma st_step_rc: â\88\80s,M1,M2. M1 â\93\97â\86¦*[s] M2 â\86\92 M1 â\93¢â¤\87* M2.
/3 width=4 by st_step_sn/
qed.
]
qed.
-lemma st_inv_lsreds_is_le: â\88\80M,N. M â\93¢â¥¤* N →
- â\88\83â\88\83r. M â\87\80*[r] N & is_le r.
+lemma st_inv_lsreds_is_le: â\88\80M,N. M â\93¢â¤\87* N →
+ â\88\83â\88\83r. M â\86¦*[r] N & is_le r.
#M #N #H elim H -M -N
[ #s #M #i #H
lapply (lhap_inv_lsreds … H)
]
qed-.
-lemma st_step_dx: â\88\80p,M,M2. M â\87\80[p] M2 â\86\92 â\88\80M1. M1 â\93¢â¥¤* M â\86\92 M1 â\93¢â¥¤* M2.
+lemma st_step_dx: â\88\80p,M,M2. M â\86¦[p] M2 â\86\92 â\88\80M1. M1 â\93¢â¤\87* M â\86\92 M1 â\93¢â¤\87* M2.
#p #M #M2 #H elim H -p -M -M2
[ #B #A #M1 #H
elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #HM1 #HB1 #H (**) (* simplify line *)
elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #HM #HA1 (**) (* simplify line *)
lapply (lhap_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1
- lapply (lhap_step_dx â\80¦ HM1 (â\97\8a) ([â¬\90B1]A1) ?) -HM1 // #HM1
+ lapply (lhap_step_dx â\80¦ HM1 (â\97\8a) ([â\86\99B1]A1) ?) -HM1 // #HM1
@(st_step_sn … HM1) /2 width=1/
| #p #A #A2 #_ #IHA2 #M1 #H
elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=4/ (**) (* simplify line *)
]
qed-.
-lemma st_lhap1_swap: â\88\80p,N1,N2. N1 â\93\97â\87\80[p] N2 â\86\92 â\88\80M1. M1 â\93¢â¥¤* N1 →
- â\88\83â\88\83q,M2. M1 â\93\97â\87\80[q] M2 & M2 â\93¢â¥¤* N2.
+lemma st_lhap1_swap: â\88\80p,N1,N2. N1 â\93\97â\86¦[p] N2 â\86\92 â\88\80M1. M1 â\93¢â¤\87* N1 →
+ â\88\83â\88\83q,M2. M1 â\93\97â\86¦[q] M2 & M2 â\93¢â¤\87* N2.
#p #N1 #N2 #H elim H -p -N1 -N2
[ #D #C #M1 #H
elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #D1 #N #HM1 #HD1 #H (**) (* simplify line *)
elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #C1 #HN #HC1 (**) (* simplify line *)
lapply (lhap_trans … HM1 … (dx:::r) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1
- lapply (lhap_step_dx â\80¦ HM1 (â\97\8a) ([â¬\90D1]C1) ?) -HM1 // #HM1
+ lapply (lhap_step_dx â\80¦ HM1 (â\97\8a) ([â\86\99D1]C1) ?) -HM1 // #HM1
elim (lhap_inv_pos … HM1 ?) -HM1
[2: >length_append normalize in ⊢ (??(??%)); // ]
#q #r #M #_ #HM1 #HM -s
]
qed-.
-lemma st_lsreds: â\88\80s,M1,M2. M1 â\87\80*[s] M2 â\86\92 M1 â\93¢â¥¤* M2.
+lemma st_lsreds: â\88\80s,M1,M2. M1 â\86¦*[s] M2 â\86\92 M1 â\93¢â¤\87* M2.
#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/
qed.
lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
qed-.
-theorem lsreds_standard: â\88\80s,M,N. M â\87\80*[s] N →
- â\88\83â\88\83r. M â\87\80*[r] N & is_le r.
+theorem lsreds_standard: â\88\80s,M,N. M â\86¦*[s] N →
+ â\88\83â\88\83r. M â\86¦*[r] N & is_le r.
#s #M #N #H
@st_inv_lsreds_is_le /2 width=2/
qed-.
-theorem lsreds_lhap1_swap: â\88\80s,M1,N1. M1 â\87\80*[s] N1 â\86\92 â\88\80p,N2. N1 â\93\97â\87\80[p] N2 →
- â\88\83â\88\83q,r,M2. M1 â\93\97â\87\80[q] M2 & M2 â\87\80*[r] N2 & is_le (q::r).
+theorem lsreds_lhap1_swap: â\88\80s,M1,N1. M1 â\86¦*[s] N1 â\86\92 â\88\80p,N2. N1 â\93\97â\86¦[p] N2 →
+ â\88\83â\88\83q,r,M2. M1 â\93\97â\86¦[q] M2 & M2 â\86¦*[r] N2 & is_le (q::r).
#s #M1 #N1 #HMN1 #p #N2 #HN12
lapply (st_lsreds … HMN1) -s #HMN1
elim (st_lhap1_swap … HN12 … HMN1) -p -N1 #q #M2 #HM12 #HMN2
(* TERM STRUCTURE ***********************************************************)
-(* Policy: term metavariables: A, B, C, D, M, N
- de Bruijn indexes : i, j
+(* Policy: term metavariables : A, B, C, D, M, N
+ depth metavariables: i, j
*)
inductive term: Type[0] ≝
-| VRef: nat → term (* variable reference by index *)
+| VRef: nat → term (* variable reference by depth *)
| Abst: term → term (* function formation *)
| Appl: term → term → term (* function application *)
.
notation "hvbox( @ term 46 C . break term 46 A )"
non associative with precedence 46
for @{ 'Application $C $A }.
-
+(*
definition appl_compatible_dx: predicate (relation term) ≝ λR.
∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2).
appl_compatible_dx (star … R).
#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/
qed.
+*)
lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
#A0 #P0 #P1 * /2 width=3/
-qed.
+qed-.
(* iff *)
definition iff :=
definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
+definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
+ ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & R a2 a.
+
+definition confluent: ∀A. predicate (relation A) ≝ λA,R.
+ ∀a0. confluent1 … R a0.
+
(* Reflexive closure ************)
definition RC: ∀A:Type[0]. relation A → relation A ≝
["#"; "⌘"; ];
["-"; "÷"; "⊢"; "⊩"; ];
["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];
- ["â\86\92"; "â\87\80"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
- ["â\87\92"; "⥤"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥰"; ] ;
+ ["â\86\92"; "â\86¦"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
+ ["â\87\92"; "â¤\87"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥰"; ] ;
["^"; "↑"; ] ;
["⇑"; "⇧"; "⬆"; ] ;
["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
["↔"; "⇔"; "⬄"; "⬌"; ] ;
["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
- ["_"; "â¬\90"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "â\86\93"; "â\86\99"; "⎽"; "⎼"; "⎻"; "⎺"; ];
["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
["("; "❨"; "❪"; "❲"; "（"; ];
[")"; "❩"; "❫"; "❳"; "）"; ];
projects / helm.git / commitdiff