- pointer structure simplified

- new properties on poiner orders
- last lemma in Kashima's article proved

diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma
index 6309d6b5394022ec0091c60f97a144445e2cca3a..4441961e1319391ec6d0cae55ff69827014f3efa 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_hap_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_computation.ma
@@ -46,6 +46,11 @@ lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
 /2 width=1 by lstar_inv_step/
 qed-.
 
+lemma lhap_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 lhap_compatible_dx: ho_compatible_dx lhap.
 /3 width=1/
 qed.

diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
index 4a7392a7646eaff25e913ebfc1e9919f28e5d69b..a609078fe56494417e19d8b4cc5a1a7673cb1380 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
@@ -43,6 +43,11 @@ 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.

diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
index 21d24c668002263f8312da073b024d2a24e7e3d9..0c75f86e2b4af80bbf55ed1b91f49c546f15802c 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
+++ b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
@@ -23,7 +23,7 @@ include "multiplicity.ma".
 *)
 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_abst   : ∀p,A1,A2. lsred p A1 A2 → lsred (sn::p) (𝛌.A1) (𝛌.A2) 
 | lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A)
 | lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2)
 .
@@ -55,22 +55,13 @@ lemma lsred_inv_nil: ∀p,M,N. M ⇀[p] N → ◊ = p →
 ]
 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 →
+                    (∃∃A1,A2. A1 ⇀[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨
                     ∃∃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 #A1 #A2 #HA12 #q #H destruct /3 width=5/
+| #p #B1 #B2 #A #HB12 #q #H destruct /3 width=6/
 | #p #B #A1 #A2 #_ #q #H destruct
 ]
 qed-.
@@ -132,8 +123,14 @@ 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 ] #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 #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+  [ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+  | #D1 #D2 #C #_ #H destruct
+  ]
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+  [ #C1 #C2 #_ #H destruct
+  | #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 ] #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *)
 ]
 qed-.

diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma
index 74977c3904f2dc7d59de1d5c175dc5855db44330..30b4fdf6409b7690a05b7b7995e9592d92f90c20 100644 (file)
--- a/matita/matita/contribs/lambda/pointer.ma
+++ b/matita/matita/contribs/lambda/pointer.ma
@@ -18,12 +18,17 @@ include "term.ma".
 
 (* 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
+         rc (rectus)  : not needed (we use sn instead)
          sn (sinister): proceed on the left argument of an application
+                        or on the argument of an abstraction (this would be rc)
          dx (dexter)  : proceed on the right argument of an application
 *)
+(* Remark: the following breaks destruct because of δ-expansions
+           definition ptr_step: Type[0] ≝ bool.
+           definition sn: bool ≝ true.
+           definition dx: bool ≝ false.
+*)
 inductive ptr_step: Type[0] ≝
-| rc: ptr_step
 | sn: ptr_step
 | dx: ptr_step
 .
@@ -45,7 +50,7 @@ lemma in_head_ind: ∀R:predicate ptr. R (◊) →
 qed-.
 
 definition compatible_rc: predicate (ptr→relation term) ≝ λR.
-                          ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
+                          ∀p,A1,A2. R p A1 A2 → R (sn::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).

diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma
index ffd1e725d409351ec5908f4ee4e2280069a68515..24dcad4fa953a14824c8c4f610287967fa850e69 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_order.ma
+++ b/matita/matita/contribs/lambda/pointer_order.ma
@@ -20,8 +20,7 @@ include "pointer.ma".
          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 (dx::p) (sn::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::◊) ◊
 .
@@ -37,7 +36,6 @@ notation "hvbox(a break ≺ b)"
 lemma pprec_fwd_in_head: ∀p,q. p ≺ q → in_head q → in_head 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-.
@@ -48,6 +46,31 @@ 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.
 
@@ -83,6 +106,15 @@ lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊.
 #p #q #Hpq #_ #H @(ple_step_sn … H) -H /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_head_ple_nil: ∀p. in_head p → p ≤ ◊.
 #p #H @(in_head_ind … H) -p // /2 width=1/
 qed.

diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma
index 9f4e63cd6e4f9dd0b6048c2ede1947447c5fcdcf..0a3d3422c37a98cbce8316b4c5c162158f82f19b 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_sequence.ma
+++ b/matita/matita/contribs/lambda/pointer_sequence.ma
@@ -57,7 +57,7 @@ theorem is_head_is_le_trans: ∀r. is_head r → ∀s. is_le s → is_le (r@s).
 qed.
 
 definition ho_compatible_rc: predicate (pseq→relation term) ≝ λR.
-                             ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
+                             ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2).
 
 definition ho_compatible_sn: predicate (pseq→relation term) ≝ λR.
                              ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index 640615d596f2aa2aa2947a23884d7a3ec9b09916..958f1059a053b90a4f7f0fea0a9c39a8a3c72555 100644 (file)
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -100,3 +100,14 @@ 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}.
+
+(* lstar *)
+
+(* Note: this cannot be in lib because of the missing xoa quantifier *)
+lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
+                     ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
+#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
+[ #H elim (lt_refl_false … H) 
+| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
+]
+qed-.

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index b536bb3a3708596bb4d9f8cd3b486475f5193bc3..75d72ed0ce0ad0dc443a54851a6baa02686db37b 100644 (file)
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -133,7 +133,7 @@ lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⥤* N →
 | #s #M #A1 #A2 #H #_ * #r #HA12 #Hr
   lapply (lhap_inv_lsreds … H) #HM
   lapply (lhap_inv_head … H) -H #Hs
-  lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
+  lapply (lsreds_trans … HM (sn:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
   @(ex2_intro … HM) -M -A2 /3 width=1/
 | #s #M #B1 #B2 #A1 #A2 #H #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
   lapply (lhap_inv_lsreds … H) #HM
@@ -149,9 +149,9 @@ lemma st_step_dx: ∀p,M,M2. M ⇀[p] M2 → ∀M1. M1 ⓢ⥤* M → M1 ⓢ⥤*
 [ #B #A #M1 #H
   elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #HM1 #HB1 #H (**) (* simplify line *)
   elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #HM #HA1 (**) (* simplify line *)
-  @(st_step_sn … ([⬐B1]A1) … (s@(dx:::r)@(◊::◊))) /2 width=1/ -B -A
-  @(lhap_trans … HM1) -M1
-  @(lhap_step_dx … (@B1.𝛌.A1)) // -s /2 width=1/
+  lapply (lhap_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1
+  lapply (lhap_step_dx … HM1 (◊) ([⬐B1]A1) ?) -HM1 // #HM1
+  @(st_step_sn … HM1) /2 width=1/
 | #p #A #A2 #_ #IHA2 #M1 #H
   elim (st_inv_abst … H ??) -H [3: // |2: skip ] /3 width=4/ (**) (* simplify line *)
 | #p #B #B2 #A #_ #IHB2 #M1 #H
@@ -161,6 +161,30 @@ lemma st_step_dx: ∀p,M,M2. M ⇀[p] M2 → ∀M1. M1 ⓢ⥤* M → M1 ⓢ⥤*
 ]
 qed-.
 
+lemma st_lhap1_swap: ∀p,N1,N2. N1 ⓗ⇀[p] N2 → ∀M1. M1 ⓢ⥤* N1 →
+                     ∃∃q,M2. M1 ⓗ⇀[q] M2 & M2 ⓢ⥤* N2.
+#p #N1 #N2 #H elim H -p -N1 -N2
+[ #D #C #M1 #H
+  elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #D1 #N #HM1 #HD1 #H (**) (* simplify line *)
+  elim (st_inv_abst … H ??) -H [3: // |2: skip ] #r #C1 #HN #HC1 (**) (* simplify line *)
+  lapply (lhap_trans … HM1 … (dx:::r) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1
+  lapply (lhap_step_dx … HM1 (◊) ([⬐D1]C1) ?) -HM1 // #HM1
+  elim (lhap_inv_pos … HM1 ?) -HM1
+  [2: >length_append normalize in ⊢ (??(??%)); // ]
+  #q #r #M #_ #HM1 #HM -s
+  @(ex2_2_intro … HM1) -M1
+  @(st_step_sn … HM) /2 width=1/
+| #p #D #C1 #C2 #_ #IHC12 #M1 #H -p
+  elim (st_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B #A1 #HM1 #HBD #HAC1 (**) (* simplify line *)
+  elim (IHC12 … HAC1) -C1 #p #C1 #HAC1 #HC12
+  lapply (lhap_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1
+  elim (lhap_inv_pos … HM1 ?) -HM1
+  [2: >length_append normalize in ⊢ (??(??%)); // ]
+  #q #r #M #_ #HM1 #HM -p -s
+  @(ex2_2_intro … HM1) -M1 /2 width=6/
+]
+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.
@@ -177,3 +201,12 @@ theorem lsreds_standard: ∀s,M,N. M ⇀*[s] N →
 #s #M #N #H
 @st_inv_lsreds_is_le /2 width=2/
 qed-.
+
+theorem lsreds_lhap1_swap: ∀s,M1,N1. M1 ⇀*[s] N1 → ∀p,N2. N1 ⓗ⇀[p] N2 →
+                           ∃∃q,r,M2. M1 ⓗ⇀[q] M2 & M2 ⇀*[r] N2 & is_le (q::r).
+#s #M1 #N1 #HMN1 #p #N2 #HN12
+lapply (st_lsreds … HMN1) -s #HMN1
+elim (st_lhap1_swap … HN12 … HMN1) -p -N1 #q #M2 #HM12 #HMN2
+elim (st_inv_lsreds_is_le … HMN2) -HMN2 #r #HMN2 #Hr
+lapply (lhap1_inv_head … HM12) /3 width=7/
+qed-.