(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "basic_2/notation/relations/psubststar_4.ma".
include "basic_2/grammar/genv.ma".
include "basic_2/substitution/lsuby.ma".

(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)

(* avtivate genv *)
inductive cpys: relation4 genv lenv term term ≝
| cpys_atom : ∀I,G,L. cpys G L (⓪{I}) (⓪{I})
| cpys_delta: ∀I,G,L,K,V,V2,W2,i.
              ⇩[i] L ≡ K.ⓑ{I}V → cpys G K V V2 →
              ⇧[0, i + 1] V2 ≡ W2 → cpys G L (#i) W2
| cpys_bind : ∀a,I,G,L,V1,V2,T1,T2.
              cpys G L V1 V2 → cpys G (L.ⓑ{I}V1) T1 T2 →
              cpys G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
| cpys_flat : ∀I,G,L,V1,V2,T1,T2.
              cpys G L V1 V2 → cpys G L T1 T2 →
              cpys G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
.

interpretation
   "context-sensitive extended multiple substitution (term)"
   'PSubstStar G L T1 T2 = (cpys G L T1 T2).

(* Basic properties *********************************************************)

lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby.
#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
[ //
| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
  elim (lsuby_ldrop_trans … HL12 … HLK1) -HL12 -HLK1 *
  /3 width=7 by cpys_delta/
| /4 width=1 by lsuby_pair, cpys_bind/
| /3 width=1 by cpys_flat/
]
qed-.

(* Note: this is "∀L. reflexive … (cpys L)" *)
lemma cpys_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ▶* T.
#G #T elim T -T // * /2 width=1 by cpys_bind, cpys_flat/
qed.

lemma cpys_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶* V2 →
                    ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ▶* ②{I}V2.T.
* /2 width=1 by cpys_bind, cpys_flat/
qed.

lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶* V2 →
                     ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶* T2 →
                     ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* ⓑ{a,I}V2.T2.
/4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed.

lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓑ{I}V) →
                   ∃∃T2,T.  ⦃G, L⦄ ⊢ T1 ▶* T2 & ⇧[d, 1] T ≡ T2.
#I #G #K #V #T1 elim T1 -T1
[ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/
  #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
  destruct
  elim (lift_total V 0 (i+1)) #W #HVW
  elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/
| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
  elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
  [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_drop, lift_bind, ex2_2_intro/
  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/
  ]
]
qed-.

(* Basic inversion lemmas ***************************************************)

fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶* T2 → ∀J. T1 = ⓪{J} →
                         T2 = ⓪{J} ∨
                         ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
                                       ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
#G #L #T1 #T2 * -L -T1 -T2
[ #I #G #L #J #H destruct /2 width=1 by or_introl/
| #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by ex4_5_intro, or_intror/
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
]
qed-.

lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶* T2 →
                      T2 = ⓪{J} ∨
                      ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
                                    ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
/2 width=3 by cpys_inv_atom1_aux/ qed-.

lemma cpys_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ▶* T2 → T2 = ⋆k.
#G #L #T2 #k #H elim (cpys_inv_atom1 … H) -H // *
#I #K #V #V2 #i #_ #_ #_ #H destruct
qed-.

lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶* T2 →
                      T2 = #i ∨
                      ∃∃I,K,V,V2. ⇩[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶* V2 &
                                  ⇧[O, i + 1] V2 ≡ T2.
#G #L #T2 #i #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ *
#I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/
qed-.

lemma cpys_inv_lref1_ge: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶* T2 → |L| ≤ i → T2 = #i.
#G #L #T2 #i #H elim (cpys_inv_lref1 … H) -H // *
#I #K #V1 #V2 #HLK #_ #_ #HL -V2 lapply (ldrop_fwd_length_lt2 … HLK) -K -I -V1
#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
qed-.

lemma cpys_inv_gref1: ∀G,L,T2,p.  ⦃G, L⦄ ⊢ §p ▶* T2 → T2 = §p.
#G #L #T2 #p #H elim (cpys_inv_atom1 … H) -H // *
#I #K #V #V2 #i #_ #_ #_ #H destruct
qed-.

fact cpys_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶* U2 →
                         ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 →
                         ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶* T2 &
                                  U2 = ⓑ{a,J}V2.T2.
#G #L #U1 #U2 * -L -U1 -U2
[ #I #G #L #b #J #W #U1 #H destruct
| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
]
qed-.

lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* U2 →
                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶* T2 &
                               U2 = ⓑ{a,I}V2.T2.
/2 width=3 by cpys_inv_bind1_aux/ qed-.

lemma cpys_inv_bind1_ext: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* U2 → ∀J.
                          ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶* T2 &
                                   U2 = ⓑ{a,I}V2.T2.
#a #I #G #L #V1 #T1 #U2 #H #J elim (cpys_inv_bind1 … H) -H
#V2 #T2 #HV12 #HT12 #H destruct
/4 width=5 by lsuby_cpys_trans, lsuby_pair, ex3_2_intro/
qed-.

fact cpys_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ▶* U2 →
                         ∀J,V1,U1. U = ⓕ{J}V1.U1 →
                         ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L⦄ ⊢ U1 ▶* T2 &
                                  U2 = ⓕ{J}V2.T2.
#G #L #U #U2 * -L -U -U2
[ #I #G #L #J #W #U1 #H destruct
| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/
]
qed-.

(* Note: lemma 1250 *)
lemma cpys_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ▶* U2 →
                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶* V2 & ⦃G, L⦄ ⊢ U1 ▶* T2 &
                               U2 = ⓕ{I}V2.T2.
/2 width=3 by cpys_inv_flat1_aux/ qed-.

(* Basic forward lemmas *****************************************************)

lemma cpys_fwd_bind1: ∀a,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶* T → ∀b,J.
                      ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,J}V1.T1 ▶* ⓑ{b,J}V2.T2 &
                               T = ⓑ{a,I}V2.T2.
#a #I #G #L #V1 #T1 #T #H #b #J elim (cpys_inv_bind1_ext … H J) -H
#V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpys_bind, ex2_2_intro/
qed-.