+++ /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".
-
-(* DELIFTING SUBSTITUTION ***************************************************)
-
-(* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec dsubst D d M on M ≝ match M with
-[ VRef i ⇒ tri … i d (#i) (↑[i] D) (#(i-1))
-| Abst A ⇒ 𝛌. (dsubst D (d+1) A)
-| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A)
-].
-
-interpretation "delifting substitution"
- 'DSubst D d M = (dsubst D d M).
-
-(* Note: the notation with "/" does not work *)
-notation "hvbox( [ term 46 d ↙ break term 46 D ] break term 46 M )"
- non associative with precedence 46
- for @{ 'DSubst $D $d $M }.
-
-notation > "hvbox( [ ↙ term 46 D ] break term 46 M )"
- non associative with precedence 46
- for @{ 'DSubst $D 0 $M }.
-
-lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i.
-normalize /2 width=1/
-qed.
-
-lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
-normalize //
-qed.
-
-lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1).
-normalize /2 width=1/
-qed.
-
-theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
- [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ 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
- >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
- | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
- | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
- [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
- | lapply (ltn_to_ltO … Hid2) #Hi
- >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
- ]
- ]
-| normalize #A #IHA #d1 #d2 #Hd21
- lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd21
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
- [d2 ↙ 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
- >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
- | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
- >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
- >dsubst_vref_gt // /2 width=1/
- ]
-| normalize #A #IHA #d1 #d2 #Hd12 #Hd21
- >IHA -IHA // /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
- [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ 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
- [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
- lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
- >(lift_vref_lt … Hid1) -Hid1 /2 width=1/
- | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
- ]
- | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
- >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // <plus_minus_m_m //
- | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
- lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
- lapply (ltn_to_ltO … Hid2h) #Hi
- >(dsubst_vref_gt … Hid2h)
- >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1
- >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
- ]
-| normalize #A #IHA #d1 #d2 #Hd12
- elim (le_inv_plus_l … Hd12) #_ #Hhd2
- >IHA -IHA /2 width=1/ <plus_minus //
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
- [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ 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
- >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
- | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/
- | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
- [ lapply (ltn_to_ltO … Hid1) #Hi
- >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
- | destruct /2 width=1/
- | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
- >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/
- >dsubst_vref_gt // /2 width=1/
- ]
- ]
-| normalize #A #IHA #d1 #d2 #Hd12
- lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
- [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ 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.
- ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
-
-definition dsubstable: predicate (relation term) ≝ λR.
- ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ 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 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
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
-qed.
-
-lemma star_dsubstable: ∀R. reflexive ? R →
- dsubstable R → dsubstable (star … R).
-#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
-qed.
+++ /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 "pointer_list.ma".
-include "parallel_computation.ma".
-
-(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
-
-definition lsreds: ptrl → relation term ≝ lstar … lsred.
-
-interpretation "labelled sequential computation"
- 'SeqRedStar M s N = (lsreds s M N).
-
-notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
- non associative with precedence 45
- for @{ 'SeqRedStar $M $s $N }.
-
-lemma lsreds_refl: reflexive … (lsreds (◊)).
-//
-qed.
-
-lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
-/2 width=3/
-qed-.
-
-lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
-/2 width=1/
-qed.
-
-lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
-/2 width=5 by lstar_inv_nil/
-qed-.
-
-lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
- ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
-/2 width=3 by lstar_inv_cons/
-qed-.
-
-lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
-/2 width=1 by lstar_inv_step/
-qed-.
-
-lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
- ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
-/2 width=1 by lstar_inv_pos/
-qed-.
-
-lemma lsred_compatible_rc: ho_compatible_rc lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
-/3 width=1/
-qed.
-
-lemma lsreds_lift: ∀s. liftable (lsreds s).
-/2 width=1/
-qed.
-
-lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
-/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
-qed-.
-
-lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
-/2 width=1/
-qed.
-
-theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
-/3 width=7 by lstar_singlevalued, lsred_mono/
-qed-.
-
-theorem lsreds_trans: ltransitive … lsreds.
-/2 width=3 by lstar_ltransitive/
-qed-.
-
-lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
- @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
-#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
-@(lsreds_trans … (@B2.A1)) /2 width=1/
-qed.
-
-lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
- @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2.
-#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
-@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
-@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
-qed.
-
-(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[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
-@(transitive_le … IHM2) -M2
-/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
-qed-.
-
-theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
-#a #s #M1 #M #HM1 #_ #IHM2
-@(preds_step_sn … IHM2) -M2 /2 width=2/
-qed.
-
-lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
-#M1 #M2 #H elim H -M1 -M2 /2 width=2/
-[ #A1 #A2 #_ * /3 width=2/
-| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
-| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
-qed-.
-
-theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
-#M1 #M2 #H elim H -M2 /2 width=2/
-#M #M2 #_ #HM2 * #r #HM1
-elim (pred_lsreds … HM2) -HM2 #s #HM2
-lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
-qed-.
-
-theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
- ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
-#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
-lapply (lsreds_preds … HM01) -s1 #HM01
-lapply (lsreds_preds … HM02) -s2 #HM02
-elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
-elim (preds_lsreds … HM1) -HM1
-elim (preds_lsreds … HM2) -HM2 /2 width=5/
-qed-.
+++ /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 "pointer.ma".
-include "multiplicity.ma".
-
-(* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************)
-
-(* Note: the application "(A B)" is represented by "@B.A" following:
- F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
- Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
-*)
-inductive lsred: ptr → relation term ≝
-| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A)
-| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::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)
-.
-
-interpretation "labelled sequential reduction"
- 'SeqRed M p N = (lsred p M N).
-
-(* Note: we do not use → since it is reserved by CIC *)
-notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )"
- non associative with precedence 45
- for @{ 'SeqRed $M $p $N }.
-
-lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥.
-#p #M #N * -p -M -N
-[ #B #A #i #H destruct
-| #p #A1 #A2 #_ #i #H destruct
-| #p #B1 #B2 #A #_ #i #H destruct
-| #p #B #A1 #A2 #_ #i #H destruct
-]
-qed-.
-
-lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p →
- ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N.
-#p #M #N * -p -M -N
-[ #B #A #_ destruct /2 width=4/
-| #p #A1 #A2 #_ #H destruct
-| #p #B1 #B2 #A #_ #H destruct
-| #p #B #A1 #A2 #_ #H destruct
-]
-qed-.
-
-lemma lsred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p →
- ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/
-| #p #B1 #B2 #A #_ #q #H destruct
-| #p #B #A1 #A2 #_ #q #H destruct
-]
-qed-.
-
-lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p →
- ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N.
-#p #M #N * -p -M -N
-[ #B #A #q #H destruct
-| #p #A1 #A2 #_ #q #H destruct
-| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/
-| #p #B #A1 #A2 #_ #q #H destruct
-]
-qed-.
-
-lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p →
- ∃∃B,A1,A2. A1 ↦[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
-| #p #B1 #B2 #A #_ #q #H destruct
-| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
-]
-qed-.
-
-lemma lsred_fwd_mult: ∀p,M,N. M ↦[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 *)
-| //
-| #p #B #D #A #_ #IHBD
- @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p
-| #p #B #A #C #_ #IHAC
- @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p
-]
-@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ]
->distributive_times_plus normalize /2 width=1/
-qed-.
-
-lemma lsred_lift: ∀p. liftable (lsred p).
-#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#B #A #d <dsubst_lift_le //
-qed.
-
-lemma lsred_inv_lift: ∀p. deliftable_sn (lsred p).
-#p #h #N1 #N2 #H elim H -p -N1 -N2
-[ #D #C #d #M1 #H
- elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
- elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
-| #p #C1 #C2 #_ #IHC12 #d #M1 #H
- elim (lift_inv_abst … H) -H #A1 #HAC1 #H
- elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro … (𝛌.A2)) // /2 width=1/
-| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
- elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
- elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
- @(ex2_intro … (@B2.A)) // /2 width=1/
-| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
- elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
- elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro … (@B.A2)) // /2 width=1/
-]
-qed-.
-
-lemma lsred_dsubst: ∀p. dsubstable_dx (lsred p).
-#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
-#D2 #A #d >dsubst_dsubst_ge //
-qed.
-
-theorem lsred_mono: ∀p. singlevalued … (lsred p).
-#p #M #N1 #H elim H -p -M -N1
-[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H //
- #D #C #H #HN2 destruct //
-| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
- #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
-| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
- #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
-| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
- #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
-]
-qed-.
+++ /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.
+++ /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 "term.ma".
-
-(* RELOCATION ***************************************************************)
-
-(* 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
-[ VRef i ⇒ #(tri … i d i (i + h) (i + h))
-| Abst A ⇒ 𝛌. (lift h (d+1) A)
-| Appl B A ⇒ @(lift h d B). (lift h d A)
-].
-
-interpretation "relocation" 'Lift h d M = (lift h d M).
-
-notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )"
- non associative with precedence 46
- for @{ 'Lift $h $d $M }.
-
-notation > "hvbox( ↑ [ term 46 h ] break term 46 M )"
- non associative with precedence 46
- for @{ 'Lift $h 0 $M }.
-
-notation > "hvbox( ↑ term 46 M )"
- non associative with precedence 46
- for @{ 'Lift 1 0 $M }.
-
-lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
-normalize /3 width=1/
-qed.
-
-lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
-#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/
-| /3 width=1/
-| /3 width=1/
-]
-qed.
-
-lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
-#j #d #Hjd #h * normalize
-[ #i elim (lt_or_eq_or_gt i d) #Hid
- [ >(tri_lt ???? … Hid) -Hid -Hjd //
- | #H destruct >tri_eq in Hjd; #H
- elim (plus_lt_false … H)
- | >(tri_gt ???? … Hid)
- lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
- elim (plus_lt_false … H)
- ]
-| #A #H destruct
-| #B #A #H destruct
-]
-qed.
-
-lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j →
- d + h ≤ j ∧ M = #(j-h).
-#j #d #Hdj #h * normalize
-[ #i elim (lt_or_eq_or_gt i d) #Hid
- [ >(tri_lt ???? … Hid) #H destruct
- lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
- elim (lt_refl_false … H)
- | #H -Hdj destruct /2 width=1/
- | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
- ]
-| #A #H destruct
-| #B #A #H destruct
-]
-qed-.
-
-lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥.
-#j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M
-lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
-elim (lt_refl_false … H)
-qed-.
-
-lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j →
- ∀M. ↑[d, h] M = #j → M = #(j-h).
-#j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/
-qed.
-
-lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
- ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
-#C #d #h * normalize
-[ #i #H destruct
-| #A #H destruct /2 width=3/
-| #B #A #H destruct
-]
-qed-.
-
-lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
- ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
-#D #C #d #h * normalize
-[ #i #H destruct
-| #A #H destruct
-| #B #A #H destruct /2 width=5/
-]
-qed-.
-
-theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 →
- ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M.
-#h1 #h2 #M elim M -M
-[ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
- >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2)
- >lift_vref_lt // /2 width=1/
- | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
- [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2)
- >lift_vref_lt // -d2 /2 width=1/
- | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/
- >lift_vref_ge // /2 width=1/
- ]
- ]
-| normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA //
-]
-qed.
-
-theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
- ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M.
-#h1 #h2 #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
- >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
- | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
- >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/
- ]
-| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA //
-]
-qed.
-
-theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 →
- ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M.
-#h1 #h2 #M #d1 #d2 #Hd12
->(lift_lift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
-qed.
-
-(* Note: this is "∀h,d. injective … (lift h d)" *)
-theorem lift_inj: ∀h,M1,M2,d. ↑[d, h] M2 = ↑[d, h] M1 → M2 = M1.
-#h #M1 elim M1 -M1
-[ #i #M2 #d #H elim (lt_or_ge i d) #Hid
- [ >(lift_vref_lt … Hid) in H; #H
- >(lift_inv_vref_lt … Hid … H) -M2 -d -h //
- | >(lift_vref_ge … Hid) in H; #H
- >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/
- ]
-| normalize #A1 #IHA1 #M2 #d #H
- elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct
- >(IHA1 … HA12) -IHA1 -A2 //
-| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H
- elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
- >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 //
-]
-qed-.
-
-theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 →
- ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 →
- ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1.
-#h1 #h2 #M1 elim M1 -M1
-[ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
- [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
- >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/
- | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
- elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
- @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1
- >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
- ]
- | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
- lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
- elim (le_inv_plus_l … Hdh2i) #Hd2i #_
- >(lift_vref_ge … Hid1) #H -Hid1
- >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
- @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *)
- [ >lift_vref_ge // -Hd1i /3 width=1/
- | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/
- ]
- ]
-| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H
- elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct
- elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1
- @(ex2_intro … (𝛌.A)) normalize //
-| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H
- elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
- elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1
- elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1
- @(ex2_intro … (@B.A)) normalize //
-]
-qed-.
-
-theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
- ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2.
-#h1 #h2 #M1 elim M1 -M1
-[ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/
- | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
- >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/
- ]
-| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
- elim (lift_inv_abst … H) -H #A #HA12 #H destruct
- >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/
-| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
- elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct
- >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 //
-]
-qed-.
-
-theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 →
- ↑[d2, h2] M2 = ↑[d1, h1] M1 →
- ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1.
-#h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H
-elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
-lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
-elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/
-qed-.
-
-definition liftable: predicate (relation term) ≝ λR.
- ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
-
-definition deliftable_sn: predicate (relation term) ≝ λR.
- ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
- ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
-
-lemma star_liftable: ∀R. liftable R → liftable (star … R).
-#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
-qed.
-
-lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
-#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
-#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
-elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
-elim (HR … HN2 … HMN) -N /3 width=3/
-qed-.
-
-lemma lstar_liftable: ∀T,R. (∀t. liftable (R t)) →
- ∀l. liftable (lstar T … R l).
-#T #R #HR #l #h #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
-qed.
-
-lemma lstar_deliftable_sn: ∀T,R. (∀t. deliftable_sn (R t)) →
- ∀l. deliftable_sn (lstar T … R l).
-#T #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
-#t #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
-elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
-elim (IHN2 … HMN) -N /3 width=3/
-qed-.
+++ /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 "delifting_substitution.ma".
-
-(* MULTIPLICITY *************************************************************)
-
-(* Note: this gives the number of variable references in M *)
-let rec mult M on M ≝ match M with
-[ VRef i ⇒ 1
-| Abst A ⇒ mult A
-| Appl B A ⇒ (mult B) + (mult A)
-].
-
-interpretation "term multiplicity"
- 'Multiplicity M = (mult M).
-
-notation "hvbox( #{ term 46 M } )"
- non associative with precedence 90
- for @{ 'Multiplicity $M }.
-
-lemma mult_positive: ∀M. 0 < #{M}.
-#M elim M -M // /2 width=1/
-qed.
-
-lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}.
-#h #M elim M -M normalize //
-qed.
-
-theorem mult_dsubst: ∀D,M,d. #{[d ↙ 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 //
- | destruct >dsubst_vref_eq normalize //
- | >(dsubst_vref_gt … Hid) normalize //
- ]
-| normalize //
-| normalize #B #A #IHB #IHA #d
- >distributive_times_plus_r /2 width=1/
-]
-qed.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERIC NOTATION *********************************************************)
+
+notation "hvbox( # term 90 i )"
+ non associative with precedence 46
+ for @{ 'VariableReferenceByIndex $i }.
+
+notation "hvbox( { term 46 b } # break term 90 i )"
+ non associative with precedence 46
+ for @{ 'VariableReferenceByIndex $b $i }.
+
+notation "hvbox( 𝛌 . term 46 A )"
+ non associative with precedence 46
+ for @{ 'Abstraction $A }.
+
+notation "hvbox( { term 46 b } 𝛌 . break term 46 T)"
+ non associative with precedence 46
+ for @{ 'Abstraction $b $T }.
+
+notation "hvbox( @ term 46 C . break term 46 A )"
+ non associative with precedence 46
+ for @{ 'Application $C $A }.
+
+notation "hvbox( { term 46 b } @ break term 46 V . break term 46 T )"
+ non associative with precedence 46
+ for @{ 'Application $b $V $T }.
+
+notation "hvbox( ↑ [ term 46 d , break term 46 h ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'Lift $h $d $M }.
+
+notation > "hvbox( ↑ [ term 46 h ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'Lift $h 0 $M }.
+
+notation > "hvbox( ↑ term 46 M )"
+ non associative with precedence 46
+ for @{ 'Lift 1 0 $M }.
+
+(* Note: the notation with "/" does not work *)
+notation "hvbox( [ term 46 d ↙ break term 46 N ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'DSubst $N $d $M }.
+
+notation > "hvbox( [ ↙ term 46 N ] break term 46 M )"
+ non associative with precedence 46
+ for @{ 'DSubst $N 0 $M }.
+
\ No newline at end of file
+++ /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 "parallel_reduction.ma".
-
-(* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
-
-definition preds: relation term ≝ star … pred.
-
-interpretation "parallel computation"
- 'ParRedStar M N = (preds M N).
-
-notation "hvbox( M ⤇* break term 46 N )"
- non associative with precedence 45
- for @{ 'ParRedStar $M $N }.
-
-lemma preds_refl: reflexive … preds.
-//
-qed.
-
-lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
-/2 width=3/
-qed-.
-
-lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
-/2 width=3/
-qed-.
-
-lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
-/2 width=1/
-qed.
-
-lemma preds_compatible_abst: compatible_abst preds.
-/3 width=1/
-qed.
-
-lemma preds_compatible_sn: compatible_sn preds.
-/3 width=1/
-qed.
-
-lemma preds_compatible_dx: compatible_dx preds.
-/3 width=1/
-qed.
-
-lemma preds_compatible_appl: compatible_appl preds.
-/3 width=1/
-qed.
-
-lemma preds_lift: liftable preds.
-/2 width=1/
-qed.
-
-lemma preds_inv_lift: deliftable_sn preds.
-/3 width=3 by star_deliftable_sn, pred_inv_lift/
-qed-.
-
-lemma preds_dsubst_dx: dsubstable_dx preds.
-/2 width=1/
-qed.
-
-lemma preds_dsubst: dsubstable preds.
-/2 width=1/
-qed.
-
-theorem preds_trans: transitive … preds.
-/2 width=3 by trans_star/
-qed-.
-
-lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 →
- ∃∃M. M1 ⤇ M & M2 ⤇* M.
-/3 width=3 by star_strip, pred_conf/
-qed-.
-
-theorem preds_conf: confluent … preds.
-/3 width=3 by star_confluent, pred_conf/
-qed-.
+++ /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 "length.ma".
-include "labeled_sequential_reduction.ma".
-
-(* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
-
-(* Note: the application "(A B)" is represented by "@B.A"
- as for labelled sequential reduction
-*)
-inductive pred: relation term ≝
-| 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: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([↙B2]A2)
-.
-
-interpretation "parallel reduction"
- 'ParRed M N = (pred M N).
-
-notation "hvbox( M ⤇ break term 46 N )"
- non associative with precedence 45
- for @{ 'ParRed $M $N }.
-
-lemma pred_refl: reflexive … pred.
-#M elim M -M // /2 width=1/
-qed.
-
-lemma pred_inv_vref: ∀M,N. M ⤇ N → ∀i. #i = M → #i = N.
-#M #N * -M -N //
-[ #A1 #A2 #_ #i #H destruct
-| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
-| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
-]
-qed-.
-
-lemma pred_inv_abst: ∀M,N. M ⤇ N → ∀A. 𝛌.A = M →
- ∃∃C. A ⤇ C & 𝛌.C = N.
-#M #N * -M -N
-[ #i #A0 #H destruct
-| #A1 #A2 #HA12 #A0 #H destruct /2 width=3/
-| #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct
-| #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct
-]
-qed-.
-
-lemma pred_inv_appl: ∀M,N. M ⤇ N → ∀B,A. @B.A = M →
- (∃∃D,C. B ⤇ D & A ⤇ C & @D.C = N) ∨
- ∃∃A0,D,C0. B ⤇ D & A0 ⤇ C0 & 𝛌.A0 = A & [↙D]C0 = N.
-#M #N * -M -N
-[ #i #B0 #A0 #H destruct
-| #A1 #A2 #_ #B0 #A0 #H destruct
-| #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=5/
-| #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=7/
-]
-qed-.
-
-lemma pred_lift: liftable pred.
-#h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/
-#B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d <dsubst_lift_le // /2 width=1/
-qed.
-
-lemma pred_inv_lift: deliftable_sn pred.
-#h #N1 #N2 #H elim H -N1 -N2 /2 width=3/
-[ #C1 #C2 #_ #IHC12 #d #M1 #H
- elim (lift_inv_abst … H) -H #A1 #HAC1 #H
- elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro … (𝛌.A2)) // /2 width=1/
-| #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
- elim (lift_inv_appl … H) -H #B1 #A1 #HBD1 #HAC1 #H
- elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
- elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro … (@B2.A2)) // /2 width=1/
-| #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
- elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
- 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 … ([↙B2]A2)) /2 width=1/
-]
-qed-.
-
-lemma pred_dsubst: dsubstable pred.
-#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
-[ #i #d elim (lt_or_eq_or_gt i d) #Hid
- [ >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
- | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/
- | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
- ]
-| normalize /2 width=1/
-| normalize /2 width=1/
-| normalize #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d
- >dsubst_dsubst_ge // /2 width=1/
-]
-qed.
-
-lemma pred_conf1_vref: ∀i. confluent1 … pred (#i).
-#i #M1 #H1 #M2 #H2
-<(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *)
-<(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *)
-/2 width=3/
-qed-.
-
-lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
-#A #IH #M1 #H1 #M2 #H2
-elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
-elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
-elim (IH … HA1 … HA2) -A /3 width=3/
-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 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 →
- ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ 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 //
-elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
-qed-.
-
-theorem pred_conf: confluent … pred.
-#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
- elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
- elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *)
- [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
- elim (IH A … HA1 … HA2) -HA1 -HA2 //
- elim (IH B … HB1 … HB2) // -A -B /3 width=5/
- | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct
- @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *)
- | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
- @ex2_commute @(pred_conf1_appl_beta … IH) //
- | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
- elim (IH B … HB1 … HB2) -HB1 -HB2 //
- elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
- ]
-]
-qed-.
-
-lemma lsred_pred: ∀p,M,N. M ↦[p] N → M ⤇ N.
-#p #M #N #H elim H -p -M -N /2 width=1/
-qed.
+++ /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 "term.ma".
-
-(* POINTER ******************************************************************)
-
-(* Policy: pointer step metavariables: c *)
-(* Note: this is a step of a path in the tree representation of a term:
- rc (rectus) : proceed on the argument of an abstraction
- sn (sinister): proceed on the left argument of an application
- dx (dexter) : proceed on the right argument of an application
-*)
-inductive ptr_step: Type[0] ≝
-| rc: ptr_step
-| sn: ptr_step
-| dx: ptr_step
-.
-
-definition is_dx: predicate ptr_step ≝ λc. dx = c.
-
-(* Policy: pointer metavariables: p, q *)
-(* Note: this is a path in the tree representation of a term, heading to a redex *)
-definition ptr: Type[0] ≝ list ptr_step.
-
-(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
-definition in_whd: predicate ptr ≝ All … is_dx.
-
-lemma in_whd_ind: ∀R:predicate ptr. R (◊) →
- (∀p. in_whd p → R p → R (dx::p)) →
- ∀p. in_whd p → R p.
-#R #H #IH #p elim p -p // -H *
-#p #IHp * #H1 #H2 destruct /3 width=1/
-qed-.
-
-definition compatible_rc: predicate (ptr→relation term) ≝ λR.
- ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
-
-definition compatible_sn: predicate (ptr→relation term) ≝ λR.
- ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
-
-definition compatible_dx: predicate (ptr→relation term) ≝ λR.
- ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).
+++ /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 "pointer.ma".
-
-(* POINTER LIST *************************************************************)
-
-(* Policy: pointer list metavariables: r, s *)
-definition ptrl: Type[0] ≝ list ptr.
-
-(* Note: a "whd" computation contracts just redexes in the whd *)
-definition is_whd: predicate ptrl ≝ All … in_whd.
-
-lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
-#s elim s -s //
-#p #s #IHs * /3 width=1/
-qed.
-
-lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
-#r elim r -r //
-#q #r #IHr * /3 width=1/
-qed.
-
-definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR.
- ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
-
-definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR.
- ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
-
-definition ho_compatible_dx: predicate (ptrl→relation term) ≝ λR.
- ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
-
-lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
-#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
-
-lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
-#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
-qed.
-
-lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
-#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
+++ /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 "pointer_list.ma".
-include "pointer_order.ma".
-
-(* STANDARD POINTER LIST ****************************************************)
-
-(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
-definition is_standard: predicate ptrl ≝ Allr … ple.
-
-lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s).
-#c #s elim s -s // #p * //
-#q #s #IHs * /3 width=1/
-qed.
-
-lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s).
-#p #s elim s -s // #q1 * /2 width=1/
-#q2 #s #IHs * /4 width=1/
-qed.
-
-lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s).
-#r elim r -r /3 width=1/ #p * /2 width=1/
-#q #r #IHr * /3 width=1/
-qed.
-
-theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
-#s elim s -s // #p * //
-#q #s #IHs * /3 width=1/
-qed.
-
-lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
-#p #Hp * // /3 width=1/
-qed.
-
-theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
-#r elim r -r // #p *
-[ #_ * /2 width=1/
-| #q #r #IHr * /3 width=1/
-]
-qed.
+++ /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 "pointer.ma".
-
-(* POINTER ORDER ************************************************************)
-
-(* Note: precedence relation on redex pointers: p ≺ q
- to serve as base for the order relations: p < q and p ≤ q *)
-inductive pprec: relation ptr ≝
-| pprec_nil : ∀c,q. pprec (◊) (c::q)
-| ppprc_rc : ∀p,q. pprec (dx::p) (rc::q)
-| ppprc_sn : ∀p,q. pprec (rc::p) (sn::q)
-| pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q)
-| pprec_skip: pprec (dx::◊) ◊
-.
-
-interpretation "'precedes' on pointers"
- 'prec p q = (pprec p q).
-
-(* Note: this should go to core_notation *)
-notation "hvbox(a break ≺ b)"
- non associative with precedence 45
- for @{ 'prec $a $b }.
-
-lemma pprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
-#p #q #H elim H -p -q // /2 width=1/
-[ #p #q * #H destruct
-| #p #q * #H destruct
-| #c #p #q #_ #IHpq * #H destruct /3 width=1/
-]
-qed-.
-
-(* Note: this is p < q *)
-definition plt: relation ptr ≝ TC … pprec.
-
-interpretation "'less than' on redex pointers"
- 'lt p q = (plt p q).
-
-lemma plt_step_rc: ∀p,q. p ≺ q → p < q.
-/2 width=1/
-qed.
-
-lemma plt_nil: ∀c,p. ◊ < c::p.
-/2 width=1/
-qed.
-
-lemma plt_skip: dx::◊ < ◊.
-/2 width=1/
-qed.
-
-lemma plt_comp: ∀c,p,q. p < q → c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
-qed.
-
-theorem plt_trans: transitive … plt.
-/2 width=3/
-qed-.
-
-lemma plt_refl: ∀p. p < p.
-#p elim p -p /2 width=1/
-@(plt_trans … (dx::◊)) //
-qed.
-
-(* Note: this is p ≤ q *)
-definition ple: relation ptr ≝ star … pprec.
-
-interpretation "'less or equal to' on redex pointers"
- 'leq p q = (ple p q).
-
-lemma ple_step_rc: ∀p,q. p ≺ q → p ≤ q.
-/2 width=1/
-qed.
-
-lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2.
-/2 width=3/
-qed-.
-
-lemma ple_rc: ∀p,q. dx::p ≤ rc::q.
-/2 width=1/
-qed.
-
-lemma ple_sn: ∀p,q. rc::p ≤ sn::q.
-/2 width=1/
-qed.
-
-lemma ple_skip: dx::◊ ≤ ◊.
-/2 width=1/
-qed.
-
-lemma ple_nil: ∀p. ◊ ≤ p.
-* // /2 width=1/
-qed.
-
-lemma ple_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2).
-#p1 #p2 #H elim H -p2 // /3 width=3/
-qed.
-
-lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊.
-#p #H @(star_ind_l ??????? H) -p //
-#p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/
-qed.
-
-theorem ple_trans: transitive … ple.
-/2 width=3/
-qed-.
-
-lemma ple_cons: ∀p,q. dx::p ≤ sn::q.
-#p #q
-@(ple_trans … (rc::q)) /2 width=1/
-qed.
-
-lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1.
-#p1 elim p1 -p1
-[ * /2 width=1/
-| #c1 #p1 #IHp1 * /2 width=1/
- * #p2 cases c1 -c1 /2 width=1/
- elim (IHp1 p2) -IHp1 /3 width=1/
-]
-qed-.
-
-lemma in_whd_ple_nil: ∀p. in_whd p → p ≤ ◊.
-#p #H @(in_whd_ind … H) -p // /2 width=1/
-qed.
-
-theorem in_whd_ple: ∀p. in_whd p → ∀q. p ≤ q.
-#p #H @(in_whd_ind … H) -p //
-#p #_ #IHp * /3 width=1/ * #q /2 width=1/
-qed.
-
-lemma ple_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p.
-#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/
-qed-.
-
-lemma ple_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p.
-/2 width=1 by ple_nil_inv_in_whd/
-qed-.
+++ /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 "pointer_list.ma".
-
-(* POINTER TREE *************************************************************)
-
-(* Policy: pointer tree metavariables: P, Q *)
-(* Note: this is a binary tree on pointer sequences *)
-inductive ptrt: Type[0] ≝
-| tnil : ptrt
-| tcons: ptrl → ptrt → ptrt → ptrt
-.
-
-let rec length (P:ptrt) on P ≝ match P with
-[ tnil ⇒ 0
-| tcons s Q1 Q2 ⇒ length Q2 + length Q1 + |s|
-].
-
-interpretation "pointer tree length" 'card P = (length P).
NAMING CONVENTIONS FOR METAVARIABLES
A, B, C, D: term
+F,G : subset of subterms
H : transient premise
IH : inductive premise
M, N : term
P, Q : pointer tree
R : arbitrary relation
-T, U : arbitrary small type
+S : arbitrary small type
+T, U, V, W: subset of subterms
+a : arbitrary element
+b : boolean mark
c : pointer step
d, e : variable reference level
h : relocation height
m, n : measures on terms
p, q : pointer
r, s : pointer sequence
-t, u : arbitrary element
+
+++ /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 "labeled_sequential_computation.ma".
-include "pointer_list_standard.ma".
-
-(* KASHIMA'S "ST" COMPUTATION ***********************************************)
-
-(* Note: this is the "standard" computation of:
- R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
-*)
-inductive st: relation term ≝
-| st_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → st M (#i)
-| st_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
-| st_appl: ∀s,M,B1,B2,A1,A2. is_whd s → M ↦*[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 ⓢ⤇* break term 46 N )"
- non associative with precedence 45
- for @{ 'Std $M $N }.
-
-lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N →
- ∃∃s. is_whd s & M ↦*[s] #j.
-#M #N * -M -N
-[ /2 width=3/
-| #s #M #A1 #A2 #_ #_ #_ #j #H destruct
-| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct
-]
-qed-.
-
-lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N →
- ∃∃s,C1. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2.
-#M #N * -M -N
-[ #s #M #i #_ #_ #C2 #H destruct
-| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/
-| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct
-]
-qed-.
-
-lemma st_inv_appl: ∀M,N. M ⓢ⤇* N → ∀D2,C2. @D2.C2 = N →
- ∃∃s,D1,C1. is_whd s & M ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2.
-#M #N * -M -N
-[ #s #M #i #_ #_ #D2 #C2 #H destruct
-| #s #M #A1 #A2 #_ #_ #_ #D2 #C2 #H destruct
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/
-]
-qed-.
-
-lemma st_refl: reflexive … st.
-#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/
-qed.
-
-lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ⤇* N2.
-#N1 #N2 #H elim H -N1 -N2
-[ #r #N #i #Hr #HN #s #M #Hs #HMN
- lapply (lsreds_trans … HMN … HN) -N /3 width=3/
-| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN
- lapply (lsreds_trans … HMN … HN) -N /3 width=7/
-| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN
- lapply (lsreds_trans … HMN … HN) -N /3 width=9/
-]
-qed-.
-
-lemma st_step_rc: ∀s,M1,M2. is_whd s → M1 ↦*[s] M2 → M1 ⓢ⤇* M2.
-/3 width=5 by st_step_sn/
-qed.
-
-lemma st_lift: liftable st.
-#h #M1 #M2 #H elim H -M1 -M2
-[ /3 width=3/
-| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
- @(st_abst … Hs) [2: @(lsreds_lift … HM) | skip ] -M // (**) (* auto fails here *)
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
- @(st_appl … Hs) [3: @(lsreds_lift … HM) |1,2: skip ] -M // (**) (* auto fails here *)
-]
-qed.
-
-lemma st_inv_lift: deliftable_sn st.
-#h #N1 #N2 #H elim H -N1 -N2
-[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1
- elim (lsreds_inv_lift … HN1 … HMN1) -N1 /3 width=3/
-| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1
- elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2
- elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct
- elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
- @(ex2_intro … (𝛌.A2)) // /2 width=5/
-| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1
- elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2
- elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct
- elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *)
- elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
- @(ex2_intro … (@B2.A2)) // /2 width=7/
-]
-qed-.
-
-lemma st_dsubst: dsubstable st.
-#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
-[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid
- [ lapply (lsreds_dsubst … N1 … HM d) -HM
- >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) /2 width=3/
- | destruct >dsubst_vref_eq
- @(st_step_sn (↑[0,i]N1) … s) /2 width=1/
- | lapply (lsreds_dsubst … N1 … HM d) -HM
- >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/
- ]
-| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
- lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=5/ (**) (* auto needs some help here *)
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
- lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=7/ (**) (* auto needs some help here *)
-]
-qed.
-
-lemma st_step_dx: ∀p,M,M2. M ↦[p] M2 → ∀M1. M1 ⓢ⤇* M → M1 ⓢ⤇* 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 #Hs #HM1 #HB1 #H (**) (* simplify line *)
- elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *)
- lapply (lsreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1
- lapply (lsreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1
- @(st_step_sn … HM1) /2 width=1/ /4 width=1/
-| #p #A #A2 #_ #IHA2 #M1 #H
- elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *)
-| #p #B #B2 #A #_ #IHB2 #M1 #H
- elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
-| #p #B #A #A2 #_ #IHA2 #M1 #H
- elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
-]
-qed-.
-
-lemma st_lsreds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ⤇* M2.
-#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/
-qed.
-
-lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N →
- ∃∃r. M ↦*[r] N & is_standard r.
-#M #N #H elim H -M -N
-[ #s #M #i #Hs #HM
- lapply (is_whd_is_standard … Hs) -Hs /2 width=3/
-| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr
- lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
- @(ex2_intro … HM) -M -A2 /3 width=1/
-| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
- lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
- lapply (lsreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM
- @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/
-]
-qed-.
-
-theorem st_trans: transitive … st.
-#M1 #M #M2 #HM1 #HM2
-elim (st_inv_lsreds_is_standard … HM1) -HM1 #s1 #HM1 #_
-elim (st_inv_lsreds_is_standard … HM2) -HM2 #s2 #HM2 #_
-lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
-qed-.
-
-theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_standard r.
-#s #M #N #H
-@st_inv_lsreds_is_standard /2 width=2/
-qed-.
-
-(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural)
- in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative)
-*)
-lemma st_lsred_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 →
- ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ⤇* N2.
-#p #H @(in_whd_ind … H) -p
-[ #N1 #N2 #H1 #M1 #H2
- elim (lsred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2
- elim (st_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H
- elim (st_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *)
- lapply (lsreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1
- lapply (lsreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1
- elim (lsreds_inv_pos … HM1 ?) -HM1
- [2: >length_append normalize in ⊢ (??(??%)); // ]
- #q #r #M #Hq #HM1 #HM
- lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
- @(ex3_2_intro … HM1) -M1 // -q
- @(st_step_sn … HM) /2 width=1/
-| #p #_ #IHp #N1 #N2 #H1 #M1 #H2
- elim (lsred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *)
- elim (st_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1
- elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12
- lapply (lsreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1
- elim (lsreds_inv_pos … HM1 ?) -HM1
- [2: >length_append normalize in ⊢ (??(??%)); // ]
- #q #r #M #Hq #HM1 #HM
- lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
- @(ex3_2_intro … HM1) -M1 // -q /2 width=7/
-]
-qed-.
-
-theorem lsreds_lsred_swap: ∀s,M1,N1. M1 ↦*[s] N1 →
- ∀p,N2. in_whd p → N1 ↦[p] N2 →
- ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 &
- is_standard (q::r).
-#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12
-lapply (st_lsreds … HMN1) -s #HMN1
-elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2
-elim (st_inv_lsreds_is_standard … HMN2) -HMN2 /3 width=8/
-qed-.
--- /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 "subterms/subterms.ma".
+
+(* RELOCATION FOR SUBTERMS **************************************************)
+
+let rec slift h d E on E ≝ match E with
+[ SVRef b i ⇒ {b}#(tri … i d i (i + h) (i + h))
+| SAbst b T ⇒ {b}𝛌.(slift h (d+1) T)
+| SAppl b V T ⇒ {b}@(slift h d V).(slift h d T)
+].
+
+interpretation "relocation for subterms" 'Lift h d E = (slift h d E).
+
+lemma slift_vref_lt: ∀b,d,h,i. i < d → ↑[d, h] {b}#i = {b}#i.
+normalize /3 width=1/
+qed.
+
+lemma slift_vref_ge: ∀b,d,h,i. d ≤ i → ↑[d, h] {b}#i = {b}#(i+h).
+#b #d #h #i #H elim (le_to_or_lt_eq … H) -H
+normalize // /3 width=1/
+qed.
+
+lemma slift_id: ∀E,d. ↑[d, 0] E = E.
+#E elim E -E
+[ #b #i #d elim (lt_or_ge i d) /2 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j.
+#b0 #j #d #Hjd #h * normalize
+[ #b #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) -Hid -Hjd //
+ | #H destruct >tri_eq in Hjd; #H
+ elim (plus_lt_false … H)
+ | >(tri_gt ???? … Hid)
+ lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
+ elim (plus_lt_false … H)
+ ]
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed.
+
+lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
+ d + h ≤ j ∧ E = {b0}#(j-h).
+#b0 #j #d #Hdj #h * normalize
+[ #b #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) #H destruct
+ lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
+ elim (lt_refl_false … H)
+ | #H -Hdj destruct /2 width=1/
+ | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
+ ]
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥.
+#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
+lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
+elim (lt_refl_false … H)
+qed-.
+
+lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j →
+ ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h).
+#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
+qed.
+
+lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U →
+ ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T.
+#b0 #U #d #h * normalize
+[ #b #i #H destruct
+| #b #T #H destruct /2 width=3/
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
+ ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
+#b0 #W #U #d #h * normalize
+[ #b #i #H destruct
+| #b #T #H destruct
+| #b #V #T #H destruct /2 width=5/
+]
+qed-.
+
+theorem slift_slift_le: ∀h1,h2,E,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] ↑[d1, h1] E = ↑[d1 + h2, h1] ↑[d2, h2] E.
+#h1 #h2 #E elim E -E
+[ #b #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid2)
+ >slift_vref_lt // /2 width=1/
+ | >(slift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
+ [ >(slift_vref_lt … Hid1) >(slift_vref_ge … Hid2)
+ >slift_vref_lt // -d2 /2 width=1/
+ | >(slift_vref_ge … Hid1) >slift_vref_ge /2 width=1/
+ >slift_vref_ge // /2 width=1/
+ ]
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd21 >IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 >IHV >IHT //
+]
+qed.
+
+theorem slift_slift_be: ∀h1,h2,E,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1 + h2] E.
+#h1 #h2 #E elim E -E
+[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
+ >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) /2 width=1/
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 >IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 >IHV >IHT //
+]
+qed.
+
+theorem slift_slift_ge: ∀h1,h2,E,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1] ↑[d2 - h1, h2] E.
+#h1 #h2 #E #d1 #d2 #Hd12
+>(slift_slift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
+qed.
+
+(* Note: this is "∀h,d. injective … (slift h d)" *)
+theorem slift_inj: ∀h,E1,E2,d. ↑[d, h] E2 = ↑[d, h] E1 → E2 = E1.
+#h #E1 elim E1 -E1
+[ #b #i #E2 #d #H elim (lt_or_ge i d) #Hid
+ [ >(slift_vref_lt … Hid) in H; #H
+ >(slift_inv_vref_lt … Hid … H) -E2 -d -h //
+ | >(slift_vref_ge … Hid) in H; #H
+ >(slift_inv_vref_ge_plus … H) -E2 // /2 width=1/
+ ]
+| normalize #b #T1 #IHT1 #E2 #d #H
+ elim (slift_inv_abst … H) -H #T2 #HT12 #H destruct
+ >(IHT1 … HT12) -IHT1 -T2 //
+| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d #H
+ elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ >(IHV1 … HV12) -IHV1 -V2 >(IHT1 … HT12) -IHT1 -T2 //
+]
+qed-.
+
+theorem slift_inv_slift_le: ∀h1,h2,E1,E2,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] E2 = ↑[d1 + h2, h1] E1 →
+ ∃∃E. ↑[d1, h1] E = E2 & ↑[d2, h2] E = E1.
+#h1 #h2 #E1 elim E1 -E1
+[ #b #i #E2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
+ [ >(slift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
+ >(slift_inv_vref_lt … Hid2 … H) -E2 /3 width=3/
+ | elim (slift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
+ elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
+ @(ex2_intro … ({b}#(i-h2))) [ /4 width=1/ ] -Hid1
+ >slift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
+ ]
+ | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
+ lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
+ elim (le_inv_plus_l … Hdh2i) #Hd2i #_
+ >(slift_vref_ge … Hid1) #H -Hid1
+ >(slift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
+ @(ex2_intro … ({b}#(i-h2))) (**) (* auto: needs some help here *)
+ [ >slift_vref_ge // -Hd1i /3 width=1/
+ | >slift_vref_ge // -Hd2i -Hd1i /3 width=1/
+ ]
+ ]
+| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd21 #H
+ elim (slift_inv_abst … H) -H >plus_plus_comm_23 #T2 #HT12 #H destruct
+ elim (IHT1 … HT12) -IHT1 -HT12 /2 width=1/ -Hd21 #T #HT2 #HT1
+ @(ex2_intro … ({b}𝛌.T)) normalize //
+| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd21 #H
+ elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IHV1 … HV12) -IHV1 -HV12 // #V #HV2 #HV1
+ elim (IHT1 … HT12) -IHT1 -HT12 // -Hd21 #T #HT2 #HT1
+ @(ex2_intro … ({b}@V.T)) normalize //
+]
+qed-.
+
+theorem slift_inv_slift_be: ∀h1,h2,E1,E2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] E2 = ↑[d1, h1 + h2] E1 → ↑[d1, h1] E1 = E2.
+#h1 #h2 #E1 elim E1 -E1
+[ #b #i #E2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(slift_vref_lt … Hid1) #H >(slift_inv_vref_lt … Hid2 … H) -h2 -E2 -d2 /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(slift_vref_ge … Hid1) #H >(slift_inv_vref_ge_plus … H) -E2 /2 width=1/
+ ]
+| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (slift_inv_abst … H) -H #T #HT12 #H destruct
+ >(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
+| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (slift_inv_appl … H) -H #V #T #HV12 #HT12 #H destruct
+ >(IHV1 … HV12) -IHV1 -HV12 // >(IHT1 … HT12) -IHT1 -HT12 //
+]
+qed-.
+
+theorem slift_inv_slift_ge: ∀h1,h2,E1,E2,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] E2 = ↑[d1, h1] E1 →
+ ∃∃E. ↑[d1, h1] E = E2 & ↑[d2 - h1, h2] E = E1.
+#h1 #h2 #E1 #E2 #d1 #d2 #Hd12 #H
+elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
+lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
+elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/
+qed-.
+(*
+definition liftable: predicate (relation term) ≝ λR.
+ ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
+
+definition deliftable_sn: predicate (relation term) ≝ λR.
+ ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
+ ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
+
+lemma star_liftable: ∀R. liftable R → liftable (star … R).
+#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
+qed.
+
+lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
+#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
+#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
+elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
+elim (HR … HN2 … HMN) -N /3 width=3/
+qed-.
+
+lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
+ ∀l. liftable (lstar S … R l).
+#S #R #HR #l #h #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+qed.
+
+lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
+ ∀l. deliftable_sn (lstar S … R l).
+#S #R #HR #l #h #N1 #N2 #H
+@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
+#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
+elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
+elim (IHN2 … HMN) -N /3 width=3/
+qed-.
+*)
--- /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 "preamble.ma".
+include "notation.ma".
+
+(* SUBSETS OF SUBTERMS ******************************************************)
+
+(* Policy: boolean marks metavariables: b
+ subterms metavariables: F,G,T,U,V,W
+*)
+(* Note: each subterm is marked with true if it belongs to the subset *)
+inductive subterms: Type[0] ≝
+| SVRef: bool → nat → subterms
+| SAbst: bool → subterms → subterms
+| SAppl: bool → subterms → subterms → subterms
+.
+
+interpretation "subterms construction (variable reference by index)"
+ 'VariableReferenceByIndex b i = (SVRef b i).
+
+interpretation "subterms construction (abstraction)"
+ 'Abstraction b T = (SAbst b T).
+
+interpretation "subterms construction (application)"
+ 'Application b V T = (SAppl b V T).
+
+(*
+definition compatible_abst: predicate (relation term) ≝ λR.
+ ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (relation term) ≝ λR.
+ ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (relation term) ≝ λR.
+ ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2).
+
+definition compatible_appl: predicate (relation term) ≝ λR.
+ ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 →
+ R (@B1.A1) (@B2.A2).
+
+lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R).
+#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/
+qed.
+
+lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R).
+#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/
+qed.
+
+lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R).
+#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/
+qed.
+
+lemma star_compatible_appl: ∀R. reflexive ? R →
+ compatible_appl R → compatible_appl (star … R).
+#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/
+qed.
+*)
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* Initial invocation: - Patience on us to gain peace and perfection! - *)
-
-include "preamble.ma".
-
-(* TERM STRUCTURE ***********************************************************)
-
-(* Policy: term metavariables : A, B, C, D, M, N
- depth metavariables: i, j
-*)
-inductive term: Type[0] ≝
-| VRef: nat → term (* variable reference by depth *)
-| Abst: term → term (* function formation *)
-| Appl: term → term → term (* function application *)
-.
-
-interpretation "term construction (variable reference by index)"
- 'VariableReferenceByIndex i = (VRef i).
-
-interpretation "term construction (abstraction)"
- 'Abstraction A = (Abst A).
-
-interpretation "term construction (application)"
- 'Application C A = (Appl C A).
-
-notation "hvbox( # term 90 i )"
- non associative with precedence 90
- for @{ 'VariableReferenceByIndex $i }.
-
-notation "hvbox( 𝛌 . term 46 A )"
- non associative with precedence 46
- for @{ 'Abstraction $A }.
-
-notation "hvbox( @ term 46 C . break term 46 A )"
- non associative with precedence 46
- for @{ 'Application $C $A }.
-
-definition compatible_abst: predicate (relation term) ≝ λR.
- ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2).
-
-definition compatible_sn: predicate (relation term) ≝ λR.
- ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A).
-
-definition compatible_dx: predicate (relation term) ≝ λR.
- ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2).
-
-definition compatible_appl: predicate (relation term) ≝ λR.
- ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 →
- R (@B1.A1) (@B2.A2).
-
-lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R).
-#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/
-qed.
-
-lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R).
-#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/
-qed.
-
-lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R).
-#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/
-qed.
-
-lemma star_compatible_appl: ∀R. reflexive ? R →
- compatible_appl R → compatible_appl (star … R).
-#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/
-qed.
--- /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 "terms/lift.ma".
+
+(* DELIFTING SUBSTITUTION ***************************************************)
+
+(* Policy: depth (level) metavariables: d, e (as for lift) *)
+let rec dsubst D d M on M ≝ match M with
+[ VRef i ⇒ tri … i d (#i) (↑[i] D) (#(i-1))
+| Abst A ⇒ 𝛌. (dsubst D (d+1) A)
+| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A)
+].
+
+interpretation "delifting substitution"
+ 'DSubst D d M = (dsubst D d M).
+
+lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i.
+normalize /2 width=1/
+qed.
+
+lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
+normalize //
+qed.
+
+lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1).
+normalize /2 width=1/
+qed.
+
+theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
+ [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ 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
+ >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
+ | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
+ | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
+ [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
+ | lapply (ltn_to_ltO … Hid2) #Hi
+ >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
+ ]
+ ]
+| normalize #A #IHA #d1 #d2 #Hd21
+ lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd21
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+ [d2 ↙ 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
+ >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
+ >dsubst_vref_gt // /2 width=1/
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12 #Hd21
+ >IHA -IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
+ [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ 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
+ [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
+ lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
+ >(lift_vref_lt … Hid1) -Hid1 /2 width=1/
+ | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
+ ]
+ | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
+ >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // <plus_minus_m_m //
+ | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
+ lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
+ lapply (ltn_to_ltO … Hid2h) #Hi
+ >(dsubst_vref_gt … Hid2h)
+ >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1
+ >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12
+ elim (le_inv_plus_l … Hd12) #_ #Hhd2
+ >IHA -IHA /2 width=1/ <plus_minus //
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
+ [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ 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
+ >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
+ | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/
+ | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
+ [ lapply (ltn_to_ltO … Hid1) #Hi
+ >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
+ | destruct /2 width=1/
+ | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
+ >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/
+ >dsubst_vref_gt // /2 width=1/
+ ]
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12
+ lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
+ [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ 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.
+ ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
+
+definition dsubstable: predicate (relation term) ≝ λR.
+ ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ 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 lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
+ ∀l. dsubstable_dx (lstar S … R l).
+#S #R #HR #l #D #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+qed.
+
+lemma star_dsubstable: ∀R. reflexive ? R →
+ dsubstable R → dsubstable (star … R).
+#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
+qed.
--- /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 "terms/pointer_list.ma".
+include "terms/parallel_computation.ma".
+
+(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************)
+
+definition lsreds: ptrl → relation term ≝ lstar … lsred.
+
+interpretation "labelled sequential computation"
+ 'SeqRedStar M s N = (lsreds s M N).
+
+notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
+ non associative with precedence 45
+ for @{ 'SeqRedStar $M $s $N }.
+
+lemma lsreds_refl: reflexive … (lsreds (◊)).
+//
+qed.
+
+lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
+/2 width=3/
+qed-.
+
+lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
+/2 width=3/
+qed-.
+
+lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
+/2 width=1/
+qed.
+
+lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
+/2 width=5 by lstar_inv_nil/
+qed-.
+
+lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
+ ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
+/2 width=3 by lstar_inv_cons/
+qed-.
+
+lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
+/2 width=1 by lstar_inv_step/
+qed-.
+
+lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
+ ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
+/2 width=1 by lstar_inv_pos/
+qed-.
+
+lemma lsred_compatible_rc: ho_compatible_rc lsreds.
+/3 width=1/
+qed.
+
+lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
+/3 width=1/
+qed.
+
+lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
+/3 width=1/
+qed.
+
+lemma lsreds_lift: ∀s. liftable (lsreds s).
+/2 width=1/
+qed.
+
+lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
+/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
+qed-.
+
+lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
+/2 width=1/
+qed.
+
+theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
+/3 width=7 by lstar_singlevalued, lsred_mono/
+qed-.
+
+theorem lsreds_trans: ltransitive … lsreds.
+/2 width=3 by lstar_ltransitive/
+qed-.
+
+lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
+ @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(lsreds_trans … (@B2.A1)) /2 width=1/
+qed.
+
+lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
+ @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::s)@◊::◊] [↙B2] A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
+@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
+qed.
+
+(* Note: "|s|" should be unparetesized *)
+lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[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
+@(transitive_le … IHM2) -M2
+/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
+qed-.
+
+theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2
+@(preds_step_sn … IHM2) -M2 /2 width=2/
+qed.
+
+lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M1 -M2 /2 width=2/
+[ #A1 #A2 #_ * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+qed-.
+
+theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M2 /2 width=2/
+#M #M2 #_ #HM2 * #r #HM1
+elim (pred_lsreds … HM2) -HM2 #s #HM2
+lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
+qed-.
+
+theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
+ ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
+#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
+lapply (lsreds_preds … HM01) -s1 #HM01
+lapply (lsreds_preds … HM02) -s2 #HM02
+elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
+elim (preds_lsreds … HM1) -HM1
+elim (preds_lsreds … HM2) -HM2 /2 width=5/
+qed-.
--- /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 "terms/pointer.ma".
+include "terms/multiplicity.ma".
+
+(* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************)
+
+(* Note: the application "(A B)" is represented by "@B.A" following:
+ F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
+ Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
+*)
+inductive lsred: ptr → relation term ≝
+| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A)
+| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::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)
+.
+
+interpretation "labelled sequential reduction"
+ 'SeqRed M p N = (lsred p M N).
+
+(* Note: we do not use → since it is reserved by CIC *)
+notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )"
+ non associative with precedence 45
+ for @{ 'SeqRed $M $p $N }.
+
+lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥.
+#p #M #N * -p -M -N
+[ #B #A #i #H destruct
+| #p #A1 #A2 #_ #i #H destruct
+| #p #B1 #B2 #A #_ #i #H destruct
+| #p #B #A1 #A2 #_ #i #H destruct
+]
+qed-.
+
+lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p →
+ ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N.
+#p #M #N * -p -M -N
+[ #B #A #_ destruct /2 width=4/
+| #p #A1 #A2 #_ #H destruct
+| #p #B1 #B2 #A #_ #H destruct
+| #p #B #A1 #A2 #_ #H destruct
+]
+qed-.
+
+lemma lsred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p →
+ ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/
+| #p #B1 #B2 #A #_ #q #H destruct
+| #p #B #A1 #A2 #_ #q #H destruct
+]
+qed-.
+
+lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p →
+ ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N.
+#p #M #N * -p -M -N
+[ #B #A #q #H destruct
+| #p #A1 #A2 #_ #q #H destruct
+| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/
+| #p #B #A1 #A2 #_ #q #H destruct
+]
+qed-.
+
+lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p →
+ ∃∃B,A1,A2. A1 ↦[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
+| #p #B1 #B2 #A #_ #q #H destruct
+| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
+]
+qed-.
+
+lemma lsred_fwd_mult: ∀p,M,N. M ↦[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 *)
+| //
+| #p #B #D #A #_ #IHBD
+ @(lt_to_le_to_lt … (♯{B}*♯{B}+♯{A})) [ /2 width=1/ ] -D -p
+| #p #B #A #C #_ #IHAC
+ @(lt_to_le_to_lt … (♯{B}+♯{A}*♯{A})) [ /2 width=1/ ] -C -p
+]
+@(transitive_le … (♯{B}*♯{B}+♯{A}*♯{A})) [ /2 width=1/ ]
+>distributive_times_plus normalize /2 width=1/
+qed-.
+
+lemma lsred_lift: ∀p. liftable (lsred p).
+#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#B #A #d <dsubst_lift_le //
+qed.
+
+lemma lsred_inv_lift: ∀p. deliftable_sn (lsred p).
+#p #h #N1 #N2 #H elim H -p -N1 -N2
+[ #D #C #d #M1 #H
+ elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
+ elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
+| #p #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_abst … H) -H #A1 #HAC1 #H
+ elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro … (𝛌.A2)) // /2 width=1/
+| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
+ elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
+ @(ex2_intro … (@B2.A)) // /2 width=1/
+| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
+ elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro … (@B.A2)) // /2 width=1/
+]
+qed-.
+
+lemma lsred_dsubst: ∀p. dsubstable_dx (lsred p).
+#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#D2 #A #d >dsubst_dsubst_ge //
+qed.
+
+theorem lsred_mono: ∀p. singlevalued … (lsred p).
+#p #M #N1 #H elim H -p -M -N1
+[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H //
+ #D #C #H #HN2 destruct //
+| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+]
+qed-.
--- /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 "terms/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.
--- /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 "terms/term.ma".
+
+(* RELOCATION ***************************************************************)
+
+(* 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
+[ VRef i ⇒ #(tri … i d i (i + h) (i + h))
+| Abst A ⇒ 𝛌. (lift h (d+1) A)
+| Appl B A ⇒ @(lift h d B). (lift h d A)
+].
+
+interpretation "relocation" 'Lift h d M = (lift h d M).
+
+lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
+normalize /3 width=1/
+qed.
+
+lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
+#d #h #i #H elim (le_to_or_lt_eq … H) -H
+normalize // /3 width=1/
+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/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
+#j #d #Hjd #h * normalize
+[ #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) -Hid -Hjd //
+ | #H destruct >tri_eq in Hjd; #H
+ elim (plus_lt_false … H)
+ | >(tri_gt ???? … Hid)
+ lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
+ elim (plus_lt_false … H)
+ ]
+| #A #H destruct
+| #B #A #H destruct
+]
+qed.
+
+lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j →
+ d + h ≤ j ∧ M = #(j-h).
+#j #d #Hdj #h * normalize
+[ #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) #H destruct
+ lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
+ elim (lt_refl_false … H)
+ | #H -Hdj destruct /2 width=1/
+ | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
+ ]
+| #A #H destruct
+| #B #A #H destruct
+]
+qed-.
+
+lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥.
+#j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M
+lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
+elim (lt_refl_false … H)
+qed-.
+
+lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j →
+ ∀M. ↑[d, h] M = #j → M = #(j-h).
+#j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/
+qed.
+
+lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
+ ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
+#C #d #h * normalize
+[ #i #H destruct
+| #A #H destruct /2 width=3/
+| #B #A #H destruct
+]
+qed-.
+
+lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
+ ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
+#D #C #d #h * normalize
+[ #i #H destruct
+| #A #H destruct
+| #B #A #H destruct /2 width=5/
+]
+qed-.
+
+theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M.
+#h1 #h2 #M elim M -M
+[ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2)
+ >lift_vref_lt // /2 width=1/
+ | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
+ [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2)
+ >lift_vref_lt // -d2 /2 width=1/
+ | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/
+ >lift_vref_ge // /2 width=1/
+ ]
+ ]
+| normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA //
+]
+qed.
+
+theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M.
+#h1 #h2 #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
+ >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
+ >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA //
+]
+qed.
+
+theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M.
+#h1 #h2 #M #d1 #d2 #Hd12
+>(lift_lift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
+qed.
+
+(* Note: this is "∀h,d. injective … (lift h d)" *)
+theorem lift_inj: ∀h,M1,M2,d. ↑[d, h] M2 = ↑[d, h] M1 → M2 = M1.
+#h #M1 elim M1 -M1
+[ #i #M2 #d #H elim (lt_or_ge i d) #Hid
+ [ >(lift_vref_lt … Hid) in H; #H
+ >(lift_inv_vref_lt … Hid … H) -M2 -d -h //
+ | >(lift_vref_ge … Hid) in H; #H
+ >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/
+ ]
+| normalize #A1 #IHA1 #M2 #d #H
+ elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct
+ >(IHA1 … HA12) -IHA1 -A2 //
+| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H
+ elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
+ >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 //
+]
+qed-.
+
+theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 →
+ ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1.
+#h1 #h2 #M1 elim M1 -M1
+[ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
+ [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
+ >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/
+ | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
+ elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
+ @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1
+ >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
+ ]
+ | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
+ lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
+ elim (le_inv_plus_l … Hdh2i) #Hd2i #_
+ >(lift_vref_ge … Hid1) #H -Hid1
+ >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
+ @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *)
+ [ >lift_vref_ge // -Hd1i /3 width=1/
+ | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/
+ ]
+ ]
+| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H
+ elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct
+ elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1
+ @(ex2_intro … (𝛌.A)) normalize //
+| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H
+ elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
+ elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1
+ elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1
+ @(ex2_intro … (@B.A)) normalize //
+]
+qed-.
+
+theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2.
+#h1 #h2 #M1 elim M1 -M1
+[ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/
+ ]
+| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (lift_inv_abst … H) -H #A #HA12 #H destruct
+ >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/
+| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct
+ >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 //
+]
+qed-.
+
+theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] M2 = ↑[d1, h1] M1 →
+ ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1.
+#h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H
+elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
+lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
+elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/
+qed-.
+
+definition liftable: predicate (relation term) ≝ λR.
+ ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
+
+definition deliftable_sn: predicate (relation term) ≝ λR.
+ ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
+ ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
+
+lemma star_liftable: ∀R. liftable R → liftable (star … R).
+#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
+qed.
+
+lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
+#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
+#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
+elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
+elim (HR … HN2 … HMN) -N /3 width=3/
+qed-.
+
+lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
+ ∀l. liftable (lstar S … R l).
+#S #R #HR #l #h #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+qed.
+
+lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
+ ∀l. deliftable_sn (lstar S … R l).
+#S #R #HR #l #h #N1 #N2 #H
+@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
+#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
+elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
+elim (IHN2 … HMN) -N /3 width=3/
+qed-.
--- /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 "terms/delifting_substitution.ma".
+
+(* MULTIPLICITY *************************************************************)
+
+(* Note: this gives the number of variable references in M *)
+let rec mult M on M ≝ match M with
+[ VRef i ⇒ 1
+| Abst A ⇒ mult A
+| Appl B A ⇒ (mult B) + (mult A)
+].
+
+interpretation "term multiplicity"
+ 'Multiplicity M = (mult M).
+
+notation "hvbox( ♯{ term 46 M } )"
+ non associative with precedence 90
+ for @{ 'Multiplicity $M }.
+
+lemma mult_positive: ∀M. 0 < ♯{M}.
+#M elim M -M // /2 width=1/
+qed.
+
+lemma mult_lift: ∀h,M,d. ♯{↑[d, h] M} = ♯{M}.
+#h #M elim M -M normalize //
+qed.
+
+theorem mult_dsubst: ∀D,M,d. ♯{[d ↙ 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 //
+ | destruct >dsubst_vref_eq normalize //
+ | >(dsubst_vref_gt … Hid) normalize //
+ ]
+| normalize //
+| normalize #B #A #IHB #IHA #d
+ >distributive_times_plus_r /2 width=1/
+]
+qed.
--- /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 "terms/parallel_reduction.ma".
+
+(* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
+
+definition preds: relation term ≝ star … pred.
+
+interpretation "parallel computation"
+ 'ParRedStar M N = (preds M N).
+
+notation "hvbox( M ⤇* break term 46 N )"
+ non associative with precedence 45
+ for @{ 'ParRedStar $M $N }.
+
+lemma preds_refl: reflexive … preds.
+//
+qed.
+
+lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
+/2 width=3/
+qed-.
+
+lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
+/2 width=3/
+qed-.
+
+lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
+/2 width=1/
+qed.
+
+lemma preds_compatible_abst: compatible_abst preds.
+/3 width=1/
+qed.
+
+lemma preds_compatible_sn: compatible_sn preds.
+/3 width=1/
+qed.
+
+lemma preds_compatible_dx: compatible_dx preds.
+/3 width=1/
+qed.
+
+lemma preds_compatible_appl: compatible_appl preds.
+/3 width=1/
+qed.
+
+lemma preds_lift: liftable preds.
+/2 width=1/
+qed.
+
+lemma preds_inv_lift: deliftable_sn preds.
+/3 width=3 by star_deliftable_sn, pred_inv_lift/
+qed-.
+
+lemma preds_dsubst_dx: dsubstable_dx preds.
+/2 width=1/
+qed.
+
+lemma preds_dsubst: dsubstable preds.
+/2 width=1/
+qed.
+
+theorem preds_trans: transitive … preds.
+/2 width=3 by trans_star/
+qed-.
+
+lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 →
+ ∃∃M. M1 ⤇ M & M2 ⤇* M.
+/3 width=3 by star_strip, pred_conf/
+qed-.
+
+theorem preds_conf: confluent … preds.
+/3 width=3 by star_confluent, pred_conf/
+qed-.
--- /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 "terms/length.ma".
+include "terms/labeled_sequential_reduction.ma".
+
+(* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
+
+(* Note: the application "(A B)" is represented by "@B.A"
+ as for labelled sequential reduction
+*)
+inductive pred: relation term ≝
+| 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: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([↙B2]A2)
+.
+
+interpretation "parallel reduction"
+ 'ParRed M N = (pred M N).
+
+notation "hvbox( M ⤇ break term 46 N )"
+ non associative with precedence 45
+ for @{ 'ParRed $M $N }.
+
+lemma pred_refl: reflexive … pred.
+#M elim M -M // /2 width=1/
+qed.
+
+lemma pred_inv_vref: ∀M,N. M ⤇ N → ∀i. #i = M → #i = N.
+#M #N * -M -N //
+[ #A1 #A2 #_ #i #H destruct
+| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
+| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
+]
+qed-.
+
+lemma pred_inv_abst: ∀M,N. M ⤇ N → ∀A. 𝛌.A = M →
+ ∃∃C. A ⤇ C & 𝛌.C = N.
+#M #N * -M -N
+[ #i #A0 #H destruct
+| #A1 #A2 #HA12 #A0 #H destruct /2 width=3/
+| #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct
+| #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct
+]
+qed-.
+
+lemma pred_inv_appl: ∀M,N. M ⤇ N → ∀B,A. @B.A = M →
+ (∃∃D,C. B ⤇ D & A ⤇ C & @D.C = N) ∨
+ ∃∃A0,D,C0. B ⤇ D & A0 ⤇ C0 & 𝛌.A0 = A & [↙D]C0 = N.
+#M #N * -M -N
+[ #i #B0 #A0 #H destruct
+| #A1 #A2 #_ #B0 #A0 #H destruct
+| #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=5/
+| #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=7/
+]
+qed-.
+
+lemma pred_lift: liftable pred.
+#h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/
+#B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d <dsubst_lift_le // /2 width=1/
+qed.
+
+lemma pred_inv_lift: deliftable_sn pred.
+#h #N1 #N2 #H elim H -N1 -N2 /2 width=3/
+[ #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_abst … H) -H #A1 #HAC1 #H
+ elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro … (𝛌.A2)) // /2 width=1/
+| #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B1 #A1 #HBD1 #HAC1 #H
+ elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
+ elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro … (@B2.A2)) // /2 width=1/
+| #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
+ 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 … ([↙B2]A2)) /2 width=1/
+]
+qed-.
+
+lemma pred_dsubst: dsubstable pred.
+#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
+[ #i #d elim (lt_or_eq_or_gt i d) #Hid
+ [ >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
+ | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/
+ | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
+ ]
+| normalize /2 width=1/
+| normalize /2 width=1/
+| normalize #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d
+ >dsubst_dsubst_ge // /2 width=1/
+]
+qed.
+
+lemma pred_conf1_vref: ∀i. confluent1 … pred (#i).
+#i #M1 #H1 #M2 #H2
+<(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *)
+<(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *)
+/2 width=3/
+qed-.
+
+lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
+#A #IH #M1 #H1 #M2 #H2
+elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
+elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
+elim (IH … HA1 … HA2) -A /3 width=3/
+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 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 →
+ ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ 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 //
+elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
+qed-.
+
+theorem pred_conf: confluent … pred.
+#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
+ elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
+ elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *)
+ [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
+ elim (IH A … HA1 … HA2) -HA1 -HA2 //
+ elim (IH B … HB1 … HB2) // -A -B /3 width=5/
+ | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct
+ @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *)
+ | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
+ @ex2_commute @(pred_conf1_appl_beta … IH) //
+ | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
+ elim (IH B … HB1 … HB2) -HB1 -HB2 //
+ elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
+ ]
+]
+qed-.
+
+lemma lsred_pred: ∀p,M,N. M ↦[p] N → M ⤇ N.
+#p #M #N #H elim H -p -M -N /2 width=1/
+qed.
--- /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 "terms/term.ma".
+
+(* POINTER ******************************************************************)
+
+(* Policy: pointer step metavariables: c *)
+(* Note: this is a step of a path in the tree representation of a term:
+ rc (rectus) : proceed on the argument of an abstraction
+ sn (sinister): proceed on the left argument of an application
+ dx (dexter) : proceed on the right argument of an application
+*)
+inductive ptr_step: Type[0] ≝
+| rc: ptr_step
+| sn: ptr_step
+| dx: ptr_step
+.
+
+definition is_dx: predicate ptr_step ≝ λc. dx = c.
+
+(* Policy: pointer metavariables: p, q *)
+(* Note: this is a path in the tree representation of a term, heading to a redex *)
+definition ptr: Type[0] ≝ list ptr_step.
+
+(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *)
+definition in_whd: predicate ptr ≝ All … is_dx.
+
+lemma in_whd_ind: ∀R:predicate ptr. R (◊) →
+ (∀p. in_whd p → R p → R (dx::p)) →
+ ∀p. in_whd p → R p.
+#R #H #IH #p elim p -p // -H *
+#p #IHp * #H1 #H2 destruct /3 width=1/
+qed-.
+
+definition compatible_rc: predicate (ptr→relation term) ≝ λR.
+ ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (ptr→relation term) ≝ λR.
+ ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (ptr→relation term) ≝ λR.
+ ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).
--- /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 "terms/pointer.ma".
+
+(* POINTER LIST *************************************************************)
+
+(* Policy: pointer list metavariables: r, s *)
+definition ptrl: Type[0] ≝ list ptr.
+
+(* Note: a "whd" computation contracts just redexes in the whd *)
+definition is_whd: predicate ptrl ≝ All … in_whd.
+
+lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s).
+#s elim s -s //
+#p #s #IHs * /3 width=1/
+qed.
+
+lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s).
+#r elim r -r //
+#q #r #IHr * /3 width=1/
+qed.
+
+definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR.
+ ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
+
+definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR.
+ ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
+
+definition ho_compatible_dx: predicate (ptrl→relation term) ≝ λR.
+ ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
+
+lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
+#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+qed.
--- /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 "terms/pointer_list.ma".
+include "terms/pointer_order.ma".
+
+(* STANDARD POINTER LIST ****************************************************)
+
+(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
+definition is_standard: predicate ptrl ≝ Allr … ple.
+
+lemma is_standard_compatible: ∀c,s. is_standard s → is_standard (c:::s).
+#c #s elim s -s // #p * //
+#q #s #IHs * /3 width=1/
+qed.
+
+lemma is_standard_cons: ∀p,s. is_standard s → is_standard ((dx::p)::sn:::s).
+#p #s elim s -s // #q1 * /2 width=1/
+#q2 #s #IHs * /4 width=1/
+qed.
+
+lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_standard ((dx:::r)@sn:::s).
+#r elim r -r /3 width=1/ #p * /2 width=1/
+#q #r #IHr * /3 width=1/
+qed.
+
+theorem is_whd_is_standard: ∀s. is_whd s → is_standard s.
+#s elim s -s // #p * //
+#q #s #IHs * /3 width=1/
+qed.
+
+lemma is_standard_in_whd: ∀p. in_whd p → ∀s. is_standard s → is_standard (p::s).
+#p #Hp * // /3 width=1/
+qed.
+
+theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_standard (r@s).
+#r elim r -r // #p *
+[ #_ * /2 width=1/
+| #q #r #IHr * /3 width=1/
+]
+qed.
--- /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 "terms/pointer.ma".
+
+(* POINTER ORDER ************************************************************)
+
+(* Note: precedence relation on redex pointers: p ≺ q
+ to serve as base for the order relations: p < q and p ≤ q *)
+inductive pprec: relation ptr ≝
+| pprec_nil : ∀c,q. pprec (◊) (c::q)
+| ppprc_rc : ∀p,q. pprec (dx::p) (rc::q)
+| ppprc_sn : ∀p,q. pprec (rc::p) (sn::q)
+| pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q)
+| pprec_skip: pprec (dx::◊) ◊
+.
+
+interpretation "'precedes' on pointers"
+ 'prec p q = (pprec p q).
+
+(* Note: this should go to core_notation *)
+notation "hvbox(a break ≺ b)"
+ non associative with precedence 45
+ for @{ 'prec $a $b }.
+
+lemma pprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
+#p #q #H elim H -p -q // /2 width=1/
+[ #p #q * #H destruct
+| #p #q * #H destruct
+| #c #p #q #_ #IHpq * #H destruct /3 width=1/
+]
+qed-.
+
+(* Note: this is p < q *)
+definition plt: relation ptr ≝ TC … pprec.
+
+interpretation "'less than' on redex pointers"
+ 'lt p q = (plt p q).
+
+lemma plt_step_rc: ∀p,q. p ≺ q → p < q.
+/2 width=1/
+qed.
+
+lemma plt_nil: ∀c,p. ◊ < c::p.
+/2 width=1/
+qed.
+
+lemma plt_skip: dx::◊ < ◊.
+/2 width=1/
+qed.
+
+lemma plt_comp: ∀c,p,q. p < q → c::p < c::q.
+#c #p #q #H elim H -q /3 width=1/ /3 width=3/
+qed.
+
+theorem plt_trans: transitive … plt.
+/2 width=3/
+qed-.
+
+lemma plt_refl: ∀p. p < p.
+#p elim p -p /2 width=1/
+@(plt_trans … (dx::◊)) //
+qed.
+
+(* Note: this is p ≤ q *)
+definition ple: relation ptr ≝ star … pprec.
+
+interpretation "'less or equal to' on redex pointers"
+ 'leq p q = (ple p q).
+
+lemma ple_step_rc: ∀p,q. p ≺ q → p ≤ q.
+/2 width=1/
+qed.
+
+lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2.
+/2 width=3/
+qed-.
+
+lemma ple_rc: ∀p,q. dx::p ≤ rc::q.
+/2 width=1/
+qed.
+
+lemma ple_sn: ∀p,q. rc::p ≤ sn::q.
+/2 width=1/
+qed.
+
+lemma ple_skip: dx::◊ ≤ ◊.
+/2 width=1/
+qed.
+
+lemma ple_nil: ∀p. ◊ ≤ p.
+* // /2 width=1/
+qed.
+
+lemma ple_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2).
+#p1 #p2 #H elim H -p2 // /3 width=3/
+qed.
+
+lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊.
+#p #H @(star_ind_l ??????? H) -p //
+#p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/
+qed.
+
+theorem ple_trans: transitive … ple.
+/2 width=3/
+qed-.
+
+lemma ple_cons: ∀p,q. dx::p ≤ sn::q.
+#p #q
+@(ple_trans … (rc::q)) /2 width=1/
+qed.
+
+lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1.
+#p1 elim p1 -p1
+[ * /2 width=1/
+| #c1 #p1 #IHp1 * /2 width=1/
+ * #p2 cases c1 -c1 /2 width=1/
+ elim (IHp1 p2) -IHp1 /3 width=1/
+]
+qed-.
+
+lemma in_whd_ple_nil: ∀p. in_whd p → p ≤ ◊.
+#p #H @(in_whd_ind … H) -p // /2 width=1/
+qed.
+
+theorem in_whd_ple: ∀p. in_whd p → ∀q. p ≤ q.
+#p #H @(in_whd_ind … H) -p //
+#p #_ #IHp * /3 width=1/ * #q /2 width=1/
+qed.
+
+lemma ple_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p.
+#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_whd/
+qed-.
+
+lemma ple_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p.
+/2 width=1 by ple_nil_inv_in_whd/
+qed-.
--- /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 "terms/pointer_list.ma".
+
+(* POINTER TREE *************************************************************)
+
+(* Policy: pointer tree metavariables: P, Q *)
+(* Note: this is a binary tree on pointer sequences *)
+inductive ptrt: Type[0] ≝
+| tnil : ptrt
+| tcons: ptrl → ptrt → ptrt → ptrt
+.
+
+let rec length (P:ptrt) on P ≝ match P with
+[ tnil ⇒ 0
+| tcons s Q1 Q2 ⇒ length Q2 + length Q1 + |s|
+].
+
+interpretation "pointer tree length" 'card P = (length P).
--- /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 "terms/labeled_sequential_computation.ma".
+include "terms/pointer_list_standard.ma".
+
+(* KASHIMA'S "ST" COMPUTATION ***********************************************)
+
+(* Note: this is the "standard" computation of:
+ R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
+*)
+inductive st: relation term ≝
+| st_vref: ∀s,M,i. is_whd s → M ↦*[s] #i → st M (#i)
+| st_abst: ∀s,M,A1,A2. is_whd s → M ↦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
+| st_appl: ∀s,M,B1,B2,A1,A2. is_whd s → M ↦*[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 ⓢ⤇* break term 46 N )"
+ non associative with precedence 45
+ for @{ 'Std $M $N }.
+
+lemma st_inv_lref: ∀M,N. M ⓢ⤇* N → ∀j. #j = N →
+ ∃∃s. is_whd s & M ↦*[s] #j.
+#M #N * -M -N
+[ /2 width=3/
+| #s #M #A1 #A2 #_ #_ #_ #j #H destruct
+| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #j #H destruct
+]
+qed-.
+
+lemma st_inv_abst: ∀M,N. M ⓢ⤇* N → ∀C2. 𝛌.C2 = N →
+ ∃∃s,C1. is_whd s & M ↦*[s] 𝛌.C1 & C1 ⓢ⤇* C2.
+#M #N * -M -N
+[ #s #M #i #_ #_ #C2 #H destruct
+| #s #M #A1 #A2 #Hs #HM #A12 #C2 #H destruct /2 width=5/
+| #s #M #B1 #B2 #A1 #A2 #_ #_ #_ #_ #C2 #H destruct
+]
+qed-.
+
+lemma st_inv_appl: ∀M,N. M ⓢ⤇* N → ∀D2,C2. @D2.C2 = N →
+ ∃∃s,D1,C1. is_whd s & M ↦*[s] @D1.C1 & D1 ⓢ⤇* D2 & C1 ⓢ⤇* C2.
+#M #N * -M -N
+[ #s #M #i #_ #_ #D2 #C2 #H destruct
+| #s #M #A1 #A2 #_ #_ #_ #D2 #C2 #H destruct
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #HB12 #HA12 #D2 #C2 #H destruct /2 width=7/
+]
+qed-.
+
+lemma st_refl: reflexive … st.
+#M elim M -M /2 width=3/ /2 width=5/ /2 width=7/
+qed.
+
+lemma st_step_sn: ∀N1,N2. N1 ⓢ⤇* N2 → ∀s,M. is_whd s → M ↦*[s] N1 → M ⓢ⤇* N2.
+#N1 #N2 #H elim H -N1 -N2
+[ #r #N #i #Hr #HN #s #M #Hs #HMN
+ lapply (lsreds_trans … HMN … HN) -N /3 width=3/
+| #r #N #C1 #C2 #Hr #HN #_ #IHC12 #s #M #Hs #HMN
+ lapply (lsreds_trans … HMN … HN) -N /3 width=7/
+| #r #N #D1 #D2 #C1 #C2 #Hr #HN #_ #_ #IHD12 #IHC12 #s #M #Hs #HMN
+ lapply (lsreds_trans … HMN … HN) -N /3 width=9/
+]
+qed-.
+
+lemma st_step_rc: ∀s,M1,M2. is_whd s → M1 ↦*[s] M2 → M1 ⓢ⤇* M2.
+/3 width=5 by st_step_sn/
+qed.
+
+lemma st_lift: liftable st.
+#h #M1 #M2 #H elim H -M1 -M2
+[ /3 width=3/
+| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
+ @(st_abst … Hs) [2: @(lsreds_lift … HM) | skip ] -M // (**) (* auto fails here *)
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
+ @(st_appl … Hs) [3: @(lsreds_lift … HM) |1,2: skip ] -M // (**) (* auto fails here *)
+]
+qed.
+
+lemma st_inv_lift: deliftable_sn st.
+#h #N1 #N2 #H elim H -N1 -N2
+[ #s #N1 #i #Hs #HN1 #d #M1 #HMN1
+ elim (lsreds_inv_lift … HN1 … HMN1) -N1 /3 width=3/
+| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1
+ elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2
+ elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct
+ elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
+ @(ex2_intro … (𝛌.A2)) // /2 width=5/
+| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1
+ elim (lsreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2
+ elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct
+ elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *)
+ elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
+ @(ex2_intro … (@B2.A2)) // /2 width=7/
+]
+qed-.
+
+lemma st_dsubst: dsubstable st.
+#N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
+[ #s #M #i #Hs #HM #d elim (lt_or_eq_or_gt i d) #Hid
+ [ lapply (lsreds_dsubst … N1 … HM d) -HM
+ >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) /2 width=3/
+ | destruct >dsubst_vref_eq
+ @(st_step_sn (↑[0,i]N1) … s) /2 width=1/
+ | lapply (lsreds_dsubst … N1 … HM d) -HM
+ >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) /2 width=3/
+ ]
+| #s #M #A1 #A2 #Hs #HM #_ #IHA12 #d
+ lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=5/ (**) (* auto needs some help here *)
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ #IHB12 #IHA12 #d
+ lapply (lsreds_dsubst … N1 … HM d) -HM /2 width=7/ (**) (* auto needs some help here *)
+]
+qed.
+
+lemma st_step_dx: ∀p,M,M2. M ↦[p] M2 → ∀M1. M1 ⓢ⤇* M → M1 ⓢ⤇* 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 #Hs #HM1 #HB1 #H (**) (* simplify line *)
+ elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *)
+ lapply (lsreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1
+ lapply (lsreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1
+ @(st_step_sn … HM1) /2 width=1/ /4 width=1/
+| #p #A #A2 #_ #IHA2 #M1 #H
+ elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *)
+| #p #B #B2 #A #_ #IHB2 #M1 #H
+ elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
+| #p #B #A #A2 #_ #IHA2 #M1 #H
+ elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
+]
+qed-.
+
+lemma st_lsreds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ⤇* M2.
+#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by st_step_dx/
+qed.
+
+lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N →
+ ∃∃r. M ↦*[r] N & is_standard r.
+#M #N #H elim H -M -N
+[ #s #M #i #Hs #HM
+ lapply (is_whd_is_standard … Hs) -Hs /2 width=3/
+| #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr
+ lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
+ @(ex2_intro … HM) -M -A2 /3 width=1/
+| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
+ lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
+ lapply (lsreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM
+ @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/
+]
+qed-.
+
+theorem st_trans: transitive … st.
+#M1 #M #M2 #HM1 #HM2
+elim (st_inv_lsreds_is_standard … HM1) -HM1 #s1 #HM1 #_
+elim (st_inv_lsreds_is_standard … HM2) -HM2 #s2 #HM2 #_
+lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
+qed-.
+
+theorem lsreds_standard: ∀s,M,N. M ↦*[s] N → ∃∃r. M ↦*[r] N & is_standard r.
+#s #M #N #H
+@st_inv_lsreds_is_standard /2 width=2/
+qed-.
+
+(* Note: we use "lapply (rewrite_r ?? is_whd … Hq)" (procedural)
+ in place of "cut (is_whd (q::r)) [ >Hq ]" (declarative)
+*)
+lemma st_lsred_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ⓢ⤇* N1 →
+ ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ⤇* N2.
+#p #H @(in_whd_ind … H) -p
+[ #N1 #N2 #H1 #M1 #H2
+ elim (lsred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2
+ elim (st_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H
+ elim (st_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *)
+ lapply (lsreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1
+ lapply (lsreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1
+ elim (lsreds_inv_pos … HM1 ?) -HM1
+ [2: >length_append normalize in ⊢ (??(??%)); // ]
+ #q #r #M #Hq #HM1 #HM
+ lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
+ @(ex3_2_intro … HM1) -M1 // -q
+ @(st_step_sn … HM) /2 width=1/
+| #p #_ #IHp #N1 #N2 #H1 #M1 #H2
+ elim (lsred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *)
+ elim (st_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1
+ elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12
+ lapply (lsreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1
+ elim (lsreds_inv_pos … HM1 ?) -HM1
+ [2: >length_append normalize in ⊢ (??(??%)); // ]
+ #q #r #M #Hq #HM1 #HM
+ lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
+ @(ex3_2_intro … HM1) -M1 // -q /2 width=7/
+]
+qed-.
+
+theorem lsreds_lsred_swap: ∀s,M1,N1. M1 ↦*[s] N1 →
+ ∀p,N2. in_whd p → N1 ↦[p] N2 →
+ ∃∃q,r,M2. in_whd q & M1 ↦[q] M2 & M2 ↦*[r] N2 &
+ is_standard (q::r).
+#s #M1 #N1 #HMN1 #p #N2 #Hp #HN12
+lapply (st_lsreds … HMN1) -s #HMN1
+elim (st_lsred_swap … Hp … HN12 … HMN1) -p -N1 #q #M2 #Hq #HM12 #HMN2
+elim (st_inv_lsreds_is_standard … HMN2) -HMN2 /3 width=8/
+qed-.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* Initial invocation: - Patience on us to gain peace and perfection! - *)
+
+include "preamble.ma".
+include "notation.ma".
+
+(* TERM STRUCTURE ***********************************************************)
+
+(* Policy: term metavariables : A, B, C, D, M, N
+ depth metavariables: i, j
+*)
+inductive term: Type[0] ≝
+| VRef: nat → term (* variable reference by depth *)
+| Abst: term → term (* function formation *)
+| Appl: term → term → term (* function application *)
+.
+
+interpretation "term construction (variable reference by index)"
+ 'VariableReferenceByIndex i = (VRef i).
+
+interpretation "term construction (abstraction)"
+ 'Abstraction A = (Abst A).
+
+interpretation "term construction (application)"
+ 'Application C A = (Appl C A).
+
+definition compatible_abst: predicate (relation term) ≝ λR.
+ ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (relation term) ≝ λR.
+ ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (relation term) ≝ λR.
+ ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2).
+
+definition compatible_appl: predicate (relation term) ≝ λR.
+ ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 →
+ R (@B1.A1) (@B2.A2).
+
+lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R).
+#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/
+qed.
+
+lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R).
+#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/
+qed.
+
+lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R).
+#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/
+qed.
+
+lemma star_compatible_appl: ∀R. reflexive ? R →
+ compatible_appl R → compatible_appl (star … R).
+#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/
+qed.
notation > "hvbox({ ident i | term 19 p })" with precedence 90
for @{ 'subset (\lambda ${ident i}. $p)}.
-notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
-notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
notation "hvbox(a break ∈ b)" non associative with precedence 45
let predefined_classes = [
[":"; "⁝"; ];
["."; "•"; "◦"; ];
- ["#"; "⌘"; ];
+ ["#"; "â\99¯"; "â\8c\98"; ];
["-"; "÷"; "⊢"; "⊩"; ];
["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];
["→"; "↦"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
projects / helm.git / commitdiff