--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PSubstNormal $G $L $T $d $e }.
>(cpr_inv_sort1 … H) //
qed.
+lemma cnr_lref_free: ∀G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
+#G #L #i #Hi #X #H elim (cpr_inv_lref1 … H) -H // *
+#K #V1 #V2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -HLK
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+qed.
+
+(* Basic_1: was only: nf2_csort_lref *)
+lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
+#G #L #i #HL @cnr_lref_free >(ldrop_fwd_length … HL) -HL //
+qed.
+
(* Basic_1: was: nf2_abst *)
lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}W.T⦄.
#a #G #L #W #T #HW #HT #X #H
(* Advanced properties ******************************************************)
-(* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
-#G #L #i #HL #X #H
-elim (cpr_inv_lref1 … H) -H // *
-#K #V1 #V2 #HLK #_ #_
-lapply (ldrop_mono … HL … HLK) -L #H destruct
-qed.
-
(* Basic_1: was: nf2_lref_abst *)
lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
#G #L #K #V #i #HLK #X #H
lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
qed.
+lemma cnx_lref_free: ∀h,g,G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
+#h #g #G #L #i #Hi #X #H elim (cpx_inv_lref1 … H) -H // *
+#I #K #V1 #V2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -HLK
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+qed.
+
+lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
+#h #g #G #L #i #HL @cnx_lref_free >(ldrop_fwd_length … HL) -HL //
+qed.
+
lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}W.T⦄.
#h #g #a #G #L #W #T #HW #HT #X #H
(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
-(* Advanced properties ******************************************************)
-
-lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
-#h #g #G #L #i #HL #X #H
-elim (cpx_inv_lref1 … H) -H // *
-#I #K #V1 #V2 #HLK #_ #_
-lapply (ldrop_mono … HL … HLK) -L #H destruct
-qed.
-
(* Relocation properties ****************************************************)
lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⇩[s, d, e] L0 ≡ L →
--- /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/psubstnormal_5.ma".
+include "basic_2/relocation/cpy.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
+
+definition cny: ∀d,e. relation3 genv lenv term ≝
+ λd,e,G,L. NF … (cpy d e G L) (eq …).
+
+interpretation
+ "normality for context-sensitive extended substitution (term)"
+ 'PSubstNormal G L T d e = (cny d e G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ →
+ ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i.
+#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/
+#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/
+#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/
+#Hi elim (ldrop_O1_lt L i) //
+#I #K #V #HLK elim (lift_total V 0 (i+1))
+#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK
+#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e //
+qed-.
+
+lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄.
+#a #I #G #L #V1 #T1 #d #e #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1
+| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1
+]
+/2 width=1 by cpy_bind/ #H destruct //
+qed-.
+
+lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄.
+#I #G #L #V1 #T1 #d #e #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1
+| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1
+]
+/2 width=1 by cpy_flat/ #H destruct //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄.
+#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H //
+qed.
+
+lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // *
+#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK
+#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
+qed.
+
+lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL //
+qed.
+
+lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // *
+#I #K #V #_ #H elim (ylt_yle_false … H) //
+qed.
+
+lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄.
+#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // *
+#I #K #V #H elim (ylt_yle_false … H) //
+qed.
+
+lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄.
+#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H //
+qed.
+
+lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
+ ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ →
+ ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄.
+#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H
+elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
+qed.
+
+lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ →
+ ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ →
+ ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄.
+#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H
+elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 //
+qed.
--- /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/relocation/cpy_lift.ma".
+include "basic_2/relocation/cny.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************)
+
+(* Properties on relocation *************************************************)
+
+lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12
+elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12
+>(HT1 … HT12) -K /2 width=5 by lift_mono/
+qed-.
+
+lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12
+elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2
+>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
+qed-.
+
+lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12
+elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2
+>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma cny_lift_inv_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdetd #T2 #HT12
+elim (lift_total T2 d e) #U2 #HTU2
+lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12
+lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
+qed-.
+
+lemma cny_lift_inv_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → dt ≤ d → yinj d + e ≤ dt + et → ⦃G, K⦄ ⊢ ▶[dt, et-e] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdtd #Hdedet #T2 #HT12
+lapply (yle_fwd_plus_ge_inj … Hdedet) // #Heet
+elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet
+elim (lift_total T2 d e) #U2 #HTU2
+lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete
+>ymax_pre_sn // -Heet #HU12
+lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
+qed-.
+
+lemma cny_lift_inv_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K →
+ ⇧[d, e] T ≡ U → yinj d + e ≤ dt → ⦃G, K⦄ ⊢ ▶[dt-e, et] 𝐍⦃T⦄.
+#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdedt #T2 #HT12
+elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #Hddte #Hedt
+elim (lift_total T2 d e) #U2 #HTU2
+lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte
+>ymax_pre_sn // -Hedt #HU12
+lapply (HU1 … HU12) -L /2 width=5 by lift_inj/
+qed-.
[ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ]
}
]
+ [ { "normal forms for context-sensitive extended substitution" * } {
+ [ "cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )" "cny_lift" * ]
+ }
+ ]
[ { "contxt-sensitive extended multiple substitution" * } {
[ "cpys ( ⦃?,?⦄ ⊢ ? ▶*×[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*×[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
}
projects / helm.git / commitdiff