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 elim H -l -M1 -M2 // /3 width=3/
+#T #R #HR #l #D #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
qed.
(* Note: this is the "head in application" computation of:
R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
*)
-definition lhap: rpseq → relation term ≝ lstar … lhap1.
+definition lhap: pseq → relation term ≝ lstar … lhap1.
interpretation "labelled 'hap' computation"
'HApStar M p N = (lhap p M N).
lemma lhap_dsubst: ∀s. dsubstable_dx (lhap s).
/2 width=1/
qed.
-(*
+
theorem lhap_mono: ∀s. singlevalued … (lhap s).
/3 width=7 by lstar_singlevalued, lhap1_mono/
qed-.
-*)
+
theorem lhap_trans: ∀s1,M1,M. M1 ⓗ⇀*[s1] M →
∀s2,M2. M ⓗ⇀*[s2] M2 → M1 ⓗ⇀*[s1@s2] M2.
/2 width=3 by lstar_trans/
qed-.
-(*
-lemma hap_appl: appl_compatible_dx hap.
-/3 width=1/
+
+lemma lhap_appl: ∀s,B,A1,A2. A1 ⓗ⇀*[s] A2 → @B.A1 ⓗ⇀*[dx:::s] @B.A2.
+#s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
qed.
-*)
-lemma lhap_spine_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_spine s.
-#s #M1 #M2 #H elim H -s -M1 -M2 //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lhap1_spine_fwd … HM1) -HM1 /2 width=1/
+
+lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/
+qed.
+
+lemma lhap_inv_head: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_head s.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/
qed-.
-lemma lhap_lsreds_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
-#s #M1 #M2 #H elim H -s -M1 -M2 //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lhap1_lsred_fwd … HM1) -HM1 /2 width=3/
+lemma lhap_inv_lsreds: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/
qed-.
-lemma lhap_le_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s.
-(*
-#M1 #M2 #H @(star_ind_l ??????? H) -M1 /3 width=3/
-#M1 #M #HM1 #H * #s * #H1s #H2s
-generalize in match HM1; -HM1 generalize in match M1; -M1
-@(star_ind_l ??????? H) -M
-[ #M1 #HM12 elim (hap1_lsred … HM12) -HM12 /4 width=3/
-| #M0 #M1 #HM01 #HM12 #_ #M #HM0 #HM02
-*)
+lemma lhap_fwd_le: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 /3 width=3/
+#a1 #s #M1 #M #HM1 #IHM1
+generalize in match HM1; -HM1
+cases IHM1 -s -M -M2 //
+#a #M0 #M #HM0 #s #M2 #_ #HM10 #H -M2
+lapply (lhap1_fwd_le … HM10 … HM0) -M -M0 -M1 /2 width=1/
+qed-.
(* *)
(**************************************************************************)
+include "pointer_order.ma".
include "labelled_sequential_reduction.ma".
(* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************)
(* Note: this is one step of the "head in application" computation of:
R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
*)
-inductive lhap1: rptr → relation term ≝
+inductive lhap1: ptr → relation term ≝
| hap1_beta: ∀B,A. lhap1 (◊) (@B.𝛌.A) ([⬐B]A)
-| hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (false::p) (@B.A1) (@B.A2)
+| hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2)
.
interpretation "labelled 'hap' reduction"
non associative with precedence 45
for @{ 'HAp $M $p $N }.
+lemma lhap1_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 #_ /2 width=4/
+| #p #B #A1 #A2 #_ #H destruct
+]
+qed-.
+
+lemma lhap1_inv_cons: ∀p,M,N. M ⓗ⇀[p] N → ∀c,q. c::q = p →
+ ∃∃B,A1,A2. dx = c & A1 ⓗ⇀[q] A2 & @B.A1 = M & @B.A2 = N.
+#p #M #N * -p -M -N
+[ #B #A #c #q #H destruct
+| #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/
+]
+qed-.
+
lemma lhap1_inv_abst_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀A. 𝛌.A = M → ⊥.
#p #M #N * -p -M -N
[ #B #A #A0 #H destruct
lemma lhap1_inv_appl_sn: ∀p,M,N. M ⓗ⇀[p] N → ∀B,A. @B.A = M →
(∃∃C. ◊ = p & 𝛌.C = A & [⬐B]C = N) ∨
- ∃∃q,C. A ⓗ⇀[q] C & false::q = p & @B.C = N.
+ ∃∃q,C. A ⓗ⇀[q] C & dx::q = p & @B.C = N.
#p #M #N * -p -M -N
[ #B #A #B0 #A0 #H destruct /3 width=3/
| #p #B #A1 #A2 #HA12 #B0 #A0 #H destruct /3 width=5/
#D2 #A #d >dsubst_dsubst_ge //
qed.
-lemma lhap1_spine_fwd: ∀p,M,N. M ⓗ⇀[p] N → in_spine p.
-#p #M #N #H elim H -p -M -N // /2 width=1/
+lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N.
+#p #H @(in_head_ind … H) -p
+[ #M #N #H elim (lsred_inv_nil … H ?) -H //
+| #p #_ #IHp #M #N #H
+ elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] /3 width=1/ (**) (* simplify line *)
+]
+qed.
+
+lemma lhap1_inv_head: ∀p,M,N. M ⓗ⇀[p] N → in_head p.
+#p #M #N #H elim H -p -M -N // /2 width=1/
qed-.
-lemma lhap1_lsred_fwd: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N.
+lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N.
#p #M #N #H elim H -p -M -N // /2 width=1/
qed-.
-lemma lhap1_le_fwd: ∀p1,M1,M. M1 ⓗ⇀[p1] M → ∀p2,M2. M ⓗ⇀[p2] M2 → p1 ≤ p2.
+lemma lhap1_fwd_le: ∀p1,M1,M. M1 ⓗ⇀[p1] M → ∀p2,M2. M ⓗ⇀[p2] M2 → p1 ≤ p2.
#p1 #M1 #M #H elim H -p1 -M1 -M //
#p1 #B #A1 #A2 #HA12 #IHA12 #p2 #M2 #H
elim (lhap1_inv_appl_sn … H ???) -H [5: // |2,3: skip ] * (**) (* simplify line *)
| -HA12 /3 width=2/
]
qed-.
+
+theorem lhap1_mono: ∀p. singlevalued … (lhap1 p).
+#p #M #N1 #H elim H -p -M -N1
+[ #B #A #N2 #H
+ elim (lhap1_inv_nil … H ?) -H // #D #C #H #HN2 destruct //
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H
+ elim (lhap1_inv_cons … H ???) -H [4: // |2,3: skip ] (**) (* simplify line *)
+ #D #C1 #C2 #_ #HC12 #H #HN2 destruct /3 width=1/
+]
+qed-.
(* *)
(**************************************************************************)
-include "redex_pointer_sequence.ma".
+include "pointer_sequence.ma".
include "labelled_sequential_reduction.ma".
(* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
-definition lsreds: rpseq → relation term ≝ lstar … lsred.
+definition lsreds: pseq → relation term ≝ lstar … lsred.
interpretation "labelled sequential computation"
'SeqRedStar M s N = (lsreds s M N).
(* Note: "|s|" should be unparetesized *)
lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
-#s #M1 #M2 #H elim H -s -M1 -M2 normalize //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
+#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 *)
(* *)
(**************************************************************************)
-include "redex_pointer.ma".
+include "pointer.ma".
include "multiplicity.ma".
(* LABELLED SEQUENTIAL REDUCTION (SINGLE STEP) ******************************)
F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
*)
-inductive lsred: rptr → relation term ≝
+inductive lsred: ptr → relation term ≝
| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A)
-| lsred_abst : ∀p,A,C. lsred p A C → lsred p (𝛌.A) (𝛌.C)
-| lsred_appl_sn: ∀p,B,D,A. lsred p B D → lsred (true::p) (@B.A) (@D.A)
-| lsred_appl_dx: ∀p,B,A,C. lsred p A C → lsred (false::p) (@B.A) (@B.C)
+| 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"
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 #A #C #_ #i #H destruct
-| #p #B #D #A #_ #i #H destruct
-| #p #B #A #C #_ #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_beta: ∀p,M,N. M ⇀[p] N → ∀D,C. @D.C = M → ◊ = p →
- ∃∃A. 𝛌.A = C & [⬐D] A = N.
+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 #D0 #C0 #H #_ destruct /2 width=3/
-| #p #A #C #_ #D0 #C0 #H destruct
-| #p #B #D #A #_ #D0 #C0 #_ #H destruct
-| #p #B #A #C #_ #D0 #C0 #_ #H destruct
+[ #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_abst: ∀p,M,N. M ⇀[p] N → ∀A. 𝛌.A = M →
- ∃∃C. A ⇀[p] C & 𝛌.C = N.
+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 #A0 #H destruct
-| #p #A #C #HAC #A0 #H destruct /2 width=3/
-| #p #B #D #A #_ #A0 #H destruct
-| #p #B #A #C #_ #A0 #H destruct
+[ #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_appl_sn: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → true::q = p →
- ∃∃D. B ⇀[q] D & @D.A = N.
+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 #B0 #A0 #p0 #_ #H destruct
-| #p #A #C #_ #B0 #D0 #p0 #H destruct
-| #p #B #D #A #HBD #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/
-| #p #B #A #C #_ #B0 #A0 #p0 #_ #H destruct
+[ #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_appl_dx: ∀p,M,N. M ⇀[p] N → ∀B,A,q. @B.A = M → false::q = p →
- ∃∃C. A ⇀[q] C & @B.C = N.
+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 #B0 #A0 #p0 #_ #H destruct
-| #p #A #C #_ #B0 #D0 #p0 #H destruct
-| #p #B #D #A #_ #B0 #A0 #p0 #_ #H destruct
-| #p #B #A #C #HAC #B0 #A0 #p0 #H1 #H2 destruct /2 width=3/
+[ #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-.
theorem lsred_mono: ∀p. singlevalued … (lsred p).
#p #M #N1 #H elim H -p -M -N1
-[ #B #A #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *)
-| #p #A #C #_ #IHAC #N2 #H elim (lsred_inv_abst … H ??) -H [3: // |2: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *)
-| #p #B #D #A #_ #IHBD #N2 #H elim (lsred_inv_appl_sn … H ?????) -H [5,6: // |2,3,4: skip ] #D0 #HBD #H destruct /3 width=1/ (**) (* simplify line *)
-| #p #B #A #C #_ #IHAC #N2 #H elim (lsred_inv_appl_dx … H ?????) -H [5,6: // |2,3,4: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *)
+[ #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 ] #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *)
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *)
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *)
]
qed-.
lemma lstar_liftable: ∀T,R. (∀t. liftable (R t)) →
∀l. liftable (lstar T … R l).
-#T #R #HR #l #h #M1 #M2 #H elim H -l -M1 -M2 // /3 width=3/
+#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 elim H -l -N1 -N2 /2 width=3/
-#t #N1 #N #HN1 #l #N2 #_ #IHN2 #d #M1 #HMN1
+#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-.
*)
inductive pred: relation term ≝
| pred_vref: ∀i. pred (#i) (#i)
-| pred_abst: ∀A,C. pred A C → pred (𝛌.A) (𝛌.C)
-| pred_appl: ∀B,D,A,C. pred B D → pred A C → pred (@B.A) (@D.C)
-| pred_beta: ∀B,D,A,C. pred B D → pred A C → pred (@B.𝛌.A) ([⬐D]C)
+| 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"
lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N.
#M #N * -M -N //
-[ #A #C #_ #i #H destruct
-| #B #D #A #C #_ #_ #i #H destruct
-| #B #D #A #C #_ #_ #i #H destruct
+[ #A1 #A2 #_ #i #H destruct
+| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
+| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
]
qed-.
∃∃C. A ⥤ C & 𝛌.C = N.
#M #N * -M -N
[ #i #A0 #H destruct
-| #A #C #HAC #A0 #H destruct /2 width=3/
-| #B #D #A #C #_ #_ #A0 #H destruct
-| #B #D #A #C #_ #_ #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-.
∃∃A0,D,C0. B ⥤ D & A0 ⥤ C0 & 𝛌.A0 = A & [⬐D]C0 = N.
#M #N * -M -N
[ #i #B0 #A0 #H destruct
-| #A #C #_ #B0 #A0 #H destruct
-| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=5/
-| #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=7/
+| #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/
-#D #D #A #C #_ #_ #IHBD #IHAC #d <dsubst_lift_le // /2 width=1/
+#B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d <dsubst_lift_le // /2 width=1/
qed.
lemma pred_inv_lift: deliftable_sn pred.
]
| normalize /2 width=1/
| normalize /2 width=1/
-| normalize #B #D #A #C #_ #_ #IHBD #IHAC #d
+| normalize #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d
>dsubst_dsubst_ge // /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 "preamble.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 the head" when is not under an abstraction nor in the lefr argument of an application *)
+definition in_head: predicate ptr ≝ All … is_dx.
+
+lemma in_head_ind: ∀R:predicate ptr. R (◊) →
+ (∀p. in_head p → R p → R (dx::p)) →
+ ∀p. in_head p → R p.
+#R #H #IH #p elim p -p // -H *
+#p #IHp * #H1 #H2 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 "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_cons: ∀p,q. pprec (dx::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 }.
+
+(* Note: this is p < q *)
+definition plt: relation ptr ≝ TC … pprec.
+
+interpretation "'less than' on redex pointers"
+ 'lt p q = (plt p q).
+
+(* 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 pprec_ple: ∀p,q. p ≺ q → p ≤ q.
+/2 width=1/
+qed.
+
+lemma ple_dx: 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.
--- /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_order.ma".
+
+(* POINTER SEQUENCE *********************************************************)
+
+(* Policy: pointer sequence metavariables: r, s *)
+definition pseq: Type[0] ≝ list ptr.
+
+(* Note: a "head" computation contracts just redexes in the head *)
+definition is_head: predicate pseq ≝ All … in_head.
+
+(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
+definition is_le: predicate pseq ≝ Allr … ple.
R : arbitrary relation
T, U : arbitrary small type
-a, b : boolean
+c : pointer step
d, e : variable reference depth
h : relocation height
i, j : de Bruijn index
k : relocation height
l : arbitrary list
m, n : measures on terms
-p, q : redex pointer
-r, s : redex pointer sequence
+p, q : pointer
+r, s : pointer sequence
t, u : arbitrary element
(**************************************************************************)
include "basics/star.ma".
-include "basics/lists/list.ma".
+include "basics/lists/lstar.ma".
include "arithmetics/exp.ma".
include "xoa_notation.ma".
definition confluent: ∀A. predicate (relation A) ≝ λA,R.
∀a0. confluent1 … R a0.
-(* booleans *)
-
-definition is_false: predicate bool ≝ λb.
- false = b.
-
(* arithmetics *)
lemma lt_refl_false: ∀n. n < n → ⊥.
notation > "◊"
non associative with precedence 90
for @{'nil}.
+
+definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a.
+ map … (cons … a).
+
+interpretation "map_cons" 'ho_cons a l = (map_cons ? a l).
+
+notation "hvbox(a ::: break l)"
+ right associative with precedence 47
+ for @{'ho_cons $a $l}.
+++ /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".
-
-(* REDEX POINTER ************************************************************)
-
-(* Policy: boolean metavariables: a, b
- pointer metavariables: p, q
-*)
-(* Note: this is a path in the tree representation of a term
- in which abstraction nodes are omitted;
- on application nodes, "false" means "proceed right"
- and "true" means "proceed left"
-*)
-definition rptr: Type[0] ≝ list bool.
-
-(* Note: a redex is "in the spine" when is not in the argument of an application *)
-definition in_spine: predicate rptr ≝ λp.
- All … is_false p.
-
-(* Note: precedence relation on redex pointers: p ≺ q
- to serve as base for the order relations: p < q and p ≤ q *)
-inductive rpprec: relation rptr ≝
-| rpprec_nil : ∀b,q. rpprec (◊) (b::q)
-| rppprc_cons: ∀p,q. rpprec (false::p) (true::q)
-| rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q)
-| rpprec_skip: rpprec (false::◊) ◊
-.
-
-interpretation "'precedes' on redex pointers"
- 'prec p q = (rpprec p q).
-
-(* Note: this should go to core_notation *)
-notation "hvbox(a break ≺ b)"
- non associative with precedence 45
- for @{ 'prec $a $b }.
-
-(* Note: this is p < q *)
-definition rplt: relation rptr ≝ TC … rpprec.
-
-interpretation "'less than' on redex pointers"
- 'lt p q = (rplt p q).
-
-(* Note: this is p ≤ q *)
-definition rple: relation rptr ≝ star … rpprec.
-
-interpretation "'less or equal to' on redex pointers"
- 'leq p q = (rple p q).
-
-lemma rpprec_rple: ∀p,q. p ≺ q → p ≤ q.
-/2 width=1/
-qed.
-
-lemma rple_false: false::◊ ≤ ◊.
-/2 width=1/
-qed.
-
-lemma rple_nil: ∀p. ◊ ≤ p.
-* // /2 width=1/
-qed.
-
-lemma rple_comp: ∀p1,p2. p1 ≤ p2 → ∀b. (b::p1) ≤ (b::p2).
-#p1 #p2 #H elim H -p2 // /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 "redex_pointer.ma".
-
-(* REDEX POINTER SEQUENCE ***************************************************)
-
-(* Policy: pointer sequence metavariables: r, s *)
-
-definition rpseq: Type[0] \def list rptr.
-
-(* Note: a "spine" computation contracts just redexes in the spine *)
-definition is_spine: predicate rpseq ≝ λs.
- All … in_spine s.
-
-(* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
-definition is_le: predicate rpseq ≝ λs.
- Allr … rple s.
-
-(* Note: a normal spine computation *)
-definition is_spine_le: predicate rpseq ≝ λs.
- is_spine s ∧ is_le s.
*)
inductive st: relation term ≝
| st_vref: ∀s,M,i. lhap s M (#i) → st M (#i)
-| st_abst: ∀s,M,A,C. lhap s M (𝛌.A) → st A C → st M (𝛌.C)
-| st_appl: ∀s,M,B,D,A,C. lhap s M (@B.A) → st B D → st A C → st M (@D.C)
+| st_abst: ∀s,M,A1,A2. lhap s M (𝛌.A1) → st A1 A2 → st M (𝛌.A2)
+| st_appl: ∀s,M,B1,B2,A1,A2. lhap s M (@B1.A1) → st B1 B2 → st A1 A2 → st M (@B2.A2)
.
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
- <key name="ex">3 1</key>
+ <key name="ex">2 2</key>
+ <key name="ex">3 1</key>
<key name="ex">3 2</key>
+ <key name="ex">3 3</key>
<key name="ex">4 3</key>
<key name="or">3</key>
</section>
include "basics/pts.ma".
+(* multiple existental quantifier (2, 2) *)
+
+inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
+ | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+
(* multiple existental quantifier (3, 1) *)
inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
+(* multiple existental quantifier (3, 3) *)
+
+inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝
+ | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
+
(* multiple existental quantifier (4, 3) *)
inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
(* This file was generated by xoa.native: do not edit *********************)
+(* multiple existental quantifier (2, 2) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }.
+
(* multiple existental quantifier (3, 1) *)
notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }.
+(* multiple existental quantifier (3, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }.
+
(* multiple existental quantifier (4, 3) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
projects / helm.git / commitdiff