From ecf5a379cf6b646426f296c9a33d4ee0e5b2d04a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 16 Jan 2013 19:05:56 +0000
Subject: [PATCH 1/1] - paths and left residuals: first case of the equivalence
 proved! - some corrections and additions - some "?" removed in customized
 eliminations

---
 .../lambda/paths/labeled_st_computation.ma    | 27 +++++++++++++++--
 .../lambda/paths/labeled_st_reduction.ma      | 15 ++++++++++
 .../contribs/lambda/paths/standard_order.ma   |  8 +++--
 .../contribs/lambda/paths/standard_trace.ma   | 30 +++++++++++++++----
 matita/matita/contribs/lambda/paths/trace.ma  | 15 ++++++----
 .../contribs/lambda/subterms/booleanized.ma   |  5 ++--
 matita/matita/lib/basics/lists/list.ma        | 15 ++++++++++
 7 files changed, 95 insertions(+), 20 deletions(-)

diff --git a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma
index 8ee4d304f..6050696f9 100644
--- a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma
+++ b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma
@@ -29,11 +29,21 @@ notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )"
    for @{ 'StdStar $F $p $G }.
 
 lemma pl_sts_fwd_pl_sreds: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ⇓F1 ↦*[s] ⇓F2.
-#s #F1 #F2 #H @(lstar_ind_r ????????? H) -s -F2 //
+#s #F1 #F2 #H @(lstar_ind_r … s F2 H) -s -F2 //
 #p #s #F #F2 #_ #HF2 #IHF1
 lapply (pl_st_fwd_pl_sred … HF2) -HF2 /2 width=3/
 qed-.
 
+lemma pl_sts_inv_pl_sreds: ∀s,M1,F2. {⊤}⇑M1 Ⓡ↦*[s] F2 → is_whd s →
+                           ∃∃M2. M1 ↦*[s] M2 & {⊤}⇑M2 = F2.
+#s #M1 #F2 #H @(lstar_ind_r … s F2 H) -s -F2 /2 width=3/
+#p #s #F #F2 #_ #HF2 #IHF #H
+elim (is_whd_inv_append … H) -H #Hs * #Hp #_
+elim (IHF Hs) -IHF -Hs #M #HM #H destruct
+elim (pl_st_inv_pl_sred … HF2) -HF2 // -Hp #M2 #HM2 #H
+lapply (pl_sreds_step_dx … HM … HM2) -M /2 width=3/
+qed-.
+
 lemma pl_sts_refl: reflexive … (pl_sts (◊)).
 //
 qed.
@@ -100,10 +110,21 @@ axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M →
                                  ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F →
                                  is_standard (s@(p::◊)) →
                                  ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2.
-
+(*
+#p #M #M2 #H elim H -p -M -M2
+[ #B #A #F #HF #s #M1 #HM1 #Hs
+  lapply (is_standard_fwd_is_whd … Hs) -Hs // #Hs
+  elim (pl_sts_inv_pl_sreds … HM1 Hs) -HM1 -Hs #M #_ #H -s -M1 destruct
+  >carrier_boolean in HF; #H destruct normalize /2 width=3/
+| #p #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
+  elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
+(*  
+  elim (carrier_inv_appl … HF) -HF #b1 #V #G #HV #HG #HF
+*)  
+*)
 theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s →
                                      ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2.
-#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 /2 width=3/
+#s #M1 #M2 #H @(lstar_ind_r … s M2 H) -s -M2 /2 width=3/
 #p #s #M #M2 #_ #HM2 #IHM1 #Hsp
 lapply (is_standard_fwd_append_sn … Hsp) #Hs
 elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
diff --git a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
index 101954e59..cdbe979a5 100644
--- a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
+++ b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
@@ -118,6 +118,21 @@ lemma pl_st_inv_dx: ∀p,F,G. F Ⓡ↦[p] G → ∀q. dx::q = p →
 ]
 qed-.
 
+lemma pl_st_inv_pl_sred: ∀p. in_whd p → ∀M1,F2. {⊤}⇑M1 Ⓡ↦[p] F2 →
+                         ∃∃M2. M1 ↦[p] M2 & {⊤}⇑M2 = F2.
+#p @(in_whd_ind … p) -p
+[ #M1 #F2 #H
+  elim (pl_st_inv_nil … H ?) -H // #V #T #HM1 #H
+  elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #N #_ #HB #HN #HM1
+  elim (boolean_inv_abst … HN) -HN #A #_ #HA #HN destruct /2 width=3/
+| #p #_ #IHp #M1 #F2 #H
+  elim (pl_st_inv_dx … H ??) -H [3: // |2:skip ] #b #V #T1 #T2 #HT12 #HM1 #H (**) (* simplify line *)
+  elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #A #Hb #HB #HA #HM1 destruct
+  elim (IHp … HT12) -IHp -HT12 #C #HAC #H destruct
+  @(ex2_intro … (@B.C)) // /2 width=1/ (**) (* auto needs some help here *)
+]
+qed-.
+
 lemma pl_st_lift: ∀p. sliftable (pl_st p).
 #p #h #F1 #F2 #H elim H -p -F1 -F2 /2 width=1/
 [ #V #T #d normalize <sdsubst_slift_le //
diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma
index 9bf484143..09d143874 100644
--- a/matita/matita/contribs/lambda/paths/standard_order.ma
+++ b/matita/matita/contribs/lambda/paths/standard_order.ma
@@ -51,7 +51,7 @@ lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀o. (o::p1) ≤ (o::p2).
 qed.
 
 lemma sle_skip_sle: ∀p. p ≤ ◊ → dx::p ≤ ◊.
-#p #H @(star_ind_l ??????? H) -p //
+#p #H @(star_ind_l … p H) -p //
 #p #q #Hpq #_ #H @(sle_step_sn … H) -H /2 width=1/
 qed.
 
@@ -91,9 +91,13 @@ theorem in_whd_sle: ∀p. in_whd p → ∀q. p ≤ q.
 qed.
 
 lemma sle_nil_inv_in_whd: ∀p. p ≤ ◊ → in_whd p.
-#p #H @(star_ind_l ??????? H) -p // /2 width=3 by sprec_fwd_in_whd/
+#p #H @(star_ind_l … p H) -p // /2 width=3 by sprec_fwd_in_whd/
 qed-.
 
 lemma sle_inv_in_whd: ∀p. (∀q. p ≤ q) → in_whd p.
 /2 width=1 by sle_nil_inv_in_whd/
 qed-.
+
+lemma sle_fwd_in_whd: ∀p,q. p ≤ q → in_whd q → in_whd p.
+#p #q #H @(star_ind_l … p H) -p // /3 width=3 by sprec_fwd_in_whd/
+qed-.
diff --git a/matita/matita/contribs/lambda/paths/standard_trace.ma b/matita/matita/contribs/lambda/paths/standard_trace.ma
index 444237640..0550ab24f 100644
--- a/matita/matita/contribs/lambda/paths/standard_trace.ma
+++ b/matita/matita/contribs/lambda/paths/standard_trace.ma
@@ -20,6 +20,14 @@ include "paths/standard_order.ma".
 (* Note: to us, a "standard" computation contracts redexes in non-decreasing positions *)
 definition is_standard: predicate trace ≝ Allr … sle.
 
+lemma is_standard_fwd_append_sn: ∀s,r. is_standard (s@r) → is_standard s.
+/2 width=2 by Allr_fwd_append_sn/
+qed-.
+
+lemma is_standard_fwd_cons: ∀p,s. is_standard (p::s) → is_standard s.
+/2 width=2 by Allr_fwd_cons/
+qed-.
+
 lemma is_standard_compatible: ∀o,s. is_standard s → is_standard (o:::s).
 #o #s elim s -s // #p * //
 #q #s #IHs * /3 width=1/
@@ -35,15 +43,22 @@ lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_sta
 #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_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2.
+#s2 #p2 #s1 elim s1 -s1
+[ #p1 * //
+| #q1 #s1 #IHs1 #p1 * /3 width=3 by sle_trans/
+]
+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: ∀s. is_whd s → is_standard s.
+#s elim s -s // #p * //
+#q #s #IHs * /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/
@@ -51,6 +66,9 @@ theorem is_whd_is_standard_trans: ∀r. is_whd r → ∀s. is_standard s → is_
 ]
 qed.
 
-lemma is_standard_fwd_append_sn: ∀s,r. is_standard (s@r) → is_standard s.
-/2 width=2 by Allr_fwd_append_sn/
+lemma is_standard_fwd_is_whd: ∀s,p,r. in_whd p → is_standard (r@(p::s)) → is_whd r.
+#s #p #r elim r -r // #q #r #IHr #Hp #H
+lapply (is_standard_fwd_cons … H)
+lapply (is_standard_fwd_sle … H) #Hqp
+lapply (sle_fwd_in_whd … Hqp Hp) /3 width=1/
 qed-.
diff --git a/matita/matita/contribs/lambda/paths/trace.ma b/matita/matita/contribs/lambda/paths/trace.ma
index 53b979809..c8e427e27 100644
--- a/matita/matita/contribs/lambda/paths/trace.ma
+++ b/matita/matita/contribs/lambda/paths/trace.ma
@@ -24,14 +24,17 @@ definition is_whd: predicate trace ≝ 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/ 
+#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/
+/2 width=1 by All_append/
 qed.
 
+lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s.
+/2 width=1 by All_inv_append/
+qed-.
+
 definition ho_compatible_rc: predicate (trace→relation term) ≝ λR.
                              ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
 
@@ -42,13 +45,13 @@ definition ho_compatible_dx: predicate (trace→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/
+#R #HR #s #A1 #A2 #H @(lstar_ind_l … s A1 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/
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l … s B1 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/
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda/subterms/booleanized.ma b/matita/matita/contribs/lambda/subterms/booleanized.ma
index 87b84b26b..b3258d224 100644
--- a/matita/matita/contribs/lambda/subterms/booleanized.ma
+++ b/matita/matita/contribs/lambda/subterms/booleanized.ma
@@ -12,15 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "subterms/carrier.ma".
 include "subterms/boolean.ma".
 
-(* BOOLEANIZED SUBSET (EMPTY OR FULL)  **************************************)
+(* BOOLEANIZED SUBSET (EMPTY OR FULL) ***************************************)
 
 definition booleanized: bool → subterms → subterms ≝
    λb,F. {b}⇑⇓F.
 
-interpretation "make boolean (subterms)"
+interpretation "booleanized (subterms)"
    'ProjectSame b F = (booleanized b F).
 
 notation "hvbox( { term 46 b } ⇕ break term 46 F)"
diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a51998ae4..48ee3078a 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -445,6 +445,17 @@ lemma All_nth : ∀A,P,n,l.
   ]
 ] qed.
 
+lemma All_append: ∀A,P,l1,l2. All A P l1 → All A P l2 → All A P (l1@l2).
+#A #P #l1 elim l1 -l1 //
+#a #l1 #IHl1 #l2 * /3 width=1/
+qed.
+
+lemma All_inv_append: ∀A,P,l1,l2. All A P (l1@l2) → All A P l1 ∧ All A P l2.
+#A #P #l1 elim l1 -l1 /2 width=1/
+#a #l1 #IHl1 #l2 * #Ha #Hl12
+elim (IHl1 … Hl12) -IHl1 -Hl12 /3 width=1/
+qed-.
+
 (**************************** Allr ******************************)
 
 let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
@@ -457,6 +468,10 @@ lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
 #A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
 qed-.
 
+lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l.
+#A #R #a * // #a0 #l * //
+qed-.
+
 (**************************** Exists *******************************)
 
 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
-- 
2.39.2