From 1407a045a96f3a96e341ba9ee16aa633467164b6 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 21 Oct 2015 17:00:58 +0000
Subject: [PATCH] new results on multiple relocation

---
 .../ground_2/relocation/trace_after.ma        | 37 +++++++++++++++++--
 .../ground_2/relocation/trace_at.ma           | 23 +++++++++++-
 2 files changed, 56 insertions(+), 4 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
index 72c5d1612..4bc0233a2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
@@ -125,7 +125,7 @@ lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄
                     ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
 [ #i1 #i #H elim (at_inv_empty … H) -H
-  #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/  
+  #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
 | #cs1 #cs2 #cs #_ * #IH #i1 #i #H
   [ elim (at_inv_true … H) -H *
     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
@@ -142,8 +142,8 @@ lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄
 ]
 qed-.
 
-lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
-                    ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
+lemma after_at1_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
+                     ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
 [ #i1 #i2 #H elim (at_inv_empty … H) -H
   #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
@@ -162,6 +162,37 @@ lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1
 ]
 qed-.
 
+lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
+                    ∀i1,i2,i. @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs⦄ ≡ i.
+#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at1_fwd … Hcs … Hi1) -cs1
+#j #H #Hj >(at_mono … Hi2 … H) -i2 //
+qed-.
+
+lemma after_fwd_at1: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
+                     ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2.
+#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at_fwd … Hcs … Hi1) -cs
+#j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
+qed-.
+
+lemma after_fwd_at2: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
+                     ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
+[ #i1 #i2 #i #Hi #Hi1 elim (at_inv_empty … Hi1) -Hi1 //
+| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #i #Hi #Hi1
+  [ elim (at_inv_true … Hi1) -Hi1 *
+    [ -IH #H1 #H2 destruct >(at_inv_true_zero_sn … Hi) -i //
+    | #j1 #j2 #H1 #H2 #Hj12 destruct elim (at_inv_true_succ_sn … Hi) -Hi
+      #j #H #Hj1 destruct /3 width=3 by at_succ/
+    ]
+  | elim (at_inv_false … Hi1) -Hi1
+    #j2 #H #Hj2 destruct elim (at_inv_false … Hi) -Hi
+    #j #H #Hj destruct /3 width=3 by at_succ/
+  ]
+| #cs1 #cs2 #cs #_ #IH #i1 #i2 #i #Hi #Hi2 elim (at_inv_false … Hi) -Hi
+  #j #H #Hj destruct /3 width=3 by at_false/
+]
+qed-.
+
 (* Main properties **********************************************************)
 
 theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 →
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
index b40b1c87b..0fd397829 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
@@ -181,7 +181,7 @@ lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
 ]
 qed-.
 
-lemma at_at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
+lemma at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
 #cs elim cs -cs [ | * #cs #IH ]
 [ * [2: #i1 ] * [2,4: #i2 ]
   [4: /2 width=1 by at_empty, or_introl/
@@ -202,6 +202,27 @@ lemma at_at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
 ]
 qed-.
 
+lemma is_at_dec: ∀cs,i2. Decidable (∃i1. @⦃i1, cs⦄ ≡ i2).
+#cs elim cs -cs
+[ * /3 width=2 by ex_intro, or_introl/
+  #i2 @or_intror * /2 width=3 by at_inv_empty_succ_dx/
+| * #cs #IH * [2,4: #i2 ]
+  [ elim (IH i2) -IH
+    [ * /4 width=2 by at_succ, ex_intro, or_introl/
+    | #H @or_intror * #x #Hx
+      elim (at_inv_true_succ_dx … Hx) -Hx
+      /3 width=2 by ex_intro/
+    ]
+  | elim (IH i2) -IH
+    [ * /4 width=2 by at_false, ex_intro, or_introl/
+    | #H @or_intror * /4 width=2 by at_inv_false_S, ex_intro/ 
+    ]
+  | /3 width=2 by at_zero, ex_intro, or_introl/
+  | @or_intror * /2 width=3 by at_inv_false_O/
+  ]
+]
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma at_increasing: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ i2.
-- 
2.39.2