let has_cleared =
try
let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
- with _ -> true in
+ with
+ | Sys.Break as e -> raise e
+ |_ -> true in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
let has_cleared =
try
let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
- with _ -> true in
+ with
+ | Sys.Break as e -> raise e
+ | _ -> true in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
cnt/props cnt_lift
C/props clt_wf__q_ind
C/props clt_wf_ind
+
csuba/arity csuba_arity
csuba/arity csuba_arity_rev
csuba/arity arity_appls_appl
csuba/getl csuba_getl_abst_rev
csuba/getl csuba_getl_abbr_rev
csuba/props csuba_refl
+
csubc/arity csubc_arity_conf
csubc/arity csubc_arity_trans
-csubc/csuba csubc_csuba
csubc/drop1 drop1_csubc_trans
csubc/drop drop_csubc_trans
+
csubt/clear csubt_clear_conf
csubt/csuba csubt_csuba
csubt/drop csubt_drop_flat
ex1/props ex1_ty3
ex2/props ex2_nf2
ex2/props ex2_arity
-fsubst0/fwd fsubst0_gen_base
leq/asucc asucc_repl
leq/asucc asucc_inj
leq/asucc leq_asucc
pc3/dec pc3_dec
pc3/dec pc3_abst_dec
-pc3/fsubst0 pc3_pr2_fsubst0
-pc3/fsubst0 pc3_pr2_fsubst0_back
-pc3/fsubst0 pc3_fsubst0
pc3/fwd pc3_gen_not_abst
pc3/fwd pc3_gen_lift_abst
pc3/nf2 pc3_nf2
pc3/nf2 pc3_nf2_unfold
pc3/pc1 pc3_pc1
-pc3/props pc3_pr0_pr2_t
pc3/props pc3_pr2_pr2_t
pc3/props pc3_pr2_pr3_t
pc3/props pc3_pr3_pc3_t
pc3/props pc3_eta
-pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
-pc3/wcpr0 pc3_wcpr0_t
-pc3/wcpr0 pc3_wcpr0
pr0/fwd pr0_gen_void
pr0/dec nf0_dec
ty3/arity_props ty3_acyclic
ty3/arity_props ty3_sn3
ty3/dec ty3_inference
-ty3/fsubst0 ty3_fsubst0
-ty3/fsubst0 ty3_csubst0
-ty3/fsubst0 ty3_subst0
ty3/fwd ty3_gen_appl
ty3/fwd tys3_gen_nil
ty3/fwd tys3_gen_cons
ty3/pr3_props ty3_sconv
ty3/props ty3_gen_abst_abst
ty3/sty0 ty3_sty0
-ty3/subst1 ty3_gen_cabbr
ty3/subst1 ty3_gen_cvoid
+
wf3/clear wf3_clear_conf
wf3/clear clear_wf3_trans
wf3/fwd wf3_gen_sort1
(* Note: this is Tait's iii, or Girard's CR4 *)
definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
∀L,Vs. all … (RP L) Vs →
- ∀T. 𝐒[T] → NF … (RR L) RS T → C L (ⒶVs.T).
+ ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T).
(* Note: this is Tait's ii *)
definition S3 ≝ λRP,C:lenv→predicate term.
(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
definition cpe: lenv → relation term ≝
- λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍[T2].
+ λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄.
interpretation "context-sensitive parallel evaluation (term)"
'PEval L T1 T2 = (cpe L T1 T2).
(* Basic_properties *********************************************************)
(* Basic_1: was: nf2_sn3 *)
-lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍[T2].
+lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄.
#L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
elim (cnf_dec L T1) /3 width=3/
(* Main properties *********************************************************)
(* Basic_1: was: nf2_pr3_confluence *)
-theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍[T1] → ∀T2. L ⊢ T ➡* 𝐍[T2] → T1 = T2.
+theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. L ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
#L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
>(cprs_inv_cnf1 … HT1 H2T1) -T1 #HT2
qed-.
(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍[T] → T = U.
+lemma cprs_inv_cnf1: ∀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/
(* Forward lemmas involving same top term constructor ***********************)
-lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍[T] → ∀U. L ⊢ T ➡* U → T ≃ U.
+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-.
(* 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.
+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 *
/4 width=1/ qed.
(* Basic_1: was: sn3_nf2 *)
-lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* T.
+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.
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.
+ 𝐒⦃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 //
lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
(∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) →
- 𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+ 𝐒⦃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
(* Advanced properties ******************************************************)
(* Basic_1: was only: sn3_appls_lref *)
-lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] →
+lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ →
∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T.
#L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
#RP #L elim L -L // /2 width=1/
qed.
-(* Basic_1: removed theorems 2: csubc_clear_conf csubc_getl_conf *)
+(* Basic_1: removed theorems 3:
+ csubc_clear_conf csubc_getl_conf csubc_csuba
+*)
lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0.
/3 width=2/ qed.
-(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
+(* Basic_1: removed theorems 4:
+ ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
+*)
--- /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/equivalence/cpcs_ltpss.ma".
+include "basic_2/dynamic/nta_nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties about parallel unfold *****************************************)
+
+lemma nta_ltpss_tpss_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U.
+#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
+[ #L1 #k #L2 #d #e #_ #T2 #H
+ >(tpss_inv_sort1 … H) -H //
+| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #d #e #HL12 #T2 #H
+ elim (tpss_inv_lref1 … H) -H
+ [ #H destruct
+ elim (lt_or_ge i d) #Hdi
+ [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct
+ /3 width=7/
+ | elim (lt_or_ge i (d + e)) #Hide [ | -Hdi ]
+ [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct
+ /3 width=7/
+ | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=7/
+ ]
+ ]
+ | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2
+ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct
+ lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+ lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=9/
+ ]
+| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H
+ elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ]
+ [ #H destruct
+ elim (lift_total V1 0 (i+1)) #W #HW
+ elim (lt_or_ge i d) #Hdi [ -HWV1 ]
+ [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #W2 #HK12 #HW12 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+ lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12
+ lapply (cpr_tpss … HU12) -HU12 #HU12
+ @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *)
+ | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -HW -Hdi ]
+ [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #W2 #HK12 #HW12 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+ lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12
+ lapply (cpr_tpss … HU12) -HU12 #HU12
+ @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *)
+ | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /2 width=6/
+ ]
+ ]
+ | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_
+ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct
+ lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct
+ ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (cpr_tpss … HV12) #HV
+ lapply (IHTU1 (L2.ⓑ{I}V1) (d+1) e ? T1 ?) // /2 width=1/ #H
+ elim (nta_fwd_correct … H) -H #U2 #HU12
+ @(nta_conv … (ⓑ{I}V2.U1)) /3 width=2/ /3 width=4/ /4 width=4/ (**) (* explicit constructor, /5 width=6/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct
+ elim (tpss_inv_bind1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
+ lapply (cpr_tpss … HV12) #HV
+ lapply (IHTU1 L2 d e ? (ⓛW1.T1) ?) // #H
+ elim (nta_fwd_correct … H) -H #X #H
+ elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_
+ @(nta_conv … (ⓐV2.ⓛW1.U1)) /3 width=2/ /3 width=4/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (cpr_tpss … HV12) #HV
+ elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU
+ @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
+ lapply (cpr_tpss … HU12) /4 width=4/
+| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
+ @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
+]
+qed.
+
+lemma nta_ltpss_tps_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U.
+/3 width=7/ qed.
+
+lemma nta_ltpss_conf: ∀h,L1,T,U. ⦃h, L1⦄ ⊢ T : U →
+ ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T : U.
+/2 width=7/ qed.
+
+lemma nta_tpss_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U →
+ ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U.
+/2 width=7/ qed.
+
+lemma nta_tps_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U →
+ ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U.
+/2 width=7/ qed.
#L #T1 #T2 #H @(cpcs_ind … H) -T2 // /3 width=3/
qed.
-(* Basic_1: removed theorems 6:
+(* Basic_1: removed theorems 9:
clear_pc3_trans pc3_ind_left
pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
- Basic_1: removed local theorems 5:
+ pc3_pr2_fsubst0 pc3_pr2_fsubst0_back pc3_fsubst0
+ Basic_1: removed local theorems 6:
pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left
+ pc3_wcpr0_t_aux
*)
elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
qed.
+lemma cpcs_bind_sn: ∀I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{I}V1. T ⬌* ⓑ{I}V2. T.
+* /2 width=1/ /2 width=2/ qed.
+
(* Basic_1: was: pc3_lift *)
lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ 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/reducibility/cpr_ltpr.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Properties about context-free parallel reduction on local environments ***)
+
+(* Basic_1: was only: pc3_pr0_pr2_t *)
+(* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
+lemma ltpr_cpr_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #HT12
+elim (cpr_ltpr_conf_eq … HT12 … HL12) -L1 #T #HT1 #HT2
+@(cprs_div … T) /2 width=1/ /3 width=1/ (**) (* /4 width=3/ is too long *)
+qed.
+
+(* Basic_1: was: pc3_wcpr0_t *)
+(* Basic_1: note: pc3_wcpr0_t should be renamed *)
+lemma ltpr_cprs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1
+@(cpcs_trans … IHT1) -T1 /2 width=3/
+qed.
+
+(* Basic_1: was: pc3_wcpr0 *)
+lemma ltpr_cpcs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #HL12 #T1 #T2 #H
+elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
+@(cpcs_canc_dx … 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/unfold/ltpss_ltpss.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Properties concerning partial unfold on local environments ***************)
+
+lemma ltpss_cpr_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #d #e #HL12 #T1 #T2 *
+lapply (ltpss_weak_all … HL12)
+>(ltpss_fwd_length … HL12) -HL12 #HL12 #T #HT1 #HT2
+elim (ltpss_tpss_conf … HT2 … HL12) -L1 #T0 #HT0 #HT20
+@(cprs_div … T0) /3 width=3/ (**) (* /4/ is too slow *)
+qed.
+
+lemma ltpss_cprs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #d #e #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1
+@(cpcs_trans … IHT1) -T1 /2 width=5/
+qed.
+
+lemma ltpss_cpcs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
+#L1 #L2 #d #e #HL12 #T1 #T2 #H
+elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
+@(cpcs_canc_dx … T) /2 width=5/
+qed.
(* Basic inversion lemmas ***************************************************)
-fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → ⊥.
+fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀J,W,U. T = ⓑ{J} W. U → ⊥.
#T * -T
[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
-lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → ⊥.
+lemma simple_inv_bind: ∀I,V,T. 𝐒⦃ⓑ{I} V. T⦄ → ⊥.
/2 width=6/ qed-.
-lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J.
+lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
* /2 width=2/ #I #V #T #H
elim (simple_inv_bind … H)
qed-.
(* properties concerning simple terms ***************************************)
-lemma applv_simple: ∀T,Vs. 𝐒[T] -> 𝐒[ⒶVs.T].
+lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ -> 𝐒⦃ⒶVs.T⦄.
#T * //
qed.
inductive tshf: relation term ≝
| tshf_atom: ∀I. tshf (⓪{I}) (⓪{I})
| tshf_abst: ∀V1,V2,T1,T2. tshf (ⓛV1. T1) (ⓛV2. T2)
- | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒[T1] → 𝐒[T2] →
+ | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ →
tshf (ⓐV1. T1) (ⓐV2. T2)
.
lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
/3 width=2/ qed.
-lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2].
+lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
#T1 #T2 #H elim H -T1 -T2 //
#V1 #V2 #T1 #T2 #H
elim (simple_inv_bind … H)
qed. (**) (* remove from index *)
-lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1].
+lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
/3 width=3/ qed-.
(* Basic inversion lemmas ***************************************************)
/2 width=5/ qed-.
fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
- ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
+ ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ &
I = Appl & T2 = ⓐW2. U2.
#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
qed.
lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
- ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
+ ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ &
I = Appl & T2 = ⓐW2. U2.
/2 width=4/ qed-.
]
qed.
-lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2].
+lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
#T1 #T2 * -T1 -T2 //
#I #V1 #V2 #T1 #T2 #H
elim (simple_inv_pair … H) -H #J #H destruct //
qed. (**) (* remove from index *)
-lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒[T2] → 𝐒[T1].
+lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
/3 width=3/ qed-.
(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
lemma tstc_inv_bind_appls_simple: ∀I,Vs,V2,T1,T2. ⒶVs.T1 ≃ ⓑ{I} V2. T2 →
- 𝐒[T1] → ⊥.
+ 𝐒⦃T1⦄ → ⊥.
#I #Vs #V2 #T1 #T2 #H
elim (tstc_inv_pair2 … H) -H #V0 #T0
elim Vs -Vs normalize
non associative with precedence 90
for @{ 'Weight $x $y }.
-notation "hvbox( 𝐒 [ T ] )"
+notation "hvbox( 𝐒 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Simple $T }.
(* Reducibility *************************************************************)
-notation "hvbox( 𝐑 [ T ] )"
+notation "hvbox( 𝐑 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $T }.
-notation "hvbox( L ⊢ break 𝐑 [ T ] )"
+notation "hvbox( L ⊢ break 𝐑 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $L $T }.
-notation "hvbox( 𝐈 [ T ] )"
+notation "hvbox( 𝐈 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $T }.
-notation "hvbox( L ⊢ break 𝐈 [ T ] )"
+notation "hvbox( L ⊢ break 𝐈 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $L $T }.
-notation "hvbox( 𝐍 [ T ] )"
+notation "hvbox( 𝐍 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Normal $T }.
-notation "hvbox( L ⊢ break 𝐍 [ T ] )"
+notation "hvbox( L ⊢ break 𝐍 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Normal $L $T }.
-notation "hvbox( 𝐖𝐇𝐑 [ T ] )"
+notation "hvbox( 𝐖𝐇𝐑 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'WHdReducible $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐑 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'WHdReducible $L $T }.
-notation "hvbox( 𝐖𝐇𝐈 [ T ] )"
+notation "hvbox( 𝐖𝐇𝐈 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'NotWHdReducible $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐈 [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐈 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'NotWHdReducible $L $T }.
-notation "hvbox( 𝐖𝐇𝐍 [ T ] )"
+notation "hvbox( 𝐖𝐇𝐍 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'WHdNormal $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐍 [ T ] )"
+notation "hvbox( L ⊢ break 𝐖𝐇𝐍 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'WHdNormal $L $T }.
non associative with precedence 45
for @{ 'CPRedStar $L1 $L2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 [ T2 ] )"
+notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )"
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
(* Basic properties *********************************************************)
(* Basic_1: was: nf2_sort *)
-lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
+lemma cnf_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄.
#L #k #X #H
>(cpr_inv_sort1 … H) //
qed.
(* Basic_1: was: nf2_dec *)
-axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
+axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨
∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
(* Basic_1: removed theorems 1: nf2_abst_shift *)
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was only: nf2_csort_lref *)
-lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍[#i].
+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 #_ #_ #_
qed.
(* Basic_1: was: nf2_lref_abst *)
-lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍[#i].
+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 #_ #_ #_
qed.
(* Basic_1: was: nf2_abst *)
-lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍[W] → L. ⓑ{I} V ⊢ 𝐍[T] → L ⊢ 𝐍[ⓛW.T].
+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) -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].
+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 //
(* 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].
+ 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
qed-.
(* Note: the main property of simple terms *)
-lemma cpr_inv_appl1_simple: ∀L,V1,T1,U. L ⊢ ⓐV1. T1 ➡ U → 𝐒[T1] →
+lemma cpr_inv_appl1_simple: ∀L,V1,T1,U. L ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
U = ⓐV2. T2.
#L #V1 #T1 #U #H #HT1
#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
<(ltpss_fwd_length … HL2) /4 width=5/
qed.
+
+lemma ltpss_lcpr: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ⊢ ➡ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=3/
+qed.
(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
-definition tif: predicate term ≝ λT. 𝐑[T] → ⊥.
+definition tif: predicate term ≝ λT. 𝐑⦃T⦄ → ⊥.
interpretation "context-free irreducibility (term)"
'NotReducible T = (tif T).
(* Basic inversion lemmas ***************************************************)
-lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → ⊥.
+lemma tif_inv_abbr: ∀V,T. 𝐈⦃ⓓV.T⦄ → ⊥.
/2 width=1/ qed-.
-lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T].
+lemma tif_inv_abst: ∀V,T. 𝐈⦃ⓛV.T⦄ → 𝐈⦃V⦄ ∧ 𝐈⦃T⦄.
/4 width=1/ qed-.
-lemma tif_inv_appl: ∀V,T. 𝐈[ⓐV.T] → ∧∧ 𝐈[V] & 𝐈[T] & 𝐒[T].
+lemma tif_inv_appl: ∀V,T. 𝐈⦃ⓐV.T⦄ → ∧∧ 𝐈⦃V⦄ & 𝐈⦃T⦄ & 𝐒⦃T⦄.
#V #T #HVT @and3_intro /3 width=1/
generalize in match HVT; -HVT elim T -T //
* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
-lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → ⊥.
+lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓣV.T⦄ → ⊥.
/2 width=1/ qed-.
(* Basic properties *********************************************************)
-lemma tif_atom: ∀I. 𝐈[⓪{I}].
+lemma tif_atom: ∀I. 𝐈⦃⓪{I}⦄.
/2 width=4/ qed.
-lemma tif_abst: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐈[ⓛV.T].
+lemma tif_abst: ∀V,T. 𝐈⦃V⦄ → 𝐈⦃T⦄ → 𝐈⦃ⓛV.T⦄.
#V #T #HV #HT #H
elim (trf_inv_abst … H) -H /2 width=1/
qed.
-lemma tif_appl: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐒[T] → 𝐈[ⓐV.T].
+lemma tif_appl: ∀V,T. 𝐈⦃V⦄ → 𝐈⦃T⦄ → 𝐒⦃T⦄ → 𝐈⦃ⓐV.T⦄.
#V #T #HV #HT #S #H
elim (trf_inv_appl … H) -H /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma tnf_inv_abst: ∀V,T. 𝐍[ⓛV.T] → 𝐍[V] ∧ 𝐍[T].
+lemma tnf_inv_abst: ∀V,T. 𝐍⦃ⓛV.T⦄ → 𝐍⦃V⦄ ∧ 𝐍⦃T⦄.
#V1 #T1 #HVT1 @conj
[ #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 //
]
qed-.
-lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T].
+lemma tnf_inv_appl: ∀V,T. 𝐍⦃ⓐV.T⦄ → ∧∧ 𝐍⦃V⦄ & 𝐍⦃T⦄ & 𝐒⦃T⦄.
#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 //
]
qed-.
-lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥.
+lemma tnf_inv_abbr: ∀V,T. 𝐍⦃ⓓV.T⦄ → ⊥.
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
]
qed.
-lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → ⊥.
+lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓣV.T⦄ → ⊥.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@discr_tpair_xy_y //
qed-.
(* Main properties properties ***********************************************)
-lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈[T1] → T1 = T2.
+lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈⦃T1⦄ → T1 = T2.
#T1 #T2 #H elim H -T1 -T2
[ //
| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
]
qed.
-theorem tif_tnf: ∀T1. 𝐈[T1] → 𝐍[T1].
+theorem tif_tnf: ∀T1. 𝐈⦃T1⦄ → 𝐍⦃T1⦄.
/3 width=1/ qed.
(* Note: this property is unusual *)
-lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → ⊥.
+lemma tnf_trf_false: ∀T1. 𝐑⦃T1⦄ → 𝐍⦃T1⦄ → ⊥.
#T1 #H elim H -T1
[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
]
qed.
-theorem tnf_tif: ∀T1. 𝐍[T1] → 𝐈[T1].
+theorem tnf_tif: ∀T1. 𝐍⦃T1⦄ → 𝐈⦃T1⦄.
/2 width=3/ qed.
-lemma tnf_abst: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐍[ⓛV.T].
+lemma tnf_abst: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐍⦃ⓛV.T⦄.
/4 width=1/ qed.
-lemma tnf_appl: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐒[T] → 𝐍[ⓐV.T].
+lemma tnf_appl: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐒⦃T⦄ → 𝐍⦃ⓐV.T⦄.
/4 width=1/ qed.
qed-.
(* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] →
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
U = ⓐV2. T2.
#V1 #T1 #U #H #HT1
(* Basic inversion lemmas ***************************************************)
-fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → ⊥.
+fact trf_inv_atom_aux: ∀I,T. 𝐑⦃T⦄ → T = ⓪{I} → ⊥.
#I #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → ⊥.
+lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥.
/2 width=4/ qed-.
-fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U].
+fact trf_inv_abst_aux: ∀W,U,T. 𝐑⦃T⦄ → T = ⓛW. U → 𝐑⦃W⦄ ∨ 𝐑⦃U⦄.
#W #U #T * -T
[ #V #T #HV #H destruct /2 width=1/
| #V #T #HT #H destruct /2 width=1/
]
qed.
-lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T].
+lemma trf_inv_abst: ∀V,T. 𝐑⦃ⓛV.T⦄ → 𝐑⦃V⦄ ∨ 𝐑⦃T⦄.
/2 width=3/ qed-.
-fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U →
- ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥).
+fact trf_inv_appl_aux: ∀W,U,T. 𝐑⦃T⦄ → T = ⓐW. U →
+ ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
#W #U #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥).
+lemma trf_inv_appl: ∀W,U. 𝐑⦃ⓐW.U⦄ → ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
/2 width=3/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T.
+lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍⦃T⦄ → T ≈ T.
normalize /2 width=1/
qed-.
]
qed.
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄.
/3 width=1/ qed.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
-lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
+lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
elim (simple_inv_bind … H)
qed-.
-lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
+lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
elim (simple_inv_bind … H)
(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
+lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
+lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
qed-.
L1 = K1. ⓑ{I} V1.
/2 width=3/ qed-.
-(* Basic_1: removed theorems 27:
+(* Basic_1: removed theorems 28:
csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
csubst0_snd_bind csubst0_fst_bind csubst0_both_bind
csubst1_head csubst1_flat csubst1_gen_head
csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
-
+ fsubst0_gen_base
*)
projects / helm.git / commitdiff