+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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-.
projects / helm.git / blobdiff