From 23e75ebc00553e178e090ca1373ac075ee650a60 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 8 Dec 2012 23:26:45 +0000
Subject: [PATCH] - list.ma: improved notation for constant lists (a "term 19"
 was missing) - lambda: more properties on pointers, extra xoa quantifier
 removed, bugfix in notations and names

---
 .../lambda/labelled_hap_computation.ma        | 13 ++-----
 .../contribs/lambda/labelled_hap_reduction.ma | 36 +------------------
 .../lambda/labelled_sequential_computation.ma |  4 +--
 .../contribs/lambda/parallel_reduction.ma     |  2 +-
 .../matita/contribs/lambda/pointer_order.ma   | 33 +++++++++++++++--
 .../contribs/lambda/pointer_sequence.ma       |  6 ++++
 .../matita/contribs/lambda/st_computation.ma  | 22 ++++++++++--
 matita/matita/contribs/lambda/xoa.conf.xml    |  1 -
 matita/matita/contribs/lambda/xoa.ma          |  8 -----
 matita/matita/contribs/lambda/xoa_notation.ma | 10 ------
 matita/matita/lib/basics/lists/list.ma        |  2 +-
 11 files changed, 63 insertions(+), 74 deletions(-)

diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma
index 70cc06b79..5cd7678d1 100644
--- a/matita/matita/contribs/lambda/labelled_hap_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_computation.ma
@@ -29,7 +29,7 @@ notation "hvbox( M break ⓗ⇀* [ term 46 p ] break term 46 N )"
    non associative with precedence 45
    for @{ 'HApStar $M $p $N }.
 
-lemma lhap1_lhap: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
+lemma lhap_step_rc: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
 /2 width=1/
 qed.
 
@@ -42,7 +42,7 @@ lemma lhap_inv_cons: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → ∀q,r. q::r = s →
 /2 width=3 by lstar_inv_cons/
 qed-.
 
-lemma lhap_inv_lhap1: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
+lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
 /2 width=1 by lstar_inv_step/
 qed-.
 
@@ -87,12 +87,3 @@ lemma lhap_inv_lsreds: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
 #p #s #M1 #M #HM1 #_ #IHM2
 lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/
 qed-.
-
-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-.
diff --git a/matita/matita/contribs/lambda/labelled_hap_reduction.ma b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
index 575abd342..e1f279f67 100644
--- a/matita/matita/contribs/lambda/labelled_hap_reduction.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
@@ -48,30 +48,6 @@ lemma lhap1_inv_cons: ∀p,M,N. M ⓗ⇀[p] N → ∀c,q. c::q = p →
 ]
 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
-| #p #B #A1 #A2 #_ #A0 #H destruct
-]
-qed-.
-
-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 & 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/
-]
-qed-.
-
-lemma lhap1_inv_abst_dx: ∀p,M,N. M ⓗ⇀[p] N → ∀C. 𝛌.C = N →
-                         ∃∃B,A. ◊ = p & @B.𝛌.A = M & 𝛌.C = [⬐B]A.
-#p #M #N * -p -M -N
-[ #B #A #C #H /2 width=4/
-| #p #B #A1 #A2 #_ #C #H destruct
-]
-qed-.
-
 lemma lhap1_lift: ∀p. liftable (lhap1 p).
 #p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
 #B #A #d <dsubst_lift_le //
@@ -100,7 +76,7 @@ lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N
 | #p #_ #IHp #M #N #H
   elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] /3 width=1/ (**) (* simplify line *)
 ]
-qed.  
+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/
@@ -110,16 +86,6 @@ 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_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 *)
-[ -IHA12 #C2 #Hp2 #HAC2 #_
-  elim (lhap1_inv_abst_dx … HA12 … HAC2) -A2 #B1 #C1 #Hp1 #_ #_ //
-| -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
diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
index 1ec666483..1f32ee8e0 100644
--- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
@@ -26,7 +26,7 @@ notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )"
    non associative with precedence 45
    for @{ 'SeqRedStar $M $s $N }.
 
-lemma lsred_lsreds: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
+lemma lsreds_step_rc: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
 /2 width=1/
 qed.
 
@@ -39,7 +39,7 @@ lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s →
 /2 width=3 by lstar_inv_cons/
 qed-.
 
-lemma lsreds_inv_lsred: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
+lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
 /2 width=1 by lstar_inv_step/
 qed-.
 
diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma
index 91fe30e1c..6b352da4d 100644
--- a/matita/matita/contribs/lambda/parallel_reduction.ma
+++ b/matita/matita/contribs/lambda/parallel_reduction.ma
@@ -30,7 +30,7 @@ inductive pred: relation term ≝
 interpretation "parallel reduction"
     'ParRed M N = (pred M N).
 
-notation "hvbox( M break ⥤ break term 46 N )"
+notation "hvbox( M ⥤ break term 46 N )"
    non associative with precedence 45
    for @{ 'ParRed $M $N }.
 
diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma
index 9d79e9dc6..ddcc3fd9e 100644
--- a/matita/matita/contribs/lambda/pointer_order.ma
+++ b/matita/matita/contribs/lambda/pointer_order.ma
@@ -33,6 +33,13 @@ notation "hvbox(a break ≺ b)"
    non associative with precedence 45
    for @{ 'prec $a $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
+| #c #p #q #_ #IHpq * #H destruct /3 width=1/
+]
+qed-.
+
 (* Note: this is p < q *)
 definition plt: relation ptr ≝ TC … pprec.
 
@@ -45,11 +52,15 @@ 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.
+lemma ple_step_rc: ∀p,q. p ≺ q → p ≤ q.
 /2 width=1/
 qed.
 
-lemma ple_dx: dx::◊ ≤ ◊.
+lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2.
+/2 width=3/
+qed-.
+
+lemma ple_skip: dx::◊ ≤ ◊.
 /2 width=1/
 qed.
 
@@ -60,3 +71,21 @@ 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.
+
+lemma in_head_ple_nil: ∀p. in_head p → p ≤ ◊.
+#p #H @(in_head_ind … H) -p // /2 width=1/
+qed.
+
+theorem in_head_ple: ∀p. in_head p → ∀q. in_head q → p ≤ q.
+#p #H @(in_head_ind … H) -p //
+#p #Hp #IHp #q #H @(in_head_ind … H) -q /3 width=1/
+qed.
+
+lemma ple_nil_inv_in_head: ∀p. p ≤ ◊ → in_head p.
+#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_head/
+qed-.
diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma
index 131711426..9a93f27ff 100644
--- a/matita/matita/contribs/lambda/pointer_sequence.ma
+++ b/matita/matita/contribs/lambda/pointer_sequence.ma
@@ -24,3 +24,9 @@ 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.
+
+theorem is_head_is_le: ∀s. is_head s → is_le s.
+#s elim s -s //
+#p #s elim s -s //
+#q #s #_ #IHs * #Hp * /4 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index c9f9aa947..028cd8a41 100644
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -20,8 +20,24 @@ include "labelled_hap_computation.ma".
          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
 *)
 inductive st: relation term ≝
-| st_vref: ∀s,M,i. lhap s M (#i) → st M (#i)
-| 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)
+| st_vref: ∀s,M,i. M ⓗ⇀*[s] #i → st M (#i)
+| st_abst: ∀s,M,A1,A2. M ⓗ⇀*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
+| st_appl: ∀s,M,B1,B2,A1,A2. 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 }.
+
+axiom st_refl: reflexive … st.
+
+axiom st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ⥤* N2.
+
+axiom st_lift: liftable st.
+
+axiom st_inv_lift: deliftable_sn st.
+
+axiom st_dsubst: dsubstable st.
diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml
index f6a3e9d8d..223be4324 100644
--- a/matita/matita/contribs/lambda/xoa.conf.xml
+++ b/matita/matita/contribs/lambda/xoa.conf.xml
@@ -9,7 +9,6 @@
     <key name="notations">xoa_notation</key>
     <key name="include">basics/pts.ma</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>
diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma
index 9d4ee880b..1e82edec7 100644
--- a/matita/matita/contribs/lambda/xoa.ma
+++ b/matita/matita/contribs/lambda/xoa.ma
@@ -24,14 +24,6 @@ inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
 
 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 ≝
-   | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
-
 (* multiple existental quantifier (3, 2) *)
 
 inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/xoa_notation.ma
index 6151aa044..b14f46cec 100644
--- a/matita/matita/contribs/lambda/xoa_notation.ma
+++ b/matita/matita/contribs/lambda/xoa_notation.ma
@@ -24,16 +24,6 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19
  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}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }.
-
-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.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }.
-
 (* multiple existental quantifier (3, 2) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 7429625dc..c1f6ab738 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -20,7 +20,7 @@ notation "hvbox(hd break :: tl)"
   right associative with precedence 47
   for @{'cons $hd $tl}.
 
-notation "[ list0 x sep ; ]"
+notation "[ list0 term 19 x sep ; ]"
   non associative with precedence 90
   for ${fold right @'nil rec acc @{'cons $x $acc}}.
 
-- 
2.39.2