(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
definition CP1 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L,k. NF … (RR L) RS (⋆k).
+ ∀L. ∃k. NF … (RR L) RS (⋆k).
definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L,K,W,i. ⇩[0,i] L ≡ K. ⓛW → NF … (RR L) RS (#i).
-
-definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term.
- ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
-
-definition CP4 ≝ λRR:lenv→relation term. λRS:relation term.
∀L0,L,T,T0,d,e. NF … (RR L) RS T →
⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0.
-definition CP4s ≝ λRR:lenv→relation term. λRS:relation term.
+definition CP2s ≝ λRR:lenv→relation term. λRS:relation term.
∀L0,L,des. ⇩*[des] L0 ≡ L →
∀T,T0. ⇧*[des] T ≡ T0 →
NF … (RR L) RS T → NF … (RR L0) RS T0.
+definition CP3 ≝ λRP:lenv→predicate term.
+ ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
+
(* requirements for abstract computation properties *)
record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝
{ cp1: CP1 RR RS;
cp2: CP2 RR RS;
- cp3: CP3 RR RP;
- cp4: CP4 RR RS
+ cp3: CP3 RP
}.
(* Basic properties *********************************************************)
(* Basic_1: was: nf2_lift1 *)
-lemma acp_lifts: ∀RR,RS. CP4 RR RS → CP4s RR RS.
+lemma acp_lifts: ∀RR,RS. CP2 RR RS → CP2s RR RS.
#RR #RS #HRR #L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
<(lifts_inv_nil … H) -H //
[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom
- @(s2 … HAtom … ◊) // /2 width=2/
+ @(s4 … HAtom … ◊) //
| #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
lapply (aacr_acr … H1RP H2RP B) #HB
elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
elim (lsubc_ldrop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
elim (lsubc_inv_pair2 … H) -H *
[ #K2 #HK20 #H destruct
- generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2
- [ elim (lift_total V0 0 (i0 +1)) #V #HV0
- elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
- @(s4 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *)
- | @(s2 … HB … ◊) // /2 width=3/
- ]
+ elim (lift_total V0 0 (i0 +1)) #V #HV0
+ elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
+ @(s5 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *)
| -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
#K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct
lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b
lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
>(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B
elim (lift_total V2 0 (i0 +1)) #V #HV2
- @(s4 … HB … ◊ … HV2 HLK2)
- @(s7 … HB … HKV2B) //
+ @(s5 … HB … ◊ … HV2 HLK2)
+ @(s8 … HB … HKV2B) //
]
| #a #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
lapply (aacr_acr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
- @(s5 … HA … ◊ ◊) // /3 width=5/
+ @(s6 … HA … ◊ ◊) // /3 width=5/
| #a #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@(aacr_abst … H1RP H2RP)
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
lapply (s1 … HA) #H
- @(s6 … HA … ◊) /2 width=5/ /3 width=5/
+ @(s7 … HA … ◊) /2 width=5/ /3 width=5/
]
qed.
definition S3 ≝ λRP,C:lenv→predicate term.
∀a,L,Vs,V,T,W. C L (ⒶVs. ⓓ{a}V. T) → RP L W → C L (ⒶVs. ⓐV. ⓛ{a}W. T).
-definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i.
+definition S4 ≝ λRP,C:lenv→predicate term.
+ ∀L,Vs. all … (RP L) Vs → ∀k. C L (ⒶVs.⋆k).
+
+definition S5 ≝ λRP,C:lenv→predicate term. ∀I,L,K,Vs,V1,V2,i.
C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 →
- â\87©[0, i] L â\89¡ K. â\93\93V1 → C L (Ⓐ Vs. #i).
+ â\87©[0, i] L â\89¡ K. â\93\91{I}V1 → C L (Ⓐ Vs. #i).
-definition S5 ≝ λRP,C:lenv→predicate term.
+definition S6 ≝ λRP,C:lenv→predicate term.
∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀a,V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓ{a}V. T).
-definition S6 ≝ λRP,C:lenv→predicate term.
+definition S7 ≝ λRP,C:lenv→predicate term.
∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T).
-definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
+definition S8 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
-definition S7s ≝ λC:lenv→predicate term.
+definition S8s ≝ λC:lenv→predicate term.
∀L1,L2,des. ⇩*[des] L2 ≡ L1 →
∀T1,T2. ⇧*[des] T1 ≡ T2 → C L1 T1 → C L2 T2.
s4: S4 RP C;
s5: S5 RP C;
s6: S6 RP C;
- s7: S7 C
+ s7: S7 RP C;
+ s8: S8 C
}.
(* the abstract candidate of reducibility associated to an atomic arity *)
(* Basic properties *********************************************************)
(* Basic_1: was: sc3_lift1 *)
-lemma acr_lifts: ∀C. S7 C → S7s C.
+lemma acr_lifts: ∀C. S8 C → S8s C.
#C #HC #L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
<(lifts_inv_nil … H) -H //
RP L V → RP L0 V0.
#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV
@acr_lifts /width=6/
-@(s7 … HRP)
+@(s8 … HRP)
qed.
(* Basic_1: was only: sns3_lifts1 *)
#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
#B #A #IHB #IHA @mk_acr normalize
[ #L #T #H
- lapply (H ? (⋆0) ? ⟠ ? ? ?) -H
+ elim (cp1 … H1RP L) #k #HK
+ lapply (H ? (⋆k) ? ⟠ ? ? ?) -H
[1,3: // |2,4: skip
- | @(s2 … IHB … ◊) // /2 width=2/
- | #H @(cp3 … H1RP … 0) @(s1 … IHA) //
+ | @(s2 … IHB … ◊) //
+ | #H @(cp3 … H1RP … k) @(s1 … IHA) //
]
| #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
@(s3 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /4 width=5/
-| #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
+| #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ >(lifts_inv_sort1 … HY) -Y
+ lapply (s1 … IHB … HB) #HV0
+ @(s4 … IHA … (V0 @ V0s)) /3 width=6/
+| #I #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
elim (ldrops_ldrop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
- @(s4 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/
+ @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/
| #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
- @(s5 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/
+ @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /2 width=6 by rp_lifts/
@(HA … (des + 1)) /2 width=1/
- [ @(s7 … IHB … HB … HV120) /2 width=1/
+ [ @(s8 … IHB … HB … HV120) /2 width=1/
| @lifts_applv //
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
>(liftv_mono … HV12s … HV10s) -V1s //
| #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
- @(s6 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/
+ @(s7 … IHA … (V0 @ V0s)) /2 width=6 by rp_lifts/ /3 width=4/
| /3 width=7/
]
qed.
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
lapply (s1 … HCB) -HCB #HCB
@(s3 … HCA … ◊) /2 width=6 by rp_lifts/
-@(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/
+@(s6 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/
qed.
(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
(* *)
(**************************************************************************)
-include "basic_2/reduction/cnf.ma".
+include "basic_2/reduction/cnr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
qed-.
(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U.
+lemma cprs_inv_cnr1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U.
#L #T #U #H @(cprs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
+++ /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/reduction/lpx_aaa.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A.
-#L #T1 #A #HT1 #T2 #HT12
-@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=3 by aaa_cpr_conf/
-qed-.
elim (cpss_conf … HU1 … HUT1) -U1 #U1 #HU1 #HTU1
lapply (cpss_trans … HU2 … HU1) -U
lapply (cprs_cpss_trans … HT21 … HTU1) -T1 /2 width=3/
-qed-.
\ No newline at end of file
+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/grammar/tstc.ma".
-include "basic_2/computation/lprs_cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Forward lemmas involving same top term constructor ***********************)
-
-lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → ∀U. L ⊢ T ➡* U → T ≃ U.
-#L #T #HT #U #H
->(cprs_inv_cnf1 … H HT) -L -T //
-qed-.
-
-(* Basic_1: was: pr3_iso_beta *)
-lemma cprs_fwd_beta: ∀a,L,V,W,T,U. L ⊢ ⓐV. ⓛ{a}W. T ➡* U →
- ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⓓ{a}V. T ➡* U.
-#a #L #V #W #T #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W0 #T0 #HV0 #HT0 #HU
- elim (cprs_fwd_abst1 … HT0 Abbr V) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1
- @or_intror -W
- @(cprs_trans … HU) -U /2 width=1/ (**) (* explicit constructor *)
-| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
- elim (cprs_fwd_abst1 … HT1 Abbr V) -HT1 #W2 #T2 #_ #_ #H destruct
-]
-qed-.
-
-(* Note: probably this is an inversion lemma *)
-lemma cprs_fwd_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
- ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- ∀U. L ⊢ #i ➡* U →
- #i ≃ U ∨ L ⊢ V2 ➡* U.
-#L #K #V1 #i #HLK #V2 #HV12 #U #H
-elim (cprs_inv_lref1 … H) -H /2 width=1/
-* #K0 #V0 #U0 #HLK0 #HVU0 #HU0
-lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
-lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
-qed-.
-
-lemma cprs_fwd_theta: ∀a,L,V1,V,T,U. L ⊢ ⓐV1. ⓓ{a}V. T ➡* U →
- ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓ{a}V. T ≃ U ∨
- L ⊢ ⓓ{a}V. ⓐV2. T ➡* U.
-#a #L #V1 #V #T #U #H #V2 #HV12
-elim (cprs_inv_appl1 … H) -H *
-[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W #T0 #HV10 #HT0 #HU
- elim (cprs_inv_abbr1 … HT0) -HT0 *
- [ #V3 #T3 #_ #_ #H destruct
- | #X #HT2 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
- @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *)
- @(cprs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T
- @(cprs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2
- @(cprs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/
- ]
-| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
- @or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *)
- elim (cprs_inv_abbr1 … HT0) -HT0 *
- [ #V5 #T5 #HV5 #HT5 #H destruct
- lapply (cprs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/
- /3 width=1/
- | #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- lapply (cprs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24
- @(cprs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T
- @(cprs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5
- @(cprs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
- ]
-]
-qed-.
-
-lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓝW. T ➡* U →
- ⓝW. T ≃ U ∨ L ⊢ T ➡* U.
-#L #W #T #U #H
-elim (cprs_inv_cast1 … H) -H /2 width=1/ *
-#W0 #T0 #_ #_ #H destruct /2 width=1/
-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/grammar/tstc_vector.ma".
-include "basic_2/relocation/lift_vector.ma".
-include "basic_2/computation/cprs_tstc.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Vector form of forward lemmas involving same top term constructor ********)
-
-(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cprs_fwd_cnf_vector: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ∀Vs,U. L ⊢ ⒶVs.T ➡* U → ⒶVs.T ≃ U.
-#L #T #H1T #H2T #Vs elim Vs -Vs [ @(cprs_fwd_cnf … H2T) ] (**) (* /2 width=3 by cprs_fwd_cnf/ does not work *)
-#V #Vs #IHVs #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #a #V0 #W0 #T0 #HV0 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (tstc_inv_bind_appls_simple … HT0 ?) //
-| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (tstc_inv_bind_appls_simple … HT0 ?) //
-]
-qed-.
-
-(* Basic_1: was: pr3_iso_appls_beta *)
-lemma cprs_fwd_beta_vector: ∀a,L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛ{a}W. T ➡* U →
- ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⒶVs. ⓓ{a}V. T ➡* U.
-#a #L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_beta/
-#V0 #Vs #IHVs #V #W #T #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
-| #b #V1 #W1 #T1 #HV01 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (tstc_inv_bind_appls_simple … HT1 ?) //
- | @or_intror -W (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- @(cprs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/
- ]
-| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (tstc_inv_bind_appls_simple … HT1 ?) //
- | @or_intror -W (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- @(cprs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/
- ]
-]
-qed-.
-
-lemma cprs_fwd_delta_vector: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
- ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- ∀Vs,U. L ⊢ ⒶVs.#i ➡* U →
- ⒶVs.#i ≃ U ∨ L ⊢ ⒶVs.V2 ➡* U.
-#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=4 by cprs_fwd_delta/
-#V #Vs #IHVs #U #H -K -V1
-elim (cprs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W0 #T0 #HV0 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
- | @or_intror -i (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- @(cprs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/
- ]
-| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
- | @or_intror -i (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- @(cprs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/
- ]
-]
-qed-.
-
-(* Basic_1: was: pr3_iso_appls_abbr *)
-lemma cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀a,V,T,U. L ⊢ ⒶV1s. ⓓ{a}V. T ➡* U →
- ⒶV1s. ⓓ{a}V. T ≃ U ∨ L ⊢ ⓓ{a}V. ⒶV2s. T ➡* U.
-#L #V1s #V2s * -V1s -V2s /3 width=1/
-#V1s #V2s #V1a #V2a #HV12a #HV12s #a
-generalize in match HV12a; -HV12a
-generalize in match V2a; -V2a
-generalize in match V1a; -V1a
-elim HV12s -V1s -V2s /2 width=1 by cprs_fwd_theta/
-#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0a #W0 #T0 #HV10a #HT0 #HU
- elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0
- [ -HV12a -HV12b -HV10a -HU
- elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
- | @or_intror -V1s (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- elim (cprs_inv_abbr1 … HT0) -HT0 *
- [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct
- | -V1b #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
- @(cprs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cprs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1
- @(cprs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/
- ]
- ]
-| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
- elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0
- [ -HV12a -HV10a -HV0a -HU
- elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
- | @or_intror -V1s -V1b (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- elim (cprs_inv_abbr1 … HT0) -HT0 *
- [ #V1 #T1 #HV1 #HT1 #H destruct
- lapply (cprs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
- @(cprs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/
- | #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
- lapply (cprs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a
- @(cprs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cprs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1
- @(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
- ]
- ]
-]
-qed-.
-
-(* Basic_1: was: pr3_iso_appls_cast *)
-lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓝW. T ➡* U →
- ⒶVs. ⓝW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U.
-#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/
-#V #Vs #IHVs #W #T #U #H
-elim (cprs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #V0 #W0 #T0 #HV0 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
- | @or_intror -W (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- @(cprs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/
- ]
-| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
- | @or_intror -W (**) (* explicit constructor *)
- @(cprs_trans … HU) -U
- @(cprs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/reduction/cpx.ma".
+include "basic_2/reduction/cnx.ma".
include "basic_2/computation/cprs.ma".
-(* EXTENDED CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS *****************)
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
definition cpxs: ∀h. sd h → lenv → relation term ≝
λh,g. LTC … (cpx h g).
elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ *
#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
qed-.
+
+lemma cpxs_inv_cnx1: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T ➡*[g] U → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → T = U.
+#h #g #L #T #U #H @(cpxs_ind_dx … H) -T //
+#T0 #T #H1T0 #_ #IHT #H2T0
+lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
+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/reduction/lpx_aaa.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_cpxs_conf: ∀h,g,L,T1,A. L ⊢ T1 ⁝ A →
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → L ⊢ T2 ⁝ A.
+#h #g #L #T1 #A #HT1 #T2 #HT12
+@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by aaa_cpx_conf/
+qed-.
+
+lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A.
+/3 width=5 by aaa_cpxs_conf, cprs_cpxs/ 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/reduction/lpx_ldrop.ma".
+include "basic_2/computation/cpxs_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Main properties **********************************************************)
+
+theorem cpxs_trans: ∀h,g,L. Transitive … (cpxs h g L).
+#h #g #L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+
+theorem cpxs_bind: ∀h,g,a,I,L,V1,V2,T1,T2. ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 →
+ ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+ ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
+#h #g #a #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cpxs_trans … IHV1) -V1 /2 width=1/
+qed.
+
+theorem cpxs_flat: ∀h,g,I,L,V1,V2,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 →
+ ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+ ⦃h, L⦄ ⊢ ⓕ{I} V1.T1 ➡*[g] ⓕ{I} V2.T2.
+#h #g #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cpxs_trans … IHV1) -IHV1 /2 width=1/
+qed.
+
+theorem cpxs_beta: ∀h,g,a,L,V1,V2,W,T1,T2.
+ ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2.
+#h #g #a #L #V1 #V2 #W #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cpxs_trans … IHV1) /2 width=1/
+qed.
+
+theorem cpxs_theta_rc: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 →
+ ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
+#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
+#W #W2 #_ #HW2 #IHW1
+@(cpxs_trans … IHW1) /2 width=1/
+qed.
+
+theorem cpxs_theta: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
+ ⇧[0, 1] V ≡ V2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
+ ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ V1 ➡*[g] V →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
+#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
+#V1 #V0 #HV10 #_ #IHV0
+@(cpxs_trans … IHV0) /2 width=1/
+qed.
+
+(* Properties on sn extended parallel reduction for local environments ******)
+
+lemma lpx_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpx h g).
+#h #g #L2 #T1 #T2 #HT12 elim HT12 -L2 -T1 -T2
+[ /2 width=3/
+| /3 width=2/
+| #I #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
+ elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
+ lapply (IHV02 … HK12) -K2 #HV02
+ lapply (cpxs_strap2 … HV10 … HV02) -V0 /2 width=7/
+| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/
+|5,7: /3 width=1/
+| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
+ lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/
+| #a #L2 #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓛW) ?) -IHT12 /2 width=1/ /3 width=1/
+| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/
+]
+qed-.
+
+lemma cpx_bind2: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+ ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡[g] T2 →
+ ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
+#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lapply (lpx_cpx_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
+qed.
+
+(* Advanced properties ******************************************************)
+
+lemma lpx_cpxs_trans: ∀h,g. s_rs_trans … (cpx h g) (lpx h g).
+/3 width=5 by s_r_trans_TC1, lpx_cpx_trans/ qed-.
+
+lemma cpxs_bind2_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+ ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[g] T2 →
+ ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
+#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lapply (lpx_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
+qed.
(* *)
(**************************************************************************)
+include "basic_2/substitution/fsups_fsups.ma".
include "basic_2/reduction/cpx_lift.ma".
include "basic_2/computation/cpxs.ma".
(* Relocation properties ****************************************************)
-(* Basic_1: was: pr3_lift *)
lemma cpxs_lift: ∀h,g. l_liftable (cpxs h g).
/3 width=9/ qed.
-(* Basic_1: was: pr3_gen_lift *)
lemma cpxs_inv_lift1: ∀h,g. l_deliftable_sn (cpxs h g).
/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/
qed-.
(* Properties on supclosure *************************************************)
-include "basic_2/substitution/fsups.ma".
-
lemma fsupq_cpxs_trans: ∀h,g,L1,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 →
∀T1. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
elim (IHTU2 … HT2) -T2 /3 width=3/
qed-.
+lemma fsups_cpxs_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃* ⦃L2, T2⦄ →
+ ∀U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 [ /2 width=3/ ]
+#L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
+elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
+elim (IHT1 … HT2) -T #T #HT1 #HT2
+lapply (fsups_trans … HT2 … HTU2) -L -T2 /2 width=3/
+qed-.
+
lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
--- /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/grammar/tstc.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Forward lemmas involving same top term constructor ***********************)
+
+lemma cpxs_fwd_cnx: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ∀U. ⦃h, L⦄ ⊢ T ➡*[g] U → T ≃ U.
+#h #g #L #T #HT #U #H
+>(cpxs_inv_cnx1 … H HT) -L -T //
+qed-.
+
+(* Basic_1: was just: pr3_iso_beta *)
+lemma cpxs_fwd_beta: ∀h,g,a,L,V,W,T,U. ⦃h, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[g] U →
+ ⓐV.ⓛ{a}W.T ≃ U ∨
+ ∃∃T0. ⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⓓ{a}V.T0 ➡*[g] U.
+#h #g #a #L #V #W #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #b #V0 #W0 #T0 #HV0 #HT0 #HU
+ elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1
+ @or_intror @(ex2_intro … HT1) -W (**) (* explicit constructors *)
+ @(cpxs_trans … HU) -U /2 width=1/
+| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
+ elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
+]
+qed-.
+
+(* Note: probably this is an inversion lemma *)
+lemma cpxs_fwd_delta: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+ ∀U. ⦃h, L⦄ ⊢ #i ➡*[g] U →
+ #i ≃ U ∨ ⦃h, L⦄ ⊢ V2 ➡*[g] U.
+#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #U #H
+elim (cpxs_inv_lref1 … H) -H /2 width=1/
+* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
+lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
+qed-.
+
+lemma cpxs_fwd_theta: ∀h,g,a,L,V1,V,T,U. ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[g] U →
+ ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≃ U ∨
+ ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U.
+#h #g #a #L #V1 #V #T #U #H #V2 #HV12
+elim (cpxs_inv_appl1 … H) -H *
+[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #b #V0 #W #T0 #HV10 #HT0 #HU
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ #V3 #T3 #_ #_ #H destruct
+ | #X #HT2 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
+ @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [ /5 width=7/ ] -V -V2 -W2 -T2
+ @(cpxs_strap2 … (ⓓ{b}V1.T0)) [ /3 width=1/ ] -W /2 width=1/
+ ]
+| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
+ @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ #V5 #T5 #HV5 #HT5 #H destruct
+ lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/
+ /3 width=1/
+ | #X #HT1 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
+ lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
+ ]
+]
+qed-.
+
+lemma cpxs_fwd_tau: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U →
+ ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ T ➡*[g] U.
+#h #g #L #W #T #U #H
+elim (cpxs_inv_cast1 … H) -H /2 width=1/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1/
+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/grammar/tstc_vector.ma".
+include "basic_2/relocation/lift_vector.ma".
+include "basic_2/computation/cpxs_tstc.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Vector form of forward lemmas involving same top term constructor ********)
+
+(* Basic_1: was just: nf2_iso_appls_lref *)
+lemma cpxs_fwd_cnx_vector: ∀h,g,L,T. 𝐒⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ →
+ ∀Vs,U. ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U → ⒶVs.T ≃ U.
+#h #g #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
+#V #Vs #IHVs #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #a #V0 #W0 #T0 #HV0 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (tstc_inv_bind_appls_simple … HT0) //
+| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (tstc_inv_bind_appls_simple … HT0) //
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_beta *)
+lemma cpxs_fwd_beta_vector: ∀h,g,a,L,Vs,V,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[g] U →
+ ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨
+ ∃∃T0.⦃h, L.ⓛW⦄ ⊢ T ➡*[g] T0 & ⦃h, L⦄ ⊢ ⒶVs.ⓓ{a}V.T0 ➡*[g] U.
+#h #g #a #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
+#V0 #Vs #IHVs #V #W #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
+| #b #V1 #W1 #T1 #HV01 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1
+ [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) //
+ | * #T0 #HT0 #HT01
+ @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV1.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=1/
+ ]
+| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1
+ [ #HT1 elim (tstc_inv_bind_appls_simple … HT1) //
+ | * #T0 #HT0 #HT01
+ @or_intror @(ex2_intro … HT0) -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/
+ ]
+]
+qed-.
+
+lemma cpxs_fwd_delta_vector: ∀h,g,I,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+ ∀Vs,U. ⦃h, L⦄ ⊢ ⒶVs.#i ➡*[g] U →
+ ⒶVs.#i ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.V2 ➡*[g] U.
+#h #g #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
+#V #Vs #IHVs #U #H -K -V1
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #b #V0 #W0 #T0 #HV0 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tstc_inv_bind_appls_simple … HT0) //
+ | @or_intror -i (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/
+ ]
+| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tstc_inv_bind_appls_simple … HT0) //
+ | @or_intror -i (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_abbr *)
+lemma cpxs_fwd_theta_vector: ∀h,g,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀a,V,T,U. ⦃h, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[g] U →
+ ⒶV1s. ⓓ{a}V. T ≃ U ∨ ⦃h, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[g] U.
+#h #g #L #V1s #V2s * -V1s -V2s /3 width=1/
+#V1s #V2s #V1a #V2a #HV12a #HV12s #a
+generalize in match HV12a; -HV12a
+generalize in match V2a; -V2a
+generalize in match V1a; -V1a
+elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/
+#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #b #V0a #W0 #T0 #HV10a #HT0 #HU
+ elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0
+ [ -HV12a -HV12b -HV10a -HU
+ elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
+ | @or_intror -V1s (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ -HV12a -HV12b -HV10a #V1 #T1 #_ #_ #H destruct
+ | -V1b #X #HT1 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s
+ @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [ /5 width=7/ ] -V -V2a -W1 -T1
+ @(cpxs_strap2 … (ⓓ{b}V1a.T0)) [ /3 width=1/ ] -W0 /2 width=1/
+ ]
+ ]
+| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
+ elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0
+ [ -HV12a -HV10a -HV0a -HU
+ elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
+ | @or_intror -V1s -V1b (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ #V1 #T1 #HV1 #HT1 #H destruct
+ lapply (cpxs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
+ @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/
+ | #X #HT1 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
+ lapply (cpxs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s
+ @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
+ ]
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_cast *)
+lemma cpxs_fwd_tau_vector: ∀h,g,L,Vs,W,T,U. ⦃h, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[g] U →
+ ⒶVs. ⓝW. T ≃ U ∨ ⦃h, L⦄ ⊢ ⒶVs.T ➡*[g] U.
+#h #g #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_tau/
+#V #Vs #IHVs #W #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #b #V0 #W0 #T0 #HV0 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tstc_inv_bind_appls_simple … HT0) //
+ | @or_intror -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=1/
+ ]
+| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tstc_inv_bind_appls_simple … HT0) //
+ | @or_intror -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /3 width=3/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/reduction/cnf.ma".
+include "basic_2/reduction/cnx.ma".
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-definition csn: lenv → predicate term ≝ λL. SN … (cpr L) (eq …).
+definition csn: ∀h. sd h → lenv → predicate term ≝
+ λh,g,L. SN … (cpx h g L) (eq …).
interpretation
- "context-sensitive strong normalization (term)"
- 'SN L T = (csn L T).
+ "context-sensitive extended strong normalization (term)"
+ 'SN h g L T = (csn h g L T).
(* Basic eliminators ********************************************************)
-lemma csn_ind: ∀L. ∀R:predicate term.
- (∀T1. L ⊢ ⬊* T1 →
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → R T2) →
+lemma csn_ind: ∀h,g,L. ∀R:predicate term.
+ (∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → R T2) →
R T1
) →
- ∀T. L ⊢ ⬊* T → R T.
-#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
+ ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → R T.
+#h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
qed-.
(* Basic properties *********************************************************)
-(* Basic_1: was: sn3_pr2_intro *)
-lemma csn_intro: ∀L,T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* T2) → L ⊢ ⬊* T1.
+(* Basic_1: was just: sn3_pr2_intro *)
+lemma csn_intro: ∀h,g,L,T1.
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] T2) →
+ ⦃h, L⦄ ⊢ ⬊*[g] T1.
/4 width=1/ qed.
-(* Basic_1: was: sn3_nf2 *)
-lemma csn_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ ⬊* T.
+(* Basic_1: was just: sn3_nf2 *)
+lemma cnx_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ ⬊*[g] T.
/2 width=1/ qed.
-lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ ⬊* T2.
-#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
+lemma csn_cpx_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2.
+#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csn_intro #T #HLT2 #HT2
elim (term_eq_dec T1 T2) #HT12
[ -IHT1 -HLT12 destruct /3 width=1/
| -HT1 -HT2 /3 width=4/
qed-.
-(* Basic_1: was: sn3_cast *)
-lemma csn_cast: ∀L,W. L ⊢ ⬊* W → ∀T. L ⊢ ⬊* T → L ⊢ ⬊* ⓝW. T.
-#L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
+(* Basic_1: was just: sn3_cast *)
+lemma csn_cast: ∀h,g,L,W. ⦃h, L⦄ ⊢ ⬊*[g] W →
+ ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓝW.T.
+#h #g #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
-elim (cpr_inv_cast1 … H1) -H1
+elim (cpx_inv_cast1 … H1) -H1
[ * #W0 #T0 #HLW0 #HLT0 #H destruct
elim (eq_false_inv_tpair_sn … H2) -H2
- [ /3 width=3 by csn_cpr_trans/
+ [ /3 width=3 by csn_cpx_trans/
| -HLW0 * #H destruct /3 width=1/
]
-| /3 width=3 by csn_cpr_trans/
+| /3 width=3 by csn_cpx_trans/
]
qed.
(* Basic forward lemmas *****************************************************)
-fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V.
-#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+fact csn_fwd_pair_sn_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U →
+ ∀I,V,T. U = ②{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] V.
+#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #V2 #HLV2 #HV2
-@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
+@(IH (②{I}V2.T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
qed-.
-(* Basic_1: was: sn3_gen_head *)
-lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V.
+(* Basic_1: was just: sn3_gen_head *)
+lemma csn_fwd_pair_sn: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ②{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] V.
/2 width=5 by csn_fwd_pair_sn_aux/ qed-.
-fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U →
- ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
-#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
+fact csn_fwd_bind_dx_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U →
+ ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[g] T.
+#h #g #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
qed-.
-(* Basic_1: was: sn3_gen_bind *)
-lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
+(* Basic_1: was just: sn3_gen_bind *)
+lemma csn_fwd_bind_dx: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓑ{a,I}V.T → ⦃h, L.ⓑ{I}V⦄ ⊢ ⬊*[g] T.
/2 width=4 by csn_fwd_bind_dx_aux/ qed-.
-fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬊* T.
-#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+fact csn_fwd_flat_dx_aux: ∀h,g,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U →
+ ∀I,V,T. U = ⓕ{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] T.
+#h #g #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
-@(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
-qed.
+@(IH (ⓕ{I}V.T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+qed-.
-(* Basic_1: was: sn3_gen_flat *)
-lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬊* ⓕ{I} V. T → L ⊢ ⬊* T.
-/2 width=5/ qed-.
+(* Basic_1: was just: sn3_gen_flat *)
+lemma csn_fwd_flat_dx: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓕ{I}V.T → ⦃h, L⦄ ⊢ ⬊*[g] T.
+/2 width=5 by csn_fwd_flat_dx_aux/ qed-.
(* Basic_1: removed theorems 14:
sn3_cdelta
(* *)
(**************************************************************************)
-include "basic_2/computation/cprs.ma".
+include "basic_2/computation/cpxs.ma".
include "basic_2/computation/csn.ma".
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* alternative definition of csn *)
-definition csna: lenv → predicate term ≝ λL. SN … (cprs L) (eq …).
+definition csna: ∀h. sd h → lenv → predicate term ≝
+ λh,g,L. SN … (cpxs h g L) (eq …).
interpretation
- "context-sensitive strong normalization (term) alternative"
- 'SNAlt L T = (csna L T).
+ "context-sensitive extended strong normalization (term) alternative"
+ 'SNAlt h g L T = (csna h g L T).
(* Basic eliminators ********************************************************)
-lemma csna_ind: ∀L. ∀R:predicate term.
- (∀T1. L ⊢ ⬊⬊* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1
+lemma csna_ind: ∀h,g,L. ∀R:predicate term.
+ (∀T1. ⦃h, L⦄ ⊢ ⬊⬊*[g] T1 →
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
- ∀T. L ⊢ ⬊⬊* T → R T.
-#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
+ ∀T. ⦃h, L⦄ ⊢ ⬊⬊*[g] T → R T.
+#h #g #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
qed-.
(* Basic properties *********************************************************)
-(* Basic_1: was: sn3_intro *)
-lemma csna_intro: ∀L,T1.
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → L ⊢ ⬊⬊* T1.
+(* Basic_1: was just: sn3_intro *)
+lemma csna_intro: ∀h,g,L,T1.
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2) →
+ ⦃h, L⦄ ⊢ ⬊⬊*[g] T1.
/4 width=1/ qed.
-fact csna_intro_aux: ∀L,T1.
- (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) → L ⊢ ⬊⬊* T1.
+fact csna_intro_aux: ∀h,g,L,T1. (
+ ∀T,T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → T1 = T → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2
+ ) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T1.
/4 width=3/ qed-.
-(* Basic_1: was: sn3_pr3_trans (old version) *)
-lemma csna_cprs_trans: ∀L,T1. L ⊢ ⬊⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊⬊* T2.
-#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
+(* Basic_1: was just: sn3_pr3_trans (old version) *)
+lemma csna_cpxs_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊⬊*[g] T1 →
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2.
+#h #g #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
@csna_intro #T #HLT2 #HT2
elim (term_eq_dec T1 T2) #HT12
[ -IHT1 -HLT12 destruct /3 width=1/
| -HT1 -HT2 /3 width=4/
qed.
-(* Basic_1: was: sn3_pr2_intro (old version) *)
-lemma csna_intro_cpr: ∀L,T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊⬊* T2) →
- L ⊢ ⬊⬊* T1.
-#L #T1 #H
-@csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T
+(* Basic_1: was just: sn3_pr2_intro (old version) *)
+lemma csna_intro_cpx: ∀h,g,L,T1. (
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T2
+ ) → ⦃h, L⦄ ⊢ ⬊⬊*[g] T1.
+#h #g #L #T1 #H
+@csna_intro_aux #T #T2 #H @(cpxs_ind_dx … H) -T
[ -H #H destruct #H
elim (H ?) //
| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
(* Main properties **********************************************************)
-theorem csn_csna: ∀L,T. L ⊢ ⬊* T → L ⊢ ⬊⬊* T.
-#L #T #H @(csn_ind … H) -T /4 width=1/
+theorem csn_csna: ∀h,g,L,T. ⦃h, L⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊⬊*[g] T.
+#h #g #L #T #H @(csn_ind … H) -T /4 width=1/
qed.
-theorem csna_csn: ∀L,T. L ⊢ ⬊⬊* T → L ⊢ ⬊* T.
-#L #T #H @(csna_ind … H) -T /4 width=1/
+theorem csna_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ ⬊⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] T.
+#h #g #L #T #H @(csna_ind … H) -T /4 width=1/
qed.
-(* Basic_1: was: sn3_pr3_trans *)
-lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬊* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬊* T2.
-#L #T1 #HT1 #T2 #H @(cprs_ind … H) -T2 // /2 width=3 by csn_cpr_trans/
+(* Basic_1: was just: sn3_pr3_trans *)
+lemma csn_cpxs_trans: ∀h,g,L,T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] T2.
+#h #g #L #T1 #HT1 #T2 #H @(cpxs_ind … H) -T2 // /2 width=3 by csn_cpx_trans/
qed-.
(* Main eliminators *********************************************************)
-lemma csn_ind_alt: ∀L. ∀R:predicate term.
- (∀T1. L ⊢ ⬊* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1
+lemma csn_ind_alt: ∀h,g,L. ∀R:predicate term.
+ (∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 = T2 → ⊥) → R T2) → R T1
) →
- ∀T. L ⊢ ⬊* T → R T.
-#L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
+ ∀T. ⦃h, L⦄ ⊢ ⬊*[g] T → R T.
+#h #g #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
@H0 -H0 /2 width=1/ -HT1 /3 width=1/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/reduction/cnf_lift.ma".
+include "basic_2/reduction/cnx_lift.ma".
include "basic_2/computation/acp.ma".
include "basic_2/computation/csn.ma".
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* Relocation properties ****************************************************)
-(* Basic_1: was: sn3_lift *)
-lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 →
- ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬊* T2.
-#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
+(* Basic_1: was just: sn3_lift *)
+lemma csn_lift: ∀h,g,L2,L1,T1,d,e. ⦃h, L1⦄ ⊢ ⬊*[g] T1 →
+ ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃h, L2⦄ ⊢ ⬊*[g] T2.
+#h #g #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
@csn_intro #T #HLT2 #HT2
-elim (cpr_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10
+elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/
qed.
-(* Basic_1: was: sn3_gen_lift *)
-lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬊* T1 →
- ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → L2 ⊢ ⬊* T2.
-#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
+(* Basic_1: was just: sn3_gen_lift *)
+lemma csn_inv_lift: ∀h,g,L2,L1,T1,d,e. ⦃h, L1⦄ ⊢ ⬊*[g] T1 →
+ ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃h, L2⦄ ⊢ ⬊*[g] T2.
+#h #g #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
@csn_intro #T #HLT2 #HT2
elim (lift_total T d e) #T0 #HT0
-lapply (cpr_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10
+lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/
qed.
(* Advanced properties ******************************************************)
-(* Basic_1: was: sn3_abbr *)
-lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬊* V → L ⊢ ⬊* #i.
-#L #K #V #i #HLK #HV
+(* Basic_1: was just: sn3_abbr *)
+lemma csn_lref_bind: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, K⦄ ⊢ ⬊*[g] V → ⦃h, L⦄ ⊢ ⬊*[g] #i.
+#h #g #I #L #K #V #i #HLK #HV
@csn_intro #X #H #Hi
-elim (cpr_inv_lref1 … H) -H
-[ #H destruct elim (Hi ?) //
-| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1
+elim (cpx_inv_lref1 … H) -H
+[ #H destruct elim Hi //
+| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct
lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK
@(csn_lift … HLK HV1) -HLK -HV1
- @(csn_cpr_trans … HV) -HV //
+ @(csn_cpx_trans … HV) -HV //
]
qed.
-lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛ{a}W. T.
-#a #L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT
+lemma csn_appl_simple: ∀h,g,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → ∀T1.
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → (T1 = T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T2) →
+ 𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1.
+#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
@csn_intro #X #H1 #H2
-elim (cpr_fwd_abst1 … H1 I V) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ /3 width=5 by csn_cpr_trans/
-| -HLW0 * #H destruct /3 width=1/
-]
-qed.
-
-lemma csn_appl_simple: ∀L,V. L ⊢ ⬊* V → ∀T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
- 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
-#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
-@csn_intro #X #H1 #H2
-elim (cpr_inv_appl1_simple … H1 ?) // -H1
+elim (cpx_inv_appl1_simple … H1) // -H1
#V0 #T0 #HLV0 #HLT10 #H destruct
elim (eq_false_inv_tpair_dx … H2) -H2
[ -IHV -HT1 #HT10
- @(csn_cpr_trans … (ⓐV.T0)) /2 width=1/ -HLV0
+ @(csn_cpx_trans … (ⓐV.T0)) /2 width=1/ -HLV0
@IHT1 -IHT1 // /2 width=1/
| -HLT10 * #H #HV0 destruct
@IHV -IHV // -HT1 /2 width=1/ -HV0
#T2 #HLT02 #HT02
- @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+ @(csn_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0
@IHT1 -IHT1 // -HLT02 /2 width=1/
]
qed.
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: sn3_gen_def *)
-lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬊* #i → K ⊢ ⬊* V.
-#L #K #V #i #HLK #Hi
+lemma csn_inv_lref_bind: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V →
+ ⦃h, L⦄ ⊢ ⬊*[g] #i → ⦃h, K⦄ ⊢ ⬊*[g] V.
+#h #g #I #L #K #V #i #HLK #Hi
elim (lift_total V 0 (i+1)) #V0 #HV0
lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
@(csn_inv_lift … H0LK … HV0) -H0LK
-@(csn_cpr_trans … Hi) -Hi /2 width=6/
+@(csn_cpx_trans … Hi) -Hi /2 width=7/
qed-.
(* Main properties **********************************************************)
-theorem csn_acp: acp cpr (eq …) (csn …).
-@mk_acp
-[ /2 width=1/
-| /2 width=3/
-| /2 width=5/
-| @cnf_lift
+theorem csn_acp: ∀h,g. acp (cpx h g) (eq …) (csn h g).
+#h #g @mk_acp
+[ #L elim (deg_total h g 0)
+ #l #Hl lapply (cnx_sort_iter … L … Hl) /2 width=2/
+| @cnx_lift
+| /2 width=3 by csn_fwd_flat_dx/
]
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/grammar/tstc_tstc.ma".
-include "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/csn_alt.ma".
-include "basic_2/computation/csn_lift.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma csn_lpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T.
-#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
-@csn_intro #T0 #HLT0 #HT0
-@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpr_cpr_trans/
-qed.
-
-lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T.
-#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
-@csn_intro #X #H1 #H2
-elim (cpr_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ #HV1 @IHV // /2 width=1/ -HV1
- @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpr_trans/
- | -IHV -HLV1 * #H destruct /3 width=1/
- ]
-| -IHV -IHT -H2 #T0 #HLT0 #HT0
- lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
- lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
-]
-qed.
-
-fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U →
- ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
-#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
-lapply (csn_fwd_pair_sn … HVT) #HV
-lapply (csn_fwd_bind_dx … HVT) #HT -HVT
-@csn_intro #X #H #H2
-elim (cpr_inv_appl1 … H) -H *
-[ #V0 #Y #HLV0 #H #H0 destruct
- elim (cpr_fwd_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- elim (eq_false_inv_beta … H2) -H2
- [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
- @csn_abbr /2 width=3 by csn_cpr_trans/ -HV
- @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/
- | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
- @(IHVT … HVT0) -IHVT -HVT0 // /3 width=1/
- ]
-| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
- lapply (cpr_lsubr_trans … HLT01 (L.ⓓV) ?) -HLT01 /2 width=1/ #HLT01
- @csn_abbr /2 width=3 by csn_cpr_trans/ -HV
- @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3 by csn_cpr_trans/
-| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was: sn3_beta *)
-lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T →
- L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
-/2 width=3 by csn_appl_beta_aux/ qed.
-
-fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
-#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csn_fwd_pair_sn … HVT) #HV
-lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
-@csn_intro #X #HL #H
-elim (cpr_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpr_inv_abbr1 … HL) -HL *
- [ #V3 #T3 #HV3 #HLT3 #H0 destruct
- elim (lift_total V0 0 1) #V4 #HV04
- elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
- [ -IHVT #H0 destruct
- elim (eq_false_inv_tpair_sn … H) -H
- [ -HLV10 -HV3 -HLT3 -HVT
- >(lift_inj … HV12 … HV04) -V4
- #H elim H //
- | * #_ #H elim H //
- ]
- | -H -HVT #H
- lapply (cpr_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24
- @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
- lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
- @(csn_cpr_trans … HVY) /2 width=1/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
- lapply (cpr_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
- @csn_abbr /2 width=3 by csn_cpr_trans/ -HV
- @(csn_lpr_conf (L. ⓓW0)) /2 width=1/ -W1
- @(csn_cprs_trans … HVT) -HVT /3 width=1/
-]
-qed-.
-
-lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
-/2 width=5 by csn_appl_theta_aux/ qed.
-
-(* Basic_1: was only: sn3_appl_appl *)
-lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1.
- L ⊢ ⬊* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
- 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
-#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csn_intro #X #HL #H
-elim (cpr_inv_appl1_simple … HL ?) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (eq_false_inv_tpair_sn … H) -H
-[ -IHT1 #HV0
- @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
- @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
- #T2 #HLT12 #HT12
- @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
- @H2T1 -H2T1 // -HLT12 /2 width=1/
-| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
- elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
- #T2 #HLT02 #HT02
- @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
- | -IHT1 -H3T1 -H1T10
- @H2T1 -H2T1 /2 width=1/
- ]
-]
-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/grammar/tstc_tstc.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
+include "basic_2/computation/csn_alt.ma".
+include "basic_2/computation/csn_lift.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Advanced properties ******************************************************)
+
+lemma csn_lpx_conf: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 →
+ ∀T. ⦃h, L1⦄ ⊢ ⬊*[g] T → ⦃h, L2⦄ ⊢ ⬊*[g] T.
+#h #g #L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
+@csn_intro #T0 #HLT0 #HT0
+@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpx_cpx_trans/
+qed.
+
+lemma csn_abst: ∀h,g,a,L,W. ⦃h, L⦄ ⊢ ⬊*[g] W →
+ ∀T. ⦃h, L.ⓛW⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓛ{a}W.T.
+#h #g #a #L #W #HW @(csn_ind … HW) -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT
+@csn_intro #X #H1 #H2
+elim (cpx_inv_abst1 … H1) -H1
+#W0 #T0 #HLW0 #HLT0 #H destruct
+elim (eq_false_inv_tpair_sn … H2) -H2
+[ -IHT #H lapply (csn_cpx_trans … HLT0) // -HT
+ #HT0 lapply (csn_lpx_conf … (L.ⓛW0) … HT0) -HT0 /2 width=1/ /3 width=1/
+| -IHW -HLW0 -HT * #H destruct /3 width=1/
+]
+qed.
+
+lemma csn_abbr: ∀h,g,a,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V →
+ ∀T. ⦃h, L.ⓓV⦄ ⊢ ⬊*[g] T → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V. T.
+#h #g #a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
+@csn_intro #X #H1 #H2
+elim (cpx_inv_abbr1 … H1) -H1 *
+[ #V1 #T1 #HLV1 #HLT1 #H destruct
+ elim (eq_false_inv_tpair_sn … H2) -H2
+ [ #HV1 @IHV // /2 width=1/ -HV1
+ @(csn_lpx_conf … (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csn_cpx_trans/
+ | -IHV -HLV1 * #H destruct /3 width=1/
+ ]
+| -IHV -IHT -H2 #T0 #HLT0 #HT0
+ lapply (csn_cpx_trans … HT … HLT0) -T #HLT0
+ lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
+]
+qed.
+
+fact csn_appl_beta_aux: ∀h,g,a,L,U1. ⦃h, L⦄ ⊢ ⬊*[g] U1 → ∀V. ⦃h, L⦄ ⊢ ⬊*[g] V →
+ ∀W,T1. U1 = ⓛ{a}W.T1 → (
+ ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2
+ ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1.
+#h #g #a #L #X1 #H @(csn_ind … H) -X1
+#X1 #HT1 #IHT1 #X2 #H @(csn_ind … H) -X2
+#V #HV #IHV #W #T1 #H1 #IHT2 destruct
+@csn_intro #X #H1 #H2
+elim (cpx_inv_appl1 … H1) -H1 *
+[ #V0 #Y #HLV0 #H #H0 destruct
+ elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+ elim (eq_false_inv_tpair_dx … H2) -H2
+ [ lapply (csn_cpx_trans … HV … HLV0) -HV #HV0 #HWT0
+ @IHT1 -IHT1 [4,5: // |1: skip |2,3: /2 width=1/ ] -HWT0 -HV0 #T2 #HT02
+ lapply (lpx_cpxs_trans … HT02 (L.ⓛW) ?) [ /2 width=1/ ] -W0 #HT02
+ lapply (cpxs_strap2 … HLT0 … HT02) -T0 #HT12
+ lapply (IHT2 … HT12) -T1 #HT2
+ @(csn_cpx_trans … HT2) -HT2 /2 width=1/
+ | -HV -HT1 -IHT1 -HLW0 -HLT0 * #H #HV0 destruct
+ @IHV -IHV [1,3: // |2: /2 width=1/ ] -HV0 #T2 #HT02
+ lapply (IHT2 … HT02) -IHT2 -HT02 #HT2
+ @(csn_cpx_trans … HT2) -HT2 /2 width=1/
+ ]
+| -HT1 -IHT1 -HV -IHV -H2 #b #V0 #W0 #T0 #T3 #HLV0 #HLT01 #H1 #H2 destruct
+ lapply (IHT2 T3 ?) [ /2 width=1/ ] -IHT2 -HLT01 #HT3
+ @(csn_cpx_trans … HT3) -HT3 /2 width=1/
+| -HT1 -IHT1 -HV -IHV -IHT2 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was just: sn3_beta *)
+lemma csn_appl_beta: ∀h,g,a,L,W,T1. ⦃h, L⦄ ⊢ ⬊*[g] ⓛ{a}W.T1 → ∀V. (
+ ∀T2. ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.T2
+ ) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.ⓛ{a}W.T1.
+#h #g #a #L #W #T1 #HWT1 #V #IHT2 lapply (IHT2 T1 ?) //
+#HVT1 lapply (csn_fwd_pair_sn … HVT1) -HVT1
+/3 width=3 by csn_appl_beta_aux/ qed.
+
+fact csn_appl_theta_aux: ∀h,g,a,L,U. ⦃h, L⦄ ⊢ ⬊*[g] U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV1.ⓓ{a}V.T.
+#h #g #a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csn_fwd_pair_sn … HVT) #HV
+lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
+@csn_intro #X #HL #H
+elim (cpx_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+ elim (cpx_inv_abbr1 … HL) -HL *
+ [ #V3 #T3 #HV3 #HLT3 #H0 destruct
+ elim (lift_total V0 0 1) #V4 #HV04
+ elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
+ [ -IHVT #H0 destruct
+ elim (eq_false_inv_tpair_sn … H) -H
+ [ -HLV10 -HV3 -HLT3 -HVT
+ >(lift_inj … HV12 … HV04) -V4
+ #H elim H //
+ | * #_ #H elim H //
+ ]
+ | -H -HVT #H
+ lapply (cpx_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24
+ @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/
+ ]
+ | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+ lapply (csn_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
+ lapply (csn_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
+ @(csn_cpx_trans … HVY) /2 width=1/
+ ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
+ lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
+ @csn_abbr /2 width=3 by csn_cpx_trans/ -HV
+ @(csn_lpx_conf … (L. ⓓW0)) /2 width=1/ -W1
+ @(csn_cpxs_trans … HVT) -HVT /3 width=1/
+]
+qed-.
+
+lemma csn_appl_theta: ∀h,g,a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀L,V,T. ⦃h, L⦄ ⊢ ⬊*[g] ⓓ{a}V.ⓐV2.T → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV1.ⓓ{a}V.T.
+/2 width=5 by csn_appl_theta_aux/ qed.
+
+(* Basic_1: was just: sn3_appl_appl *)
+lemma csn_appl_simple_tstc: ∀h,g,L,V. ⦃h, L⦄ ⊢ ⬊*[g] V → ∀T1. ⦃h, L⦄ ⊢ ⬊*[g] T1 →
+ (∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → (T1 ≃ T2 → ⊥) → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T2) →
+ 𝐒⦃T1⦄ → ⦃h, L⦄ ⊢ ⬊*[g] ⓐV.T1.
+#h #g #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csn_intro #X #HL #H
+elim (cpx_inv_appl1_simple … HL ?) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (eq_false_inv_tpair_sn … H) -H
+[ -IHT1 #HV0
+ @(csn_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
+ @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
+ #T2 #HLT12 #HT12
+ @(csn_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+ @H2T1 -H2T1 // -HLT12 /2 width=1/
+| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
+ elim (tstc_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
+ #T2 #HLT02 #HT02
+ @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
+ | -IHT1 -H3T1 -H1T10
+ @H2T1 -H2T1 /2 width=1/
+ ]
+]
+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/reduction/lpx_aaa.ma".
-include "basic_2/computation/lprs.ma".
-
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.
-#L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3 by aaa_lpr_conf/
-qed-.
interpretation "parallel computation (local environment, sn variant) alternative"
'PRedSnStarAlt L1 L2 = (lprsa L1 L2).
-(* Main properties on the alternative definition **********************************)
+(* Main properties on the alternative definition ****************************)
theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2.
/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
-(* Main inversion lemmas on the alternative definition ****************************)
+(* Main inversion lemmas on the alternative definition **********************)
theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2.
/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-.
-(* Alternative eliminators ********************************************************)
+(* Alternative eliminators **************************************************)
lemma lprs_ind_alt: ∀R:relation lenv.
R (⋆) (⋆) → (
theorem lprs_conf: confluent2 … lprs lprs.
/3 width=3 by TC_confluent2, lpr_conf/ qed-.
-theorem lfprs_trans: Transitive … lprs.
+theorem lprs_trans: Transitive … lprs.
/2 width=3/ 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/reduction/lpx.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+definition lpxs: ∀h. sd h → relation lenv ≝ λh,g. TC … (lpx h g).
+
+interpretation "extended parallel computation (local environment, sn variant)"
+ 'PRedSnStar h g L1 L2 = (lpxs h g L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lpxs_ind: ∀h,g,L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. ⦃h, L1⦄ ⊢ ➡*[g] L → ⦃h, L⦄ ⊢ ➡[g] L2 → R L → R L2) →
+ ∀L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L2.
+#h #g #L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma lpxs_ind_dx: ∀h,g,L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. ⦃h, L1⦄ ⊢ ➡[g] L → ⦃h, L⦄ ⊢ ➡*[g] L2 → R L → R L1) →
+ ∀L1. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L1.
+#h #g #L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+/3 width=3/ qed.
+
+lemma lpx_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+/2 width=1/ qed.
+
+lemma lpxs_refl: ∀h,g,L. ⦃h, L⦄ ⊢ ➡*[g] L.
+/2 width=1/ qed.
+
+lemma lpxs_strap1: ∀h,g,L1,L,L2. ⦃h, L1⦄ ⊢ ➡*[g] L → ⦃h, L⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+/2 width=3/ qed.
+
+lemma lpxs_strap2: ∀h,g,L1,L,L2. ⦃h, L1⦄ ⊢ ➡[g] L → ⦃h, L⦄ ⊢ ➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+/2 width=3/ qed.
+
+lemma lpxs_pair_refl: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ∀I,V. ⦃h, L1. ⓑ{I}V⦄ ⊢ ➡*[g] L2. ⓑ{I}V.
+/2 width=1 by TC_lpx_sn_pair_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpxs_inv_atom1: ∀h,g,L2. ⦃h, ⋆⦄ ⊢ ➡*[g] L2 → L2 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
+
+lemma lpxs_inv_atom2: ∀h,g,L1. ⦃h, L1⦄ ⊢ ➡*[g] ⋆ → L1 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpxs_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → |L1| = |L2|.
+/2 width=2 by TC_lpx_sn_fwd_length/ 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/reduction/lpx_aaa.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lpxs_conf: ∀h,g,L1,T,A.
+ L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → L2 ⊢ T ⁝ A.
+#h #g #L1 #T #A #HT #L2 #HL12
+@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_lpx_conf/
+qed-.
+
+lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.
+#L1 #T #A #HT #L2 #HL12
+@(aaa_lpxs_conf … HT) -A -T /2 width=3/
+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/computation/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* alternative definition *)
+definition lpxsa: ∀h. sd h → relation lenv ≝ λh,g. lpx_sn … (cpxs h g).
+
+interpretation "extended parallel computation (local environment, sn variant) alternative"
+ 'PRedSnStarAlt h g L1 L2 = (lpxsa h g L1 L2).
+
+(* Main properties on the alternative definition ****************************)
+
+theorem lpxsa_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
+
+(* Main inversion lemmas on the alternative definition **********************)
+
+theorem lpxs_inv_lpxsa: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡➡*[g] L2.
+/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
+
+(* Alternative eliminators **************************************************)
+
+lemma lpxs_ind_alt: ∀h,g. ∀R:relation lenv.
+ R (⋆) (⋆) → (
+ ∀I,K1,K2,V1,V2.
+ ⦃h, K1⦄ ⊢ ➡*[g] K2 → ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 →
+ R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ 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/computation/cpxs_cpxs.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Advanced properties ******************************************************)
+
+lemma lpxs_pair: ∀h,g,I,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ∀V1,V2. ⦃h, L1⦄ ⊢ V1 ➡*[g] V2 →
+ ⦃h, L1.ⓑ{I}V1⦄ ⊢ ➡*[g] L2.ⓑ{I}V2.
+/2 width=1 by TC_lpx_sn_pair/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpxs_inv_pair1: ∀h,g,I,K1,L2,V1. ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡*[g] L2 →
+ ∃∃K2,V2. ⦃h, K1⦄ ⊢ ➡*[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 & L2 = K2.ⓑ{I}V2.
+/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
+
+lemma lpxs_inv_pair2: ∀h,g,I,L1,K2,V2. ⦃h, L1⦄ ⊢ ➡*[g] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃h, K1⦄ ⊢ ➡*[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 & L1 = K1.ⓑ{I}V1.
+/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
+
+(* Properties on context-sensitive extended parallel computation for terms **)
+
+lemma lpxs_cpx_trans: ∀h,g. s_r_trans … (cpx h g) (lpxs h g).
+/3 width=5 by s_r_trans_TC2, lpx_cpxs_trans/ qed-.
+
+lemma lpxs_cpxs_trans: ∀h,g. s_rs_trans … (cpx h g) (lpxs h g).
+/3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ qed-.
+
+lemma cpxs_bind2: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+ ∀I,T1,T2. ⦃h, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[g] T2 →
+ ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
+#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lapply (lpxs_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
+qed.
+
+(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
+
+lemma cpxs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[g] U2 →
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 ➡*[g] T2 &
+ U2 = ⓛ{a}V2.T2.
+#h #g #a #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02
+lapply (cpxs_strap1 … HV10 … HV02) -V0
+lapply (cpxs_trans … HT10 … HT02) -T0 /2 width=5/
+qed-.
+
+lemma cpxs_inv_abbr1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[g] U2 → (
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L.ⓓV1⦄ ⊢ T1 ➡*[g] T2 &
+ U2 = ⓓ{a}V2.T2
+ ) ∨
+ ∃∃T2. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡*[g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#h #g #a #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpx_inv_abbr1 … HU02) -HU02 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct
+ lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02
+ lapply (cpxs_strap1 … HV10 … HV02) -V0
+ lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=5/
+ | #T2 #HT02 #HUT2
+ lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02
+ lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=3/
+ ]
+| #U1 #HTU1 #HU01
+ elim (lift_total U2 0 1) #U #HU2
+ lapply (cpx_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/
+]
+qed-.
+
+(* More advanced properties *************************************************)
+
+lemma lpxs_pair2: ∀h,g,I,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 →
+ ∀V1,V2. ⦃h, L2⦄ ⊢ V1 ➡*[g] V2 → ⦃h, L1.ⓑ{I}V1⦄ ⊢ ➡*[g] L2.ⓑ{I}V2.
+/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ 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/reduction/lpx_ldrop.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpxs_ldrop_conf: ∀h,g. dropable_sn (lpxs h g).
+/3 width=3 by dropable_sn_TC, lpx_ldrop_conf/ qed-.
+
+lemma ldrop_lpxs_trans: ∀h,g. dedropable_sn (lpxs h g).
+/3 width=3 by dedropable_sn_TC, ldrop_lpx_trans/ qed-.
+
+lemma lpxs_ldrop_trans_O1: ∀h,g. dropable_dx (lpxs h g).
+/3 width=3 by dropable_dx_TC, lpx_ldrop_trans_O1/ 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/computation/lpxs.ma".
+
+(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
+
+(* Main properties **********************************************************)
+
+theorem lpxs_trans: ∀h,g. Transitive … (lpxs h g).
+/2 width=3/ qed-.
| #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
elim (IHLK1 … HK12) #K #HL1K #HK2
lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
- lapply (s7 … HA … HV2 … HLK1 HV21) -HV2
+ lapply (s8 … HA … HV2 … HLK1 HV21) -HV2
elim (lift_total W2 d e) /4 width=9/
]
]
l: abstraction
n: native type annotation
-NAMING CONVENTIONS FOR TRANSFORMATIONS
+NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
- first letter
-second letter
-p: parallel
-s: sequential
+i: irreducible form
+n: normal form
+p: parallel transformation
+r: reducible form
+s: sequential transformation
- third letter
- forth letter (if present)
-p: non-reflexive transitive closure
-q: reflexive closure
-s: reflexive transitive closure
+p: non-reflexive transitive closure (plus)
+q: reflexive closure (question)
+s: reflexive transitive closure (star)
(* Reduction ****************************************************************)
-notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )"
+notation "hvbox( L ⊢ 𝐑 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $L $T }.
-notation "hvbox( L ⊢ break 𝐈 ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐑 break [ term 46 g ] break ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'Reducible $h $g $L $T }.
+
+notation "hvbox( L ⊢ 𝐈 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $L $T }.
-notation "hvbox( L ⊢ break 𝐍 ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐈 break [ term 46 g ] break ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'NotReducible $h $g $L $T }.
+
+notation "hvbox( L ⊢ 𝐍 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'Normal $L $T }.
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐍 break [ term 46 g ] break ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'Normal $h $g $L $T }.
+
notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
(* Computation **************************************************************)
+notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )"
+ non associative with precedence 45
+ for @{ 'InEInt $R $L $T $A }.
+
+notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEq $T1 $R $T2 }.
+
notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $h $g $L $T1 $T2 }.
+
notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedSnStar $L1 $L2 }.
-notation "hvbox( L1 ⊢ ➡➡* break term 46 L2 )"
+notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 g ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'PRedSnStarAlt $L1 $L2 }.
+ for @{ 'PRedSnStar $h $g $L1 $L2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
+notation "hvbox( L1 ⊢ ➡ ➡ * break term 46 L2 )"
non associative with precedence 45
- for @{ 'PEval $L $T1 $T2 }.
+ for @{ 'PRedSnStarAlt $L1 $L2 }.
-notation "hvbox( L ⊢ ⬊ * break term 46 T )"
+notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ ➡ * break [ term 46 g ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'SN $L $T }.
+ for @{ 'PRedSnStarAlt $h $g $L1 $L2 }.
-notation "hvbox( L ⊢ ⬊ ⬊ * break term 46 T )"
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )"
non associative with precedence 45
- for @{ 'SNAlt $L $T }.
+ for @{ 'DecomposedPRedStar $h $g $L $T1 $T2 }.
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
non associative with precedence 45
- for @{ 'PRedStar $h $g $L $T1 $T2 }.
+ for @{ 'PEval $L $T1 $T2 }.
notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )"
non associative with precedence 45
non associative with precedence 45
for @{ 'SNAlt $h $g $L $T }.
-notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )"
- non associative with precedence 45
- for @{ 'InEInt $R $L $T $A }.
-
-notation "hvbox( T1 ⊑ break [ term 46 R ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'CrSubEq $T1 $R $T2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DecomposedXPRedStar $h $g $L $T1 $T2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ term 46 g ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DecomposedXSN $h $g $L $T }.
-
(* Conversion ***************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
+++ /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/reduction/crf.ma".
-
-(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
-
-definition cif: lenv → predicate term ≝ λL,T. L ⊢ 𝐑⦃T⦄ → ⊥.
-
-interpretation "context-sensitive irreducibility (term)"
- 'NotReducible L T = (cif L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cif_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐈⦃#i⦄ → ⊥.
-/3 width=3/ qed-.
-
-lemma cif_inv_ri2: ∀I,L,V,T. ri2 I → L ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
-/3 width=1/ qed-.
-
-lemma cif_inv_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
- L ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄.
-/4 width=1/ qed-.
-
-lemma cif_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
- ∧∧ L ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I.
-#a * [ elim a -a ]
-[ #L #V #T #H elim (H ?) -H /3 width=1/
-|*: #L #V #T #H elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=1/
-]
-qed-.
-
-lemma cif_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.
-#L #V #T #HVT @and3_intro /3 width=1/
-generalize in match HVT; -HVT elim T -T //
-* // #a * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
-qed-.
-
-lemma cif_inv_flat: ∀I,L,V,T. L ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
- ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
-* #L #V #T #H
-[ elim (cif_inv_appl … H) -H /2 width=1/
-| elim (cif_inv_ri2 … H) -H /2 width=1/
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tif_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄.
-/2 width=2 by trf_inv_atom/ qed.
-
-lemma cif_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
-#a #I #L #V #T #HI #HV #HT #H
-elim (crf_inv_ib2 … HI H) -HI -H /2 width=1/
-qed.
-
-lemma cif_appl: ∀L,V,T. L ⊢ 𝐈⦃V⦄ → L ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐈⦃ⓐV.T⦄.
-#L #V #T #HV #HT #H1 #H2
-elim (crf_inv_appl … H2) -H2 /2 width=1/
-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/reduction/crf_append.ma".
-include "basic_2/reduction/cif.ma".
-
-(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
-
-(* Advanved properties ******************************************************)
-
-lemma cif_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄.
-/3 width=2 by crf_inv_labst_last/ qed.
-
-lemma cif_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄.
-/3 width=2 by crf_inv_trf/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cif_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃T⦄.
-/3 width=1/ qed-.
-
-lemma cif_inv_tif: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄ → ⋆ ⊢ 𝐈⦃T⦄.
-/3 width=1/ 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/reduction/crr.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+definition cir: lenv → predicate term ≝ λL,T. L ⊢ 𝐑⦃T⦄ → ⊥.
+
+interpretation "context-sensitive irreducibility (term)"
+ 'NotReducible L T = (cir L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cir_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐈⦃#i⦄ → ⊥.
+/3 width=3/ qed-.
+
+lemma cir_inv_ri2: ∀I,L,V,T. ri2 I → L ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
+/3 width=1/ qed-.
+
+lemma cir_inv_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ L ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄.
+/4 width=1/ qed-.
+
+lemma cir_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ∧∧ L ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I.
+#a * [ elim a -a ]
+[ #L #V #T #H elim H -H /3 width=1/
+|*: #L #V #T #H elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+]
+qed-.
+
+lemma cir_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.
+#L #V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // #a * #U #T #_ #_ #H elim H -H /2 width=1/
+qed-.
+
+lemma cir_inv_flat: ∀I,L,V,T. L ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
+ ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
+* #L #V #T #H
+[ elim (cir_inv_appl … H) -H /2 width=1/
+| elim (cir_inv_ri2 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cir_sort: ∀L,k. L ⊢ 𝐈⦃⋆k⦄.
+/2 width=3 by crr_inv_sort/ qed.
+
+lemma cir_gref: ∀L,p. L ⊢ 𝐈⦃§p⦄.
+/2 width=3 by crr_inv_gref/ qed.
+
+lemma tir_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄.
+/2 width=2 by trr_inv_atom/ qed.
+
+lemma cir_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
+#a #I #L #V #T #HI #HV #HT #H
+elim (crr_inv_ib2 … HI H) -HI -H /2 width=1/
+qed.
+
+lemma cir_appl: ∀L,V,T. L ⊢ 𝐈⦃V⦄ → L ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐈⦃ⓐV.T⦄.
+#L #V #T #HV #HT #H1 #H2
+elim (crr_inv_appl … H2) -H2 /2 width=1/
+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/reduction/crr_append.ma".
+include "basic_2/reduction/cir.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+(* Advanved properties ******************************************************)
+
+lemma cir_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄.
+/3 width=2 by crr_inv_labst_last/ qed.
+
+lemma cir_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄.
+/3 width=2 by crr_inv_trr/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cir_inv_append_sn: ∀L,K,T. K @@ L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃T⦄.
+/3 width=1/ qed-.
+
+lemma cir_inv_tir: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄ → ⋆ ⊢ 𝐈⦃T⦄.
+/3 width=1/ 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/reduction/crr_lift.ma".
+include "basic_2/reduction/cir.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+(* Properties on relocation *************************************************)
+
+lemma cir_lift: ∀K,T. K ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → L ⊢ 𝐈⦃U⦄.
+/3 width=7 by crr_inv_lift/ qed.
+
+lemma cir_inv_lift: ∀L,U. L ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → K ⊢ 𝐈⦃T⦄.
+/3 width=7/ 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/reduction/cir.ma".
+include "basic_2/reduction/crx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************)
+
+definition cix: ∀h. sd h → lenv → predicate term ≝ λh,g,L,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → ⊥.
+
+interpretation "context-sensitive extended irreducibility (term)"
+ 'NotReducible h g L T = (cix h g L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cix_inv_sort: ∀h,g,L,k,l. deg h g k (l+1) → ⦃h, L⦄ ⊢ 𝐈[g]⦃⋆k⦄ → ⊥.
+/3 width=2/ qed-.
+
+lemma cix_inv_delta: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, L⦄ ⊢ 𝐈[g]⦃#i⦄ → ⊥.
+/3 width=4/ qed-.
+
+lemma cix_inv_ri2: ∀h,g,I,L,V,T. ri2 I → ⦃h, L⦄ ⊢ 𝐈[g]⦃②{I}V.T⦄ → ⊥.
+/3 width=1/ qed-.
+
+lemma cix_inv_ib2: ∀h,g,a,I,L,V,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓑ{a,I}V.T⦄ →
+ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[g]⦃T⦄.
+/4 width=1/ qed-.
+
+lemma cix_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓑ{a,I}V.T⦄ →
+ ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[g]⦃T⦄ & ib2 a I.
+#h #g #a * [ elim a -a ]
+[ #L #V #T #H elim H -H /3 width=1/
+|*: #L #V #T #H elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+]
+qed-.
+
+lemma cix_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓐV.T⦄ →
+ ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ & 𝐒⦃T⦄.
+#h #g #L #V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // #a * #U #T #_ #_ #H elim H -H /2 width=1/
+qed-.
+
+lemma cix_inv_flat: ∀h,g,I,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓕ{I}V.T⦄ →
+ ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
+#h #g * #L #V #T #H
+[ elim (cix_inv_appl … H) -H /2 width=1/
+| elim (cix_inv_ri2 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cix_inv_cir: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → L ⊢ 𝐈⦃T⦄.
+/3 width=1/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cix_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐈[g]⦃⋆k⦄.
+#h #g #L #k #Hk #H elim (crx_inv_sort … H) -L #l #Hkl
+lapply (deg_mono … Hk Hkl) -h -k <plus_n_Sm #H destruct
+qed.
+
+lemma tix_lref: ∀h,g,i. ⦃h, ⋆⦄ ⊢ 𝐈[g]⦃#i⦄.
+#h #g #i #H elim (trx_inv_atom … H) -H #k #l #_ #H destruct
+qed.
+
+lemma cix_gref: ∀h,g,L,p. ⦃h, L⦄ ⊢ 𝐈[g]⦃§p⦄.
+#h #g #L #p #H elim (crx_inv_gref … H)
+qed.
+
+lemma cix_ib2: ∀h,g,a,I,L,V,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ → ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[g]⦃T⦄ →
+ ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓑ{a,I}V.T⦄.
+#h #g #a #I #L #V #T #HI #HV #HT #H
+elim (crx_inv_ib2 … HI H) -HI -H /2 width=1/
+qed.
+
+lemma cix_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ → ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → 𝐒⦃T⦄ → ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓐV.T⦄.
+#h #g #L #V #T #HV #HT #H1 #H2
+elim (crx_inv_appl … H2) -H2 /2 width=1/
+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/reduction/crx_append.ma".
+include "basic_2/reduction/cix.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cix_inv_append_sn: ∀h,g,L,K,T. ⦃h, K @@ L⦄ ⊢ 𝐈[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄.
+/3 width=1/ qed-.
+
+lemma cix_inv_tix: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → ⦃h, ⋆⦄ ⊢ 𝐈[g]⦃T⦄.
+/3 width=1/ 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/reduction/crx_lift.ma".
+include "basic_2/reduction/cix.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cix_lref: ∀h,g,L,i. ⇩[0, i] L ≡ ⋆ → ⦃h, L⦄ ⊢ 𝐈[g]⦃#i⦄.
+#h #g #L #i #HL #H elim (crx_inv_lref … H) -h #I #K #V #HLK
+lapply (ldrop_mono … HLK … HL) -L -i #H destruct
+qed.
+
+(* Properties on relocation *************************************************)
+
+lemma cix_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ 𝐈[g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊢ 𝐈[g]⦃U⦄.
+/3 width=7 by crx_inv_lift/ qed.
+
+lemma cix_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ 𝐈[g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ 𝐈[g]⦃T⦄.
+/3 width=7/ 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/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
-
-definition cnf: lenv → predicate term ≝ λL. NF … (cpr L) (eq …).
-
-interpretation
- "context-sensitive normality (term)"
- 'Normal L T = (cnf L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cnf_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐍⦃#i⦄ → ⊥.
-#L #K #V #i #HLK #H
-elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct
-elim (lift_inv_lref2_be … HVW ? ?) -HVW //
-qed-.
-
-lemma cnf_inv_abst: ∀a,L,V,T. L ⊢ 𝐍⦃ⓛ{a}V.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓛV ⊢ 𝐍⦃T⦄.
-#a #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
-]
-qed-.
-
-lemma cnf_inv_abbr: ∀L,V,T. L ⊢ 𝐍⦃-ⓓV.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓓV ⊢ 𝐍⦃T⦄.
-#L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
-]
-qed-.
-
-lemma cnf_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
-#L #V #T #H elim (is_lift_dec T 0 1)
-[ * #U #HTU
- lapply (H U ?) -H /2 width=3/ #H destruct
- elim (lift_inv_pair_xy_y … HTU)
-| #HT
- elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
- lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/
-]
-qed-.
-
-lemma cnf_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V⦄ & L ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
-#L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
-| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
- [ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
- | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
-]
-qed-.
-
-lemma cnf_inv_tau: ∀L,V,T. L ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
-#L #V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: nf2_sort *)
-lemma cnf_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄.
-#L #k #X #H
->(cpr_inv_sort1 … H) //
-qed.
-
-(* Basic_1: was: nf2_abst *)
-lemma cnf_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄.
-#a #I #L #V #W #T #HW #HT #X #H
-elim (cpr_fwd_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct
->(HW … HW0) -W0 >(HT … HT0) -T0 //
-qed.
-
-(* Basic_1: was only: nf2_appl_lref *)
-lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄.
-#L #V #T #HV #HT #HS #X #H
-elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
->(HV … HV0) -V0 >(HT … HT0) -T0 //
-qed.
-
-(* Basic_1: was: nf2_dec *)
-axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨
- ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
-
-(* Basic_1: removed theorems 1: nf2_abst_shift *)
+++ /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/reduction/cpr_cif.ma".
-include "basic_2/reduction/cnf_crf.ma".
-
-(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
-
-(* Main properties on context-sensitive irreducible terms *******************)
-
-theorem cif_cnf: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄.
-/2 width=3 by cpr_fwd_cif/ qed.
-
-(* Main inversion lemmas on context-sensitive irreducible terms *************)
-
-theorem cnf_inv_cif: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄.
-/2 width=4 by cnf_inv_crf/ 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/reduction/crf.ma".
-include "basic_2/reduction/cnf.ma".
-
-(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
-
-(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
-
-(* Note: this property is unusual *)
-lemma cnf_inv_crf: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥.
-#L #T #H elim H -L -T
-[ #L #K #V #i #HLK #H
- elim (cnf_inv_delta … HLK H)
-| #L #V #T #_ #IHV #H
- elim (cnf_inv_appl … H) -H /2 width=1/
-| #L #V #T #_ #IHT #H
- elim (cnf_inv_appl … H) -H /2 width=1/
-| #I #L #V #T * #H1 #H2 destruct
- [ elim (cnf_inv_zeta … H2)
- | elim (cnf_inv_tau … H2)
- ]
-|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
- [1,3: elim (cnf_inv_abbr … H2) -H2 /2 width=1/
- |*: elim (cnf_inv_abst … H2) -H2 /2 width=1/
- ]
-| #a #L #V #W #T #H
- elim (cnf_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| #a #L #V #W #T #H
- elim (cnf_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-]
-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/reduction/cpr_lift.ma".
-include "basic_2/reduction/cnf.ma".
-
-(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was only: nf2_csort_lref *)
-lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍⦃#i⦄.
-#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 cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄.
-#L #K #V #i #HLK #X #H
-elim (cpr_inv_lref1 … H) -H // *
-#K0 #V1 #V2 #HLK0 #_ #_
-lapply (ldrop_mono … HLK … HLK0) -L #H destruct
-qed.
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: was: nf2_lift *)
-lemma cnf_lift: ∀L0,L,T,T0,d,e.
- L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄.
-#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
-elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
-<(HLT … HT1) in HT0; -L #HT0
->(lift_mono … HT10 … HT0) -T1 -X //
-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/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+definition cnr: lenv → predicate term ≝ λL. NF … (cpr L) (eq …).
+
+interpretation
+ "context-sensitive normality (term)"
+ 'Normal L T = (cnr L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cnr_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐍⦃#i⦄ → ⊥.
+#L #K #V #i #HLK #H
+elim (lift_total V 0 (i+1)) #W #HVW
+lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct
+elim (lift_inv_lref2_be … HVW) -HVW //
+qed-.
+
+lemma cnr_inv_abst: ∀a,L,V,T. L ⊢ 𝐍⦃ⓛ{a}V.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓛV ⊢ 𝐍⦃T⦄.
+#a #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+]
+qed-.
+
+lemma cnr_inv_abbr: ∀L,V,T. L ⊢ 𝐍⦃-ⓓV.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓓV ⊢ 𝐍⦃T⦄.
+#L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+]
+qed-.
+
+lemma cnr_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
+#L #V #T #H elim (is_lift_dec T 0 1)
+[ * #U #HTU
+ lapply (H U ?) -H /2 width=3/ #H destruct
+ elim (lift_inv_pair_xy_y … HTU)
+| #HT
+ elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+ lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/
+]
+qed-.
+
+lemma cnr_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V⦄ & L ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
+#L #V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
+ [ elim (lift_total V1 0 1) #V2 #HV12
+ lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
+ | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
+]
+qed-.
+
+lemma cnr_inv_tau: ∀L,V,T. L ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
+#L #V #T #H lapply (H T ?) -H /2 width=1/ #H
+@discr_tpair_xy_y //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: nf2_sort *)
+lemma cnr_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄.
+#L #k #X #H
+>(cpr_inv_sort1 … H) //
+qed.
+
+(* Basic_1: was: nf2_abst *)
+lemma cnr_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄.
+#a #I #L #V #W #T #HW #HT #X #H
+elim (cpr_fwd_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct
+>(HW … HW0) -W0 >(HT … HT0) -T0 //
+qed.
+
+(* Basic_1: was only: nf2_appl_lref *)
+lemma cnr_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄.
+#L #V #T #HV #HT #HS #X #H
+elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
+>(HV … HV0) -V0 >(HT … HT0) -T0 //
+qed.
+
+(* Basic_1: was: nf2_dec *)
+axiom cnr_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨
+ ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
+
+(* Basic_1: removed theorems 1: nf2_abst_shift *)
--- /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/reduction/cpr_cir.ma".
+include "basic_2/reduction/cnr_crr.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+(* Main properties on context-sensitive irreducible terms *******************)
+
+theorem cir_cnr: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄.
+/2 width=3 by cpr_fwd_cir/ qed.
+
+(* Main inversion lemmas on context-sensitive irreducible terms *************)
+
+theorem cnr_inv_cir: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄.
+/2 width=4 by cnr_inv_crr/ 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/reduction/crr.ma".
+include "basic_2/reduction/cnr.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
+
+(* Note: this property is unusual *)
+lemma cnr_inv_crr: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥.
+#L #T #H elim H -L -T
+[ #L #K #V #i #HLK #H
+ elim (cnr_inv_delta … HLK H)
+| #L #V #T #_ #IHV #H
+ elim (cnr_inv_appl … H) -H /2 width=1/
+| #L #V #T #_ #IHT #H
+ elim (cnr_inv_appl … H) -H /2 width=1/
+| #I #L #V #T * #H1 #H2 destruct
+ [ elim (cnr_inv_zeta … H2)
+ | elim (cnr_inv_tau … H2)
+ ]
+|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
+ [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/
+ |*: elim (cnr_inv_abst … H2) -H2 /2 width=1/
+ ]
+| #a #L #V #W #T #H
+ elim (cnr_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #a #L #V #W #T #H
+ elim (cnr_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+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/reduction/cpr_lift.ma".
+include "basic_2/reduction/cnr.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was only: nf2_csort_lref *)
+lemma cnr_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍⦃#i⦄.
+#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: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄.
+#L #K #V #i #HLK #X #H
+elim (cpr_inv_lref1 … H) -H // *
+#K0 #V1 #V2 #HLK0 #_ #_
+lapply (ldrop_mono … HLK … HLK0) -L #H destruct
+qed.
+
+(* Relocation properties ****************************************************)
+
+(* Basic_1: was: nf2_lift *)
+lemma cnr_lift: ∀L0,L,T,T0,d,e.
+ L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄.
+#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
+<(HLT … HT1) in HT0; -L #HT0
+>(lift_mono … HT10 … HT0) -T1 -X //
+qed.
+
+(* Note: this was missing in basic_1 *)
+lemma cnr_inv_lift: ∀L0,L,T,T0,d,e.
+ L0 ⊢ 𝐍⦃T0⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L ⊢ 𝐍⦃T⦄.
+#L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
+elim (lift_total X d e) #X0 #HX0
+lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0
+>(HLT0 … HTX0) in HX0; -L0 -X0 #H
+>(lift_inj … H … HT0) -T0 -X -d -e //
+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/reduction/cnr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
+
+definition cnx: ∀h. sd h → lenv → predicate term ≝
+ λh,g,L. NF … (cpx h g L) (eq …).
+
+interpretation
+ "context-sensitive extended normality (term)"
+ 'Normal h g L T = (cnx h g L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cnx_inv_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄ → deg h g k 0.
+#h #g #L #k #H elim (deg_total h g k)
+#l @(nat_ind_plus … l) -l // #l #_ #Hkl
+lapply (H (⋆(next h k)) ?) -H /2 width=2/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
+lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
+qed-.
+
+lemma cnx_inv_delta: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃h, L⦄ ⊢ 𝐍[g]⦃#i⦄ → ⊥.
+#h #g #I #L #K #V #i #HLK #H
+elim (lift_total V 0 (i+1)) #W #HVW
+lapply (H W ?) -H [ /3 width=7/ ] -HLK #H destruct
+elim (lift_inv_lref2_be … HVW) -HVW //
+qed-.
+
+lemma cnx_inv_abst: ∀h,g,a,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓛ{a}V.T⦄ →
+ ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ ∧ ⦃h, L.ⓛV⦄ ⊢ 𝐍[g]⦃T⦄.
+#h #g #a #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+]
+qed-.
+
+lemma cnx_inv_abbr: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃-ⓓV.T⦄ →
+ ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ ∧ ⦃h, L.ⓓV⦄ ⊢ 𝐍[g]⦃T⦄.
+#h #g #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+]
+qed-.
+
+lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥.
+#h #g #L #V #T #H elim (is_lift_dec T 0 1)
+[ * #U #HTU
+ lapply (H U ?) -H /2 width=3/ #H destruct
+ elim (lift_inv_pair_xy_y … HTU)
+| #HT
+ elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+ lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/
+]
+qed-.
+
+lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄ →
+ ∧∧ ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ & ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ & 𝐒⦃T⦄.
+#h #g #L #V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
+ [ elim (lift_total V1 0 1) #V2 #HV12
+ lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
+ | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
+]
+qed-.
+
+lemma cnx_inv_tau: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓝV.T⦄ → ⊥.
+#h #g #L #V #T #H lapply (H T ?) -H /2 width=1/ #H
+@discr_tpair_xy_y //
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cnx_fwd_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → L ⊢ 𝐍⦃T⦄.
+#h #g #L #T #H #U #HTU
+@H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *)
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cnx_sort: ∀h,g,L,k. deg h g k 0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆k⦄.
+#h #g #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_
+lapply (deg_mono … Hkl Hk) -h -L <plus_n_Sm #H destruct
+qed.
+
+lemma cnx_sort_iter: ∀h,g,L,k,l. deg h g k l → ⦃h, L⦄ ⊢ 𝐍[g]⦃⋆((next h)^l k)⦄.
+#h #g #L #k #l #Hkl
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1/
+qed.
+
+lemma cnx_abst: ∀h,g,a,L,W,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃W⦄ → ⦃h, L.ⓛW⦄ ⊢ 𝐍[g]⦃T⦄ →
+ ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓛ{a}W.T⦄.
+#h #g #a #L #W #T #HW #HT #X #H
+elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
+>(HW … HW0) -W0 >(HT … HT0) -T0 //
+qed.
+
+lemma cnx_appl_simple: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → 𝐒⦃T⦄ →
+ ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄.
+#h #g #L #V #T #HV #HT #HS #X #H
+elim (cpx_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
+>(HV … HV0) -V0 >(HT … HT0) -T0 //
+qed.
+
+axiom cnx_dec: ∀h,g,L,T1. ⦃h, L⦄ ⊢ 𝐍[g]⦃T1⦄ ∨
+ ∃∃T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 & (T1 = T2 → ⊥).
--- /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/reduction/cpx_cix.ma".
+include "basic_2/reduction/cnx_crx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
+
+(* Main properties on context-sensitive extended irreducible terms **********)
+
+theorem cix_cnr: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄.
+/2 width=5 by cpx_fwd_cix/ qed.
+
+(* Main inversion lemmas on context-sensitive extended irreducible terms ****)
+
+theorem cnr_inv_cix: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄.
+/2 width=6 by cnx_inv_crx/ 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/reduction/crx.ma".
+include "basic_2/reduction/cnx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
+
+(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
+
+(* Note: this property is unusual *)
+lemma cnx_inv_crx: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⊥.
+#h #g #L #T #H elim H -L -T
+[ #L #k #l #Hkl #H
+ lapply (cnx_inv_sort … H) -H #H
+ lapply (deg_mono … H Hkl) -h -L -k <plus_n_Sm #H destruct
+| #I #L #K #V #i #HLK #H
+ elim (cnx_inv_delta … HLK H)
+| #L #V #T #_ #IHV #H
+ elim (cnx_inv_appl … H) -H /2 width=1/
+| #L #V #T #_ #IHT #H
+ elim (cnx_inv_appl … H) -H /2 width=1/
+| #I #L #V #T * #H1 #H2 destruct
+ [ elim (cnx_inv_zeta … H2)
+ | elim (cnx_inv_tau … H2)
+ ]
+|6,7: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
+ [1,3: elim (cnx_inv_abbr … H2) -H2 /2 width=1/
+ |*: elim (cnx_inv_abst … H2) -H2 /2 width=1/
+ ]
+| #a #L #V #W #T #H
+ elim (cnx_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #a #L #V #W #T #H
+ elim (cnx_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+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/reduction/cpx_lift.ma".
+include "basic_2/reduction/cnx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cnx_lref_atom: ∀h,g,L,i. ⇩[0, i] L ≡ ⋆ → ⦃h, L⦄ ⊢ 𝐍[g]⦃#i⦄.
+#h #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,L0,L,T,T0,d,e. ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → ⇩[d, e] L0 ≡ L →
+ ⇧[d, e] T ≡ T0 → ⦃h, L0⦄ ⊢ 𝐍[g]⦃T0⦄.
+#h #g #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
+<(HLT … HT1) in HT0; -L #HT0
+>(lift_mono … HT10 … HT0) -T1 -X //
+qed.
+
+lemma cnx_inv_lift: ∀h,g,L0,L,T,T0,d,e. ⦃h, L0⦄ ⊢ 𝐍[g]⦃T0⦄ → ⇩[d, e] L0 ≡ L →
+ ⇧[d, e] T ≡ T0 → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄.
+#h #g #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
+elim (lift_total X d e) #X0 #HX0
+lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
+>(HLT0 … HTX0) in HX0; -L0 -X0 #H
+>(lift_inj … H … HT0) -T0 -X -d -e //
+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/reduction/cif.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Advanced forward lemmas on context-sensitive irreducible terms ***********)
-
-lemma cpr_fwd_cif: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1.
-#L #T1 #T2 #H elim H -L -T1 -T2
-[ //
-| #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
- elim (cif_inv_delta … HLK ?) //
-| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
- [ elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
- lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
- lapply (IHT1 … HT1) -IHT1 #H destruct //
- | elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=2/
- ]
-| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
- [ elim (cif_inv_appl … H) -H #HV1 #HT1 #_
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (cif_inv_ri2 … H) /2 width=1/
- ]
-| #L #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (cif_inv_ri2 … H) /2 width=1/
-| #L #V1 #T1 #T2 #_ #_ #H
- elim (cif_inv_ri2 … H) /2 width=1/
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
- elim (cif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (cif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-]
-qed-.
-
-lemma cpss_fwd_cif_eq: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1.
-/3 width=3 by cpr_fwd_cif, cpss_cpr/ 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/reduction/cir.ma".
+include "basic_2/reduction/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
+
+(* Advanced forward lemmas on context-sensitive irreducible terms ***********)
+
+lemma cpr_fwd_cir: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1.
+#L #T1 #T2 #H elim H -L -T1 -T2
+[ //
+| #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
+ elim (cir_inv_delta … HLK) //
+| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct
+ lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
+ lapply (IHT1 … HT1) -IHT1 #H destruct //
+ | elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=2/
+ ]
+| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (cir_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (cir_inv_ri2 … H) /2 width=1/
+ ]
+| #L #V1 #T1 #T #T2 #_ #_ #_ #H
+ elim (cir_inv_ri2 … H) /2 width=1/
+| #L #V1 #T1 #T2 #_ #_ #H
+ elim (cir_inv_ri2 … H) /2 width=1/
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (cir_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (cir_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+qed-.
+
+lemma cpss_fwd_cir_eq: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ 𝐈⦃T1⦄ → T2 = T1.
+/3 width=3 by cpr_fwd_cir, cpss_cpr/ 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/reduction/cix.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Advanced forward lemmas on context-sensitive extended irreducible terms **)
+
+lemma cpx_fwd_cix: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ 𝐈[g]⦃T1⦄ → T2 = T1.
+#h #g #L #T1 #T2 #H elim H -L -T1 -T2
+[ //
+| #L #k #l #Hkl #H elim (cix_inv_sort … Hkl H)
+| #I #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
+ elim (cix_inv_delta … HLK) //
+| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (cix_inv_bind … H) -H #HV1 #HT1 * #H destruct
+ lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
+ lapply (IHT1 … HT1) -IHT1 #H destruct //
+ | elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=2/
+ ]
+| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (cix_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (cix_inv_ri2 … H) /2 width=1/
+ ]
+| #L #V1 #T1 #T #T2 #_ #_ #_ #H
+ elim (cix_inv_ri2 … H) /2 width=1/
+| #L #V1 #T1 #T2 #_ #_ #H
+ elim (cix_inv_ri2 … H) /2 width=1/
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (cix_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (cix_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+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/ldrop.ma".
-
-(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
-
-(* reducible binary items *)
-definition ri2: predicate item2 ≝
- λI. I = Bind2 true Abbr ∨ I = Flat2 Cast.
-
-(* irreducible binary binders *)
-definition ib2: relation2 bool bind2 ≝
- λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr.
-
-(* reducible terms *)
-inductive crf: lenv → predicate term ≝
-| crf_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crf L (#i)
-| crf_appl_sn: ∀L,V,T. crf L V → crf L (ⓐV. T)
-| crf_appl_dx: ∀L,V,T. crf L T → crf L (ⓐV. T)
-| crf_ri2 : ∀I,L,V,T. ri2 I → crf L (②{I}V. T)
-| crf_ib2_sn : ∀a,I,L,V,T. ib2 a I → crf L V → crf L (ⓑ{a,I}V. T)
-| crf_ib2_dx : ∀a,I,L,V,T. ib2 a I → crf (L.ⓑ{I}V) T → crf L (ⓑ{a,I}V. T)
-| crf_beta : ∀a,L,V,W,T. crf L (ⓐV. ⓛ{a}W. T)
-| crf_theta : ∀a,L,V,W,T. crf L (ⓐV. ⓓ{a}W. T)
-.
-
-interpretation
- "context-sensitive reducibility (term)"
- 'Reducible L T = (crf L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
-#I #L #T * -L -T
-[ #L #K #V #i #HLK #H1 #H2 destruct
- elim (ldrop_inv_atom1 … HLK) -HLK #H destruct
-| #L #V #T #_ #_ #H destruct
-| #L #V #T #_ #_ #H destruct
-| #J #L #V #T #_ #_ #H destruct
-| #a #J #L #V #T #_ #_ #_ #H destruct
-| #a #J #L #V #T #_ #_ #_ #H destruct
-| #a #L #V #W #T #_ #H destruct
-| #a #L #V #W #T #_ #H destruct
-]
-qed-.
-
-lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
-/2 width=6 by trf_inv_atom_aux/ qed-.
-
-fact crf_inv_lref_aux: ∀L,T. L ⊢ 𝐑⦃T⦄ → ∀i. T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
-#L #T * -L -T
-[ #L #K #V #j #HLK #i #H destruct /2 width=3/
-| #L #V #T #_ #i #H destruct
-| #L #V #T #_ #i #H destruct
-| #J #L #V #T #_ #i #H destruct
-| #a #J #L #V #T #_ #_ #i #H destruct
-| #a #J #L #V #T #_ #_ #i #H destruct
-| #a #L #V #W #T #i #H destruct
-| #a #L #V #W #T #i #H destruct
-]
-qed-.
-
-lemma crf_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
-/2 width=3 by crf_inv_lref_aux/ qed-.
-
-fact crf_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W. U →
- L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
-#a #I #L #W #U #T #HI * -T
-[ #L #K #V #i #_ #H destruct
-| #L #V #T #_ #H destruct
-| #L #V #T #_ #H destruct
-| #J #L #V #T #H1 #H2 destruct
- elim H1 -H1 #H destruct
- elim HI -HI #H destruct
-| #b #J #L #V #T #_ #HV #H destruct /2 width=1/
-| #b #J #L #V #T #_ #HT #H destruct /2 width=1/
-| #b #L #V #W #T #H destruct
-| #b #L #V #W #T #H destruct
-]
-qed-.
-
-lemma crf_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
- L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄.
-/2 width=5 by crf_inv_ib2_aux/ qed-.
-
-fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U →
- ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
-#L #W #U #T * -T
-[ #L #K #V #i #_ #H destruct
-| #L #V #T #HV #H destruct /2 width=1/
-| #L #V #T #HT #H destruct /2 width=1/
-| #J #L #V #T #H1 #H2 destruct
- elim H1 -H1 #H destruct
-| #a #I #L #V #T #_ #_ #H destruct
-| #a #I #L #V #T #_ #_ #H destruct
-| #a #L #V #W0 #T #H destruct
- @or3_intro2 #H elim (simple_inv_bind … H)
-| #a #L #V #W0 #T #H destruct
- @or3_intro2 #H elim (simple_inv_bind … H)
-]
-qed-.
-
-lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
-/2 width=3 by crf_inv_appl_aux/ 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/ldrop_append.ma".
-include "basic_2/reduction/crf.ma".
-
-(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
-
-(* Advanved properties ******************************************************)
-
-lemma crf_labst_last: ∀L,T,W. L ⊢ 𝐑⦃T⦄ → ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄.
-#L #T #W #H elim H -L -T /2 width=1/
-#L #K #V #i #HLK
-lapply (ldrop_fwd_length_lt2 … HLK) #Hi
-lapply (ldrop_O1_append_sn_le … HLK … (⋆.ⓛW)) -HLK /2 width=2/ -Hi /2 width=3/
-qed.
-
-lemma crf_trf: ∀T,W. ⋆ ⊢ 𝐑⦃T⦄ → ⋆.ⓛW ⊢ 𝐑⦃T⦄.
-#T #W #H lapply (crf_labst_last … W H) //
-qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact crf_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ →
- ∀L2. L1 = ⋆.ⓛW @@ L2 → L2 ⊢ 𝐑⦃T⦄.
-#L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
-[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
- lapply (ldrop_fwd_length_lt2 … HLK1)
- >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
- elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct
- [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
- lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
- normalize #H destruct /2 width=3/
- | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
- lapply (ldrop_inv_O2 … H) -H #H destruct
- ]
-| #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
-]
-qed.
-
-lemma crf_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐑⦃T⦄.
-/2 width=4/ qed-.
-
-lemma crf_inv_trf: ∀T,W. ⋆.ⓛW ⊢ 𝐑⦃T⦄ → ⋆ ⊢ 𝐑⦃T⦄.
-/2 width=4/ 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/ldrop.ma".
+
+(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
+
+(* reducible binary items *)
+definition ri2: predicate item2 ≝
+ λI. I = Bind2 true Abbr ∨ I = Flat2 Cast.
+
+(* irreducible binary binders *)
+definition ib2: relation2 bool bind2 ≝
+ λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr.
+
+(* reducible terms *)
+inductive crr: lenv → predicate term ≝
+| crr_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crr L (#i)
+| crr_appl_sn: ∀L,V,T. crr L V → crr L (ⓐV.T)
+| crr_appl_dx: ∀L,V,T. crr L T → crr L (ⓐV.T)
+| crr_ri2 : ∀I,L,V,T. ri2 I → crr L (②{I}V.T)
+| crr_ib2_sn : ∀a,I,L,V,T. ib2 a I → crr L V → crr L (ⓑ{a,I}V.T)
+| crr_ib2_dx : ∀a,I,L,V,T. ib2 a I → crr (L.ⓑ{I}V) T → crr L (ⓑ{a,I}V.T)
+| crr_beta : ∀a,L,V,W,T. crr L (ⓐV. ⓛ{a}W.T)
+| crr_theta : ∀a,L,V,W,T. crr L (ⓐV. ⓓ{a}W.T)
+.
+
+interpretation
+ "context-sensitive reducibility (term)"
+ 'Reducible L T = (crr L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact crr_inv_sort_aux: ∀L,T,k. L ⊢ 𝐑⦃T⦄ → T = ⋆k → ⊥.
+#L #T #k0 * -L -T
+[ #L #K #V #i #HLK #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crr_inv_sort: ∀L,k. L ⊢ 𝐑⦃⋆k⦄ → ⊥.
+/2 width=5 by crr_inv_sort_aux/ qed-.
+
+fact crr_inv_lref_aux: ∀L,T,i. L ⊢ 𝐑⦃T⦄ → T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+#L #T #j * -L -T
+[ #L #K #V #i #HLK #H destruct /2 width=3/
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crr_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+/2 width=3 by crr_inv_lref_aux/ qed-.
+
+fact crr_inv_gref_aux: ∀L,T,p. L ⊢ 𝐑⦃T⦄ → T = §p → ⊥.
+#L #T #q * -L -T
+[ #L #K #V #i #HLK #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crr_inv_gref: ∀L,p. L ⊢ 𝐑⦃§p⦄ → ⊥.
+/2 width=5 by crr_inv_gref_aux/ qed-.
+
+lemma trr_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
+* #i #H
+[ elim (crr_inv_sort … H)
+| elim (crr_inv_lref … H) -H #L #V #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| elim (crr_inv_gref … H)
+]
+qed-.
+
+fact crr_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W.U →
+ L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
+#b #J #L #W0 #U #T #HI * -L -T
+[ #L #K #V #i #_ #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #H1 #H2 destruct
+ elim H1 -H1 #H destruct
+ elim HI -HI #H destruct
+| #a #I #L #V #T #_ #HV #H destruct /2 width=1/
+| #a #I #L #V #T #_ #HT #H destruct /2 width=1/
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crr_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
+ L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄.
+/2 width=5 by crr_inv_ib2_aux/ qed-.
+
+fact crr_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW.U →
+ ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
+#L #W0 #U #T * -L -T
+[ #L #K #V #i #_ #H destruct
+| #L #V #T #HV #H destruct /2 width=1/
+| #L #V #T #HT #H destruct /2 width=1/
+| #I #L #V #T #H1 #H2 destruct
+ elim H1 -H1 #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+ @or3_intro2 #H elim (simple_inv_bind … H)
+| #a #L #V #W #T #H destruct
+ @or3_intro2 #H elim (simple_inv_bind … H)
+]
+qed-.
+
+lemma crr_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
+/2 width=3 by crr_inv_appl_aux/ 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/ldrop_append.ma".
+include "basic_2/reduction/crr.ma".
+
+(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
+
+(* Advanved properties ******************************************************)
+
+lemma crr_append_sn: ∀L,K,T. L ⊢ 𝐑⦃T⦄ → K @@ L ⊢ 𝐑⦃T⦄.
+#L #K0 #T #H elim H -L -T /2 width=1/
+#L #K #V #i #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #Hi
+lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/
+qed.
+
+lemma trr_crr: ∀L,T. ⋆ ⊢ 𝐑⦃T⦄ → L ⊢ 𝐑⦃T⦄.
+#L #T #H lapply (crr_append_sn … H) //
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact crr_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ →
+ ∀L2. L1 = ⋆.ⓛW @@ L2 → L2 ⊢ 𝐑⦃T⦄.
+#L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
+[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
+ lapply (ldrop_fwd_length_lt2 … HLK1)
+ >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
+ elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct
+ [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
+ lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
+ normalize #H destruct /2 width=3/
+ | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
+ lapply (ldrop_inv_O2 … H) -H #H destruct
+ ]
+| #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
+]
+qed.
+
+lemma crr_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐑⦃T⦄.
+/2 width=4/ qed-.
+
+lemma crr_inv_trr: ∀T,W. ⋆.ⓛW ⊢ 𝐑⦃T⦄ → ⋆ ⊢ 𝐑⦃T⦄.
+/2 width=4/ 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/ldrop_ldrop.ma".
+include "basic_2/reduction/crr.ma".
+
+(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
+
+(* Properties on relocation *************************************************)
+
+lemma crr_lift: ∀K,T. K ⊢ 𝐑⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → L ⊢ 𝐑⦃U⦄.
+#K #T #H elim H -K -T
+[ #K #K0 #V #i #HK0 #L #d #e #HLK #X #H
+ elim (lift_inv_lref1 … H) -H * #Hid #H destruct
+ [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/
+ ]
+| #K #V #T #_ #IHV #L #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
+| #K #V #T #_ #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/
+| #I #K #V #T #HI #L #d #e #_ #X #H
+ elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/
+| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
+| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/
+| #a #K #V #V0 #T #L #d #e #_ #X #H
+ elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+| #a #K #V #V0 #T #L #d #e #_ #X #H
+ elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+]
+qed.
+
+lemma crr_inv_lift: ∀L,U. L ⊢ 𝐑⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → K ⊢ 𝐑⦃T⦄.
+#L #U #H elim H -L -U
+[ #L #L0 #W #i #HK0 #K #d #e #HLK #X #H
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/
+ | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/
+ ]
+| #L #W #U #_ #IHW #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
+| #L #W #U #_ #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/
+| #I #L #W #U #HI #K #d #e #_ #X #H
+ elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/
+| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
+| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
+| #a #L #W #W0 #U #K #d #e #_ #X #H
+ elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+| #a #L #W #W0 #U #K #d #e #_ #X #H
+ elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+]
+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/static/sd.ma".
+include "basic_2/reduction/crr.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************)
+
+(* extended reducible terms *)
+inductive crx (h) (g): lenv → predicate term ≝
+| crx_sort : ∀L,k,l. deg h g k (l+1) → crx h g L (⋆k)
+| crx_delta : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g L (#i)
+| crx_appl_sn: ∀L,V,T. crx h g L V → crx h g L (ⓐV.T)
+| crx_appl_dx: ∀L,V,T. crx h g L T → crx h g L (ⓐV.T)
+| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g L (②{I}V.T)
+| crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g L V → crx h g L (ⓑ{a,I}V.T)
+| crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g (L.ⓑ{I}V) T → crx h g L (ⓑ{a,I}V.T)
+| crx_beta : ∀a,L,V,W,T. crx h g L (ⓐV. ⓛ{a}W.T)
+| crx_theta : ∀a,L,V,W,T. crx h g L (ⓐV. ⓓ{a}W.T)
+.
+
+interpretation
+ "context-sensitive extended reducibility (term)"
+ 'Reducible h g L T = (crx h g L T).
+
+(* Basic properties *********************************************************)
+
+lemma crr_crx: ∀h,g,L,T. L ⊢ 𝐑⦃T⦄ → ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄.
+#h #g #L #T #H elim H -L -T // /2 width=1/ /2 width=4/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact crx_inv_sort_aux: ∀h,g,L,T,k. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = ⋆k →
+ ∃l. deg h g k (l+1).
+#h #g #L #T #k0 * -L -T
+[ #L #k #l #Hkl #H destruct /2 width=2/
+| #I #L #K #V #i #HLK #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crx_inv_sort: ∀h,g,L,k. ⦃h, L⦄ ⊢ 𝐑[g]⦃⋆k⦄ → ∃l. deg h g k (l+1).
+/2 width=4 by crx_inv_sort_aux/ qed-.
+
+fact crx_inv_lref_aux: ∀h,g,L,T,i. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = #i →
+ ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+#h #g #L #T #j * -L -T
+[ #L #k #l #_ #H destruct
+| #I #L #K #V #i #HLK #H destruct /2 width=4/
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crx_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊢ 𝐑[g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+/2 width=5 by crx_inv_lref_aux/ qed-.
+
+fact crx_inv_gref_aux: ∀h,g,L,T,p. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = §p → ⊥.
+#h #g #L #T #q * -L -T
+[ #L #k #l #_ #H destruct
+| #I #L #K #V #i #HLK #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crx_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊢ 𝐑[g]⦃§p⦄ → ⊥.
+/2 width=7 by crx_inv_gref_aux/ qed-.
+
+lemma trx_inv_atom: ∀h,g,I. ⦃h, ⋆⦄ ⊢ 𝐑[g]⦃⓪{I}⦄ →
+ ∃∃k,l. deg h g k (l+1) & I = Sort k.
+#h #g * #i #H
+[ elim (crx_inv_sort … H) -H /2 width=4/
+| elim (crx_inv_lref … H) -H #I #L #V #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| elim (crx_inv_gref … H)
+]
+qed-.
+
+fact crx_inv_ib2_aux: ∀h,g,a,I,L,W,U,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ →
+ T = ⓑ{a,I}W.U → ⦃h, L⦄ ⊢ 𝐑[g]⦃W⦄ ∨ ⦃h, L.ⓑ{I}W⦄ ⊢ 𝐑[g]⦃U⦄.
+#h #g #b #J #L #W0 #U #T #HI * -L -T
+[ #L #k #l #_ #H destruct
+| #I #L #K #V #i #_ #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #I #L #V #T #H1 #H2 destruct
+ elim H1 -H1 #H destruct
+ elim HI -HI #H destruct
+| #a #I #L #V #T #_ #HV #H destruct /2 width=1/
+| #a #I #L #V #T #_ #HT #H destruct /2 width=1/
+| #a #L #V #W #T #H destruct
+| #a #L #V #W #T #H destruct
+]
+qed-.
+
+lemma crx_inv_ib2: ∀h,g,a,I,L,W,T. ib2 a I → ⦃h, L⦄ ⊢ 𝐑[g]⦃ⓑ{a,I}W.T⦄ →
+ ⦃h, L⦄ ⊢ 𝐑[g]⦃W⦄ ∨ ⦃h, L.ⓑ{I}W⦄ ⊢ 𝐑[g]⦃T⦄.
+/2 width=5 by crx_inv_ib2_aux/ qed-.
+
+fact crx_inv_appl_aux: ∀h,g,L,W,U,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → T = ⓐW.U →
+ ∨∨ ⦃h, L⦄ ⊢ 𝐑[g]⦃W⦄ | ⦃h, L⦄ ⊢ 𝐑[g]⦃U⦄ | (𝐒⦃U⦄ → ⊥).
+#h #g #L #W0 #U #T * -L -T
+[ #L #k #l #_ #H destruct
+| #I #L #K #V #i #_ #H destruct
+| #L #V #T #HV #H destruct /2 width=1/
+| #L #V #T #HT #H destruct /2 width=1/
+| #I #L #V #T #H1 #H2 destruct
+ elim H1 -H1 #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W #T #H destruct
+ @or3_intro2 #H elim (simple_inv_bind … H)
+| #a #L #V #W #T #H destruct
+ @or3_intro2 #H elim (simple_inv_bind … H)
+]
+qed-.
+
+lemma crx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃ⓐV.T⦄ →
+ ∨∨ ⦃h, L⦄ ⊢ 𝐑[g]⦃V⦄ | ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ | (𝐒⦃T⦄ → ⊥).
+/2 width=3 by crx_inv_appl_aux/ 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/ldrop_append.ma".
+include "basic_2/reduction/crx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************)
+
+(* Advanved properties ******************************************************)
+
+lemma crx_append_sn: ∀h,g,L,K,T. ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄ → ⦃h, K @@ L⦄ ⊢ 𝐑[g]⦃T⦄.
+#h #g #L #K0 #T #H elim H -L -T /2 width=1/ /2 width=2/
+#I #L #K #V #i #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #Hi
+lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=4/
+qed.
+
+lemma trx_crx: ∀h,g,L,T. ⦃h, ⋆⦄ ⊢ 𝐑[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐑[g]⦃T⦄.
+#h #g #L #T #H lapply (crx_append_sn … H) //
+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/ldrop_ldrop.ma".
+include "basic_2/reduction/crx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************)
+
+(* Properties on relocation *************************************************)
+
+lemma crx_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ 𝐑[g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊢ 𝐑[g]⦃U⦄.
+#h #g #K #T #H elim H -K -T
+[ #K #k #l #Hkl #L #d #e #_ #X #H
+ >(lift_inv_sort1 … H) -X /2 width=2/
+| #I #K #K0 #V #i #HK0 #L #d #e #HLK #X #H
+ elim (lift_inv_lref1 … H) -H * #Hid #H destruct
+ [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/
+ ]
+| #K #V #T #_ #IHV #L #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
+| #K #V #T #_ #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/
+| #I #K #V #T #HI #L #d #e #_ #X #H
+ elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/
+| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
+| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/
+| #a #K #V #V0 #T #L #d #e #_ #X #H
+ elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+| #a #K #V #V0 #T #L #d #e #_ #X #H
+ elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+]
+qed.
+
+lemma crx_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ 𝐑[g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ 𝐑[g]⦃T⦄.
+#h #g #L #U #H elim H -L -U
+[ #L #k #l #Hkl #K #d #e #_ #X #H
+ >(lift_inv_sort2 … H) -X /2 width=2/
+| #I #L #L0 #W #i #HK0 #K #d #e #HLK #X #H
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/
+ | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/
+ ]
+| #L #W #U #_ #IHW #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
+| #L #W #U #_ #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/
+| #I #L #W #U #HI #K #d #e #_ #X #H
+ elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/
+| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
+| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
+| #a #L #W #W0 #U #K #d #e #_ #X #H
+ elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+| #a #L #W #W0 #U #K #d #e #_ #X #H
+ elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+]
+qed.
include "basic_2/static/lsuba_aaa.ma".
include "basic_2/reduction/lpx_ldrop.ma".
-(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
(* Properties on atomic arity assignment for terms **************************)
axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.
+(* Advanced properties ******************************************************)
+
(* Basic_1: was: drop_conf_lt *)
lemma ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
elim (ldrop_inv_skip1 … HK2) -HK2 [2: /2 width=1/] #K1 #V1 #HK21 #HV12 #H destruct /2 width=5/
qed.
+(* Note: apparently this was missing in basic_1 *)
+lemma ldrop_trans_lt: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
+ ∀e2,L2,I,V2. ⇩[0, e2] L ≡ L2.ⓑ{I}V2 →
+ e2 < d1 → let d ≝ d1 - e2 - 1 in
+ ∃∃L0,V0. ⇩[0, e2] L1 ≡ L0.ⓑ{I}V0 &
+ ⇩[d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
+#d1 #e1 #L1 #L #HL1 #e2 #L2 #I #V2 #HL2 #Hd21
+elim (ldrop_trans_le … HL1 … HL2) -L [2: /2 width=1/ ] #L0 #HL10 #HL02
+elim (ldrop_inv_skip2 … HL02) -HL02 [2: /2 width=1/ ] #L #V1 #HL2 #HV21 #H destruct /2 width=5/
+qed-.
+
lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
⇩[d1, e1] L1 ≡ L → ⇩[0, e2] L ≡ L2 → d1 ≤ e2 →
⇩[0, e2 + e1] L1 ≡ L2.
(* Basic forward lemmas *****************************************************)
+lemma lift_fwd_pair1: ∀I,T2,V1,U1,d,e. ⇧[d,e] ②{I}V1.U1 ≡ T2 →
+ ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & T2 = ②{I}V2.U2.
+* [ #a ] #I #T2 #V1 #U1 #d #e #H
+[ elim (lift_inv_bind1 … H) -H /2 width=4/
+| elim (lift_inv_flat1 … H) -H /2 width=4/
+]
+qed-.
+
+lemma lift_fwd_pair2: ∀I,T1,V2,U2,d,e. ⇧[d,e] T1 ≡ ②{I}V2.U2 →
+ ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & T1 = ②{I}V1.U1.
+* [ #a ] #I #T1 #V2 #U2 #d #e #H
+[ elim (lift_inv_bind2 … H) -H /2 width=4/
+| elim (lift_inv_flat2 … H) -H /2 width=4/
+]
+qed-.
+
lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
(* Basic properties *********************************************************)
+lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
+#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ <minus_n_O // ]
+#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
+qed.
+
lemma deg_pred: ∀h,g,k,l. deg h g (next h k) (l + 1) → deg h g k (l + 2).
#h #g #k #l #H1
elim (deg_total h g k) #l0 #H0
lapply (le_to_lt_to_lt … IHl H) -IHl -H /2 width=2/
qed.
+lemma nexts_lt: ∀h,k,l. k < (next h)^(l+1) k.
+#h #k #l >iter_SO
+lapply (nexts_le h k l) #H
+@(le_to_lt_to_lt … H) //
+qed.
+
axiom nexts_dec: ∀h,k1,k2. Decidable (∃l. (next h)^l k1 = k2).
axiom nexts_inj: ∀h,k,l1,l2. (next h)^l1 k = (next h)^l2 k → l1 = l2.
[ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
}
]
- [ { "context-sensitive extended computation" * } {
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_lift" * ]
- }
- ]
[ { "weakly normalizing computation" * } {
[ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
}
]
[ { "strongly normalizing computation" * } {
[ "csn_vector ( ? ⊢ ⬊* ? )" "csn_tstc_vector" + "csn_aaa" * ]
- [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpr" * ]
+ [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpx" * ]
+ }
+ ]
+ [ { "context-sensitive extended computation" * } {
+ [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
- [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_lpss" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ]
- [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_tstc" + "cprs_tstc_vector" + "cprs_lift" + "cprs_lpss" + "cprs_aaa" + "cprs_cprs" * ]
+ [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_lpss" + "lprs_cprs" + "lprs_lprs" * ]
+ [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_lpss" + "cprs_cprs" * ]
}
]
[ { "local env. ref. for abstract candidates of reducibility" * } {
]
class "water"
[ { "reduction" * } {
+ [ { "context-sensitive extended normal forms" * } {
+ [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
+ }
+ ]
[ { "context-sensitive extended reduction" * } {
[ "lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpx_ldrop" + "lpx_aaa" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" + "cpx_cix" * ]
+ }
+ ]
+ [ { "context-sensitive extended irreducible forms" * } {
+ [ "cix ( ⦃?,?⦄ ⊢ 𝐈[?]⦃?⦄ )" "cix_append" + "cix_lift" * ]
+ }
+ ]
+ [ { "context-sensitive extended reducible forms" * } {
+ [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ )" "crx_append" + "crx_lift" * ]
}
]
[ { "context-sensitive normal forms" * } {
- [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_liftt" + "cnf_crf" + "cnf_cif" * ]
+ [ "cnr ( ? ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
[ { "context-sensitive reduction" * } {
[ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_lpr" * ]
- [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ]
+ [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ]
+ }
+ ]
+ [ { "context-sensitive irreducible forms" * } {
+ [ "cir ( ? ⊢ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ]
}
]
[ { "context-sensitive reducible forms" * } {
- [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ]
+ [ "crr ( ? ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ]
}
]
}
]
class "red"
[ { "grammar" * } {
- [ { "pointwise extension of a relation" * } {
+ [ { "pointwise extension of a relation" * } {
[ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
}
]
definition NF: ∀A. relation A → relation A → predicate A ≝
λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1.
+definition NF_dec: ∀A. relation A → relation A → Prop ≝
+ λA,R,S. ∀a1. NF A R S a1 ∨
+ ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥).
+
inductive SN (A) (R,S:relation A): predicate A ≝
| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1
.
elim HSa12 -HSa12 /2 width=1/
qed.
+lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
+ ∀a1. SN A R S a1 →
+ ∃∃a2. star … R a1 a2 & NF A R S a2.
+#A #R #S #HRS #a1 #H elim H -a1
+#a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3/
+* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3/
+qed-.
+
definition NF_sn: ∀A. relation A → relation A → predicate A ≝
λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.
projects / helm.git / commitdiff