next_plus/props next_plus_lt
nf2/arity arity_nf2_inv_all
nf2/dec nf2_dec
+
nf2/fwd nf2_gen_lref
nf2/fwd nf2_gen_abst
nf2/fwd nf2_gen_cast
nf2/fwd nf2_gen_flat
nf2/fwd nf2_gen__nf2_gen_aux
nf2/fwd nf2_gen_abbr
+
nf2/fwd nf2_gen_void
nf2/iso nf2_iso_appls_lref
-nf2/lift1 nf2_lift1
nf2/pr3 nf2_pr3_unfold
nf2/pr3 nf2_pr3_confluence
-nf2/props nf2_sort
-nf2/props nf2_csort_lref
-nf2/props nf2_abst
-nf2/props nf2_abst_shift
+
nf2/props nfs2_tapp
nf2/props nf2_appls_lref
-nf2/props nf2_appl_lref
-nf2/props nf2_lref_abst
-nf2/props nf2_lift
+
pc1/props pc1_pr0_r
pc1/props pc1_pr0_x
pc1/props pc1_refl
pr2/fwd pr2_gen_void
pr2/props pr2_ctail
pr2/subst1 pr2_gen_cabbr
+
pr3/fwd pr3_gen_sort
pr3/fwd pr3_gen_abst
pr3/fwd pr3_gen_cast
pr3/iso pr3_iso_appls_beta
pr3/pr1 pr3_pr1
pr3/pr3 pr3_strip
-pr3/pr3 pr3_confluence
-pr3/props clear_pr3_trans
-pr3/props pr3_pr2
-pr3/props pr3_t
pr3/props pr3_thin_dx
pr3/props pr3_head_1
pr3/props pr3_head_2
pr3/props pr3_head_21
pr3/props pr3_head_12
-pr3/props pr3_cflat
pr3/props pr3_flat
-pr3/props pr3_pr0_pr2_t
-pr3/props pr3_pr2_pr2_t
-pr3/props pr3_pr2_pr3_t
pr3/props pr3_pr3_pr3_t
pr3/props pr3_lift
pr3/props pr3_eta
pr3/subst1 pr3_subst1
pr3/subst1 pr3_gen_cabbr
pr3/wcpr0 pr3_wcpr0_t
-sc3/arity sc3_arity_csubc
-sc3/arity sc3_arity
-sc3/props sc3_arity_gen
-sc3/props sc3_repl
-sc3/props sc3_lift
-sc3/props sc3_lift1
-sc3/props sc3_abbr
-sc3/props sc3_cast
-sc3/props sc3_props__sc3_sn3_abst
-sc3/props sc3_sn3
-sc3/props sc3_abst
-sc3/props sc3_bind
-sc3/props sc3_appl
-sn3/fwd sn3_gen_bind
-sn3/fwd sn3_gen_flat
-sn3/fwd sn3_gen_head
-sn3/fwd sn3_gen_cflat
-sn3/fwd sn3_gen_lift
-sn3/lift1 sns3_lifts1
-sn3/nf2 sn3_nf2
sn3/nf2 nf2_sn3
sn3/props sn3_pr3_trans
-sn3/props sn3_pr2_intro
-sn3/props sn3_cast
-sn3/props sn3_cflat
+sn3/props sn3_cpr3_trans
+
sn3/props sn3_shift
sn3/props sn3_change
sn3/props sn3_gen_def
sn3/props sn3_cdelta
-sn3/props sn3_cpr3_trans
-sn3/props sn3_bind
sn3/props sn3_beta
sn3/props sn3_appl_lref
sn3/props sn3_appl_abbr
sn3/props sn3_appls_cast
sn3/props sn3_appls_bind
sn3/props sn3_appls_beta
-sn3/props sn3_lift
sn3/props sn3_abbr
sn3/props sn3_appls_abbr
sn3/props sns3_lifts
+
sty0/fwd sty0_gen_sort
sty0/fwd sty0_gen_lref
sty0/fwd sty0_gen_bind
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.
+ ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0.
definition CP4s ≝ λRR:lenv→relation term. λRS:relation term.
∀L0,L,des. ⇩*[des] L0 ≡ L →
(* Basic properties *********************************************************)
+(* Basic_1: was: nf2_lift1 *)
lemma acp_lifts: ∀RR,RS. CP4 RR RS → CP4s RR RS.
#RR #RS #HRR #L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
(* Main propertis ***********************************************************)
+(* Basic_1: was: sc3_arity_csubc *)
theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
]
qed.
+(* Basic_1: was: sc3_arity *)
lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L,T,A. L ⊢ T ÷ A → ⦃L, T⦄ [RP] ϵ 〚A〛.
/2 width=8/ qed.
definition S6 ≝ λ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. ∀L1,L2,T1,T2,d,e.
- C L1 T1 → ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
+definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e.
+ C L1 T1 â\86\92 â\88\80T2. â\87©[d, e] L2 â\89¡ L1 â\86\92 â\87§[d, e] T1 â\89¡ T2 â\86\92 C L2 T2.
definition S7s ≝ λC:lenv→predicate term.
∀L1,L2,des. ⇩*[des] L2 ≡ L1 →
(* Basic properties *********************************************************)
+(* Basic_1: was: sc3_lift1 *)
lemma acr_lifts: ∀C. S7 C → S7s C.
#C #HC #L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
@(s7 … HRP)
qed.
+(* Basic_1: was only: sns3_lifts1 *)
lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
- ∀des,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L →
+ ∀des,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L →
all … (RP L) Vs → all … (RP L0) V0s.
#RR #RS #RP #HRP #des #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //
#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s
@conj /2 width=1/ /2 width=6 by rp_lifts/
qed.
+(* Basic_1: was:
+ sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift
+*)
lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀A. acr RR RS RP (aacr RP A).
#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
@(s3 … HCA … ◊) /2 width=6 by rp_lifts/
@(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/
qed.
+
+(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
+(* Basic_1: removed local theorems 1: sc3_sn3_abst *)
--- /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/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Basic_1: includes: pr3_pr2 *)
+definition cprs: lenv → relation term ≝
+ λL. TC … (cpr L).
+
+interpretation "context-sensitive parallel computation (term)"
+ 'PRedStar L T1 T2 = (cprs L T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 →
+ (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) →
+ ∀T2. L ⊢ T1 ➡* T2 → R T2.
+#L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: pr3_refl *)
+lemma cprs_refl: ∀L,T. L ⊢ T ➡* T.
+/2 width=1/ qed.
+
+lemma cprs_strap1: ∀L,T1,T,T2.
+ L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → L ⊢ T1 ➡* T2.
+/2 width=3/ qed.
+
+(* Basic_1: was: pr3_step *)
+lemma cprs_strap2: ∀L,T1,T,T2.
+ L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
+/2 width=3/ qed.
+
+(* Note: it does not hold replacing |L1| with |L2| *)
+lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+ ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡* T2.
+/3 width=3/
+qed.
+
+(* Basic_1: removed theorems 2: clear_pr3_trans pr3_cflat *)
--- /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/reducibility/cpr_cpr.ma".
+include "Basic_2/computation/cprs_lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Main propertis ***********************************************************)
+
+(* Basic_1: was: pr3_t *)
+theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
+/2 width=3/ qed.
+
+(* Basic_1: was: pr3_confluence *)
+theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 →
+ ∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0.
+/3 width=3/ qed.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was only: pr3_pr2_pr3_t *)
+lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT2 /3 width=5/
+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/reducibility/ltpr_tps.ma".
+include "Basic_2/reducibility/cpr_ltpss.ma".
+include "Basic_2/reducibility/lcpr.ma".
+include "Basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning context-sensitive parallel reduction on lenv's *****)
+
+lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 →
+ ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2
+[ /2 width=3/
+| #T #T2 #_ #HT2 * #T0 #HT10 #HT0
+ elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32
+ @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *)
+ @(cprs_strap1 … T3 …) /2 width=1/ -HT32
+ @(cprs_strap1 … HT0) -HT0 /3 width=3/
+]
+qed.
+
+(* Basic_1: was just: pr3_pr0_pr2_t *)
+lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 * #T #HT1
+<(ltpr_fwd_length … HL12) #HT2
+elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/
+qed.
+
+(* Basic_1: was just: pr3_pr2_pr2_t *)
+lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 * /3 width=7/
+qed.
(**************************************************************************)
include "Basic_2/reducibility/cpr.ma".
-include "Basic_2/computation/acp.ma".
+include "Basic_2/reducibility/cnf.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
interpretation
"context-sensitive strong normalization (term)"
- 'SN L T = (csn L T).
+ 'SN L T = (csn L T).
+
+(* Basic eliminators ********************************************************)
+
+lemma csn_ind: ∀L. ∀R:predicate term.
+ (∀T1. L ⊢ ⬇* T1 →
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → R T2) →
+ R T1
+ ) →
+ ∀T. L ⊢ ⬇* T → R T.
+#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
+@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
+qed-.
(* Basic properties *********************************************************)
-axiom csn_acp: acp cpr (eq …) (csn …).
+(* Basic_1: was: sn3_pr2_intro *)
+lemma csn_intro: ∀L,T1.
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1.
+#L #T1 #H
+@(SN_intro … H)
+qed.
+
+(* Basic_1: was: sn3_nf2 *)
+lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* 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
+@csn_intro #T #HLT2 #HT2
+elim (term_eq_dec T1 T2) #HT12
+[ -IHT1 -HLT12 destruct /3 width=1/
+| -HT1 -HT2 /3 width=4/
+qed.
+
+axiom tpss_csn_trans: ∀L,T2. L ⊢ ⬇* T2 → ∀T1,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ ⬇* T1.
+(*
+#L #T2 #H @(csn_ind … H) -T2 #T2 #HT2 #IHT2 #T1 #d #e #HT12
+@csn_intro #T #HLT1 #HT1
+*)
+(* 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
+@csn_intro #X #H1 #H2
+elim (cpr_inv_cast1 … H1) -H1
+[ * #W0 #T0 #HLW0 #HLT0 #H destruct
+ elim (eq_false_inv_tpair … H2) -H2
+ [ /3 width=3/
+ | -HLW0 * #H destruct /3 width=1/
+ ]
+| /3 width=3/
+]
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+fact csn_fwd_flat2_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
+@csn_intro #T2 #HLT2 #HT2
+@(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+qed.
+
+(* Basic_1: was: sn3_gen_flat *)
+lemma csn_fwd_flat2: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
+/2 width=5/ qed-.
+
+(*
+sn3/fwd sn3_gen_bind
+sn3/fwd sn3_gen_head
+*)
+
+(* Basic_1: removed theorems 3: sn3_gen_cflat sn3_cflat sn3_bind *)
(**************************************************************************)
include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/csn.ma".
+include "Basic_2/computation/csn_lift.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
--- /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/reducibility/cnf_lift.ma".
+include "Basic_2/computation/acp.ma".
+include "Basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma csn_acp: acp cpr (eq …) (csn …).
+@mk_acp
+[ /2 width=1/
+| /2 width=3/
+| /2 width=5/
+| @cnf_lift
+]
+qed.
+
+lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T.
+#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT
+@csn_intro #X #H1 #H2
+elim (cpr_inv_abst1 … H1 I V) -H1
+#W0 #T0 #HLW0 #HLT0 #H destruct
+elim (eq_false_inv_tpair … H2) -H2
+[ /3 width=5/
+| -HLW0 * #H destruct /3 width=1/
+]
+qed.
+
+(* 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
+@csn_intro #T #HLT2 #HT2
+elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10
+@(IHT1 … HLT10) // -L1 -L2 #H destruct
+>(lift_mono … HT0 … HT12) in HT2; -T0 /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
+@csn_intro #T #HLT2 #HT2
+elim (lift_total T d e) #T0 #HT0
+lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10
+@(IHT1 … HLT10) // -L1 -L2 #H destruct
+>(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1/
+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 (s7 … HA … HV2 … HLK1 HV21) -HV2
elim (lift_total W2 d e) /4 width=9/
]
]
interpretation "native type annotation (term)"
'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: term_dec *)
+axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2).
+
(* Basic inversion lemmas ***************************************************)
lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False.
]
qed-.
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: term_dec *)
-axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2).
+lemma eq_false_inv_tpair: ∀I,V1,T1,V2,T2.
+ (②{I} V1. T1 = ②{I} V2. T2 → False) →
+ (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)).
+#I #V1 #T1 #V2 #T2 #H
+elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
+@or_intror @conj // #HT12 destruct /2 width=1/
+qed-.
(* Basic_1: removed theorems 3:
not_void_abst not_abbr_void not_abst_void
non associative with precedence 45
for @{ 'Simple $T }.
+notation "hvbox( L ⊢ break term 90 T1 ≈ break T2 )"
+ non associative with precedence 45
+ for @{ 'Hom $L $T1 $T2 }.
+
notation "hvbox( T1 break [ d , break e ] ≼ break T2 )"
non associative with precedence 45
for @{ 'SubEq $T1 $d $e $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/reducibility/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 properties *********************************************************)
+
+(* Basic_1: was: nf2_sort *)
+lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
+#L #k #X #H
+>(cpr_inv_sort1 … H) //
+qed.
+
+(* 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/reducibility/cpr_lift.ma".
+include "Basic_2/reducibility/cnf.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was only: nf2_csort_lref *)
+lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍[#i].
+#L #i #HLK #X #H
+elim (cpr_inv_lref1 … H) // *
+#K0 #V0 #V1 #HLK0 #_ #_ #_
+lapply (ldrop_mono … HLK … HLK0) -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) // *
+#K0 #V0 #V1 #HLK0 #_ #_ #_
+lapply (ldrop_mono … HLK … HLK0) -L #H destruct
+qed.
+
+(* Basic_1: was: nf2_abst *)
+lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍[W] → L. ⓑ{I} V ⊢ 𝐍[T] → L ⊢ 𝐍[ⓛW.T].
+#I #L #V #W #T #HW #HT #X #H
+elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct
+>(HW … HW0) -W >(HT … HT0) -T //
+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) -V >(HT … HT0) -T //
+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_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1
+>(HLT … HT1) in HT0; -L #HT0
+>(lift_mono … HT10 … HT0) -T1 -X //
+qed.
qed-.
(* Basic_1: was: pr2_gen_abst *)
-lemma cpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
- ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
-/2 width=3/ qed-.
+lemma cpr_inv_abst1: ∀L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡ U2 → ∀I,W.
+ ∃∃V2,T2. L ⊢ V1 ➡ V2 & L. ⓑ{I} W ⊢ T1 ➡ T2 & U2 = ⓛV2. T2.
+#L #V1 #T1 #Y * #X #H1 #H2 #I #W
+elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+lapply (tpss_lsubs_conf … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/
+qed-.
(* Basic_1: was pr2_gen_appl *)
lemma cpr_inv_appl1: ∀L,V1,U0,U2. L ⊢ ⓐV1. U0 ➡ 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/unfold/ltpss_ltpss.ma".
+include "Basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was pr2_gen_abbr *)
+lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
+ (∃∃V2,T2,T. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 &
+ L. ⓓV2 ⊢ T [1, |L|] ▶* T2 &
+ U2 = ⓓV2. T
+ ) ∨
+ ∃∃T. ⇧[0,1] T ≡ T1 & L ⊢ T ➡ U2.
+#L #V1 #T1 #Y * #X #H1 #H2
+elim (tpr_inv_abbr1 … H1) -H1 *
+[ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
+ elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
+ lapply (tps_lsubs_conf … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+ elim (ltpss_tps_conf … HT0 (L. ⓓV2) 1 (|L|) ?) -HT0 /2 width=1/ #V0 #HV20 #HV0
+ lapply (tpss_weak_all … HV20) -HV20 #HV20
+ lapply (tpss_lsubs_conf … HV0 (L. ⓓV2) ?) -HV0 /2 width=1/ #HV0
+ elim (tpss_conf_eq … HT2 … HV0) -T #T3 #HT23 #HVT3
+ lapply (tpss_weak_all … HVT3) -HVT3 #HVT3
+ lapply (tpss_trans_eq … HV20 … HVT3) -V0 /4 width=7/
+| /4 width=5/
+]
+qed-.
+
+(* Properties concerning partial unfold on local environments ***************)
+
+lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶* L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
+#L1 #L2 #d #e #HL12 #T1 #T2 *
+lapply (ltpss_weak_all … HL12)
+<(ltpss_fwd_length … HL12) -HL12 /3 width=5/
+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/unfold/ltpss_ltpss.ma".
-include "Basic_2/reducibility/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was pr2_gen_abbr *)
-lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
- (∃∃V2,T2,T. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 &
- L. ⓓV2 ⊢ T [1, |L|] ▶* T2 &
- U2 = ⓓV2. T
- ) ∨
- ∃∃T. ⇧[0,1] T ≡ T1 & L ⊢ T ➡ U2.
-#L #V1 #T1 #Y * #X #H1 #H2
-elim (tpr_inv_abbr1 … H1) -H1 *
-[ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
- elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- lapply (tps_lsubs_conf … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
- elim (ltpss_tps_conf … HT0 (L. ⓓV2) 1 (|L|) ?) -HT0 /2 width=1/ #V0 #HV20 #HV0
- lapply (tpss_weak_all … HV20) -HV20 #HV20
- lapply (tpss_lsubs_conf … HV0 (L. ⓓV2) ?) -HV0 /2 width=1/ #HV0
- elim (tpss_conf_eq … HT2 … HV0) -T #T3 #HT23 #HVT3
- lapply (tpss_weak_all … HVT3) -HVT3 #HVT3
- lapply (tpss_trans_eq … HV20 … HVT3) -V0 /4 width=7/
-| /4 width=5/
-]
-qed-.
qed.
(* Basic_1: was: wcpr0_ldrop_back *)
-lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 →
+lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 →
∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
elim (IHLK1 … HK12) -K1 /3 width=5/
]
qed.
+
+fact ltpr_ldrop_trans_O1_aux: ∀L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. L1 ➡ L2 →
+ d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ➡ K2.
+#L2 #K2 #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #X #H >(ltpr_inv_atom2 … H) -H /2 width=3/
+| #K2 #I #V2 #X #H
+ elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
+| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
+ elim (ltpr_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IHLK2 … HL12 ?) -L2 // /3 width=3/
+| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
+ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma ltpr_ldrop_trans_O1: ∀L1,L2. L1 ➡ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ➡ K2.
+/2 width=5/ 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/reducibility/ltpr_ldrop.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Properties concerning parallel substitution on terms *********************)
+
+lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡ L2 →
+ ∃∃T. L1 ⊢ T1 [d, e] ▶ T & T ➡ T2.
+#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e
+[ /2 width=3/
+| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
+ elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
+ elim (lift_total V1 0 (i+1)) #W1 #HVW1
+ lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/
+| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
+ elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2
+ elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/
+| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12
+ elim (IHV12 … HL12) -IHV12
+ elim (IHT12 … HL12) -L2 /3 width=5/
+]
+qed.
#L #I #V #IHL * /2 width=1/ * /2 width=1/
qed.
+lemma ltps_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → L1 [0, |L2|] ▶ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+// /3 width=2/ /3 width=3/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltps_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+normalize //
+qed-.
+
(* Basic inversion lemmas ***************************************************)
fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → e = 0 → L1 = L2.
lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L.
/2 width=1/ qed.
+lemma ltpss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → L1 [0, |L2|] ▶* L2.
+#L1 #L2 #d #e #H @(ltpss_ind … H) -L2 //
+#L #L2 #_ #HL2
+>(ltps_fwd_length … HL2) /3 width=5/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H @(ltpss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12
+/2 width=3 by ltps_fwd_length/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶* L2 → L1 = L2.
;;
let predefined_classes = [
+ ["-"; "÷"; "⊢"; ];
+ ["="; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];
["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
["⇒"; "➾"; "⇨"; "➡"; "⇉"; "⥤"; "⥰"; ] ;
["⇑"; "⇧"; "⬆"; ] ;
projects / helm.git / commitdiff