- the theory of context-free parallel reduction of local environments (ltpr) is ready
- the proof of the substitution lemma for context-free parallel reduction is started ...
- some renaming and annotating
arity/subst0 arity_subst0
asucc/fwd asucc_gen_sort
asucc/fwd asucc_gen_head
-
-# check ######################################################################
-
-clen/getl getl_ctail_clen
-clen/getl getl_gen_tail
cnt/props cnt_lift
-C/props clt_cong
-C/props clt_head
C/props clt_wf__q_ind
C/props clt_wf_ind
C/props chead_ctail
-C/props clt_thead
+C/props clt_thead (ctail)
C/props c_tail_ind
-
-# waiting ####################################################################
-
csuba/arity csuba_arity
csuba/arity csuba_arity_rev
csuba/arity arity_appls_appl
csubc/fwd csubc_gen_head_r
csubc/getl csubc_getl_conf
csubc/props csubc_refl
-csubst0/clear csubst0_clear_O
-csubst0/clear csubst0_clear_O_back
-csubst0/clear csubst0_clear_S
-csubst0/clear csubst0_clear_trans
-csubst0/drop csubst0_drop_gt
-csubst0/drop csubst0_drop_gt_back
-csubst0/drop csubst0_drop_lt
-csubst0/drop csubst0_drop_eq
-csubst0/drop csubst0_drop_eq_back
-csubst0/drop csubst0_drop_lt_back
-csubst0/fwd csubst0_gen_sort
-csubst0/fwd csubst0_gen_head
-csubst0/fwd csubst0_gen_S_bind_2
-csubst0/getl csubst0_getl_ge
-csubst0/getl csubst0_getl_lt
-csubst0/getl csubst0_getl_ge_back
-csubst0/getl csubst0_getl_lt_back
-csubst0/props csubst0_snd_bind
-csubst0/props csubst0_fst_bind
-csubst0/props csubst0_both_bind
-csubst1/fwd csubst1_gen_head
-csubst1/getl csubst1_getl_ge
-csubst1/getl csubst1_getl_lt
-csubst1/getl csubst1_getl_ge_back
-csubst1/getl getl_csubst1
-csubst1/props csubst1_head
-csubst1/props csubst1_bind
-csubst1/props csubst1_flat
csubt/clear csubt_clear_conf
csubt/csuba csubt_csuba
csubt/drop csubt_drop_flat
drop1/props drop1_skip_bind
drop1/props drop1_cons_tail
drop1/props drop1_trans
-
drop/props drop_ctail
-
ex0/props aplus_gz_le
ex0/props aplus_gz_ge
ex0/props next_plus_gz
ex1/props ex1_ty3
ex2/props ex2_nf2
ex2/props ex2_arity
-
-# check ######################################################################
-
-flt/props flt_thead_sx
-flt/props flt_thead_dx
-flt/props flt_shift
-flt/props flt_arith0
-flt/props flt_arith1
-flt/props flt_arith2
-flt/props flt_trans
-flt/props flt_wf__q_ind
-flt/props flt_wf_ind
fsubst0/fwd fsubst0_gen_base
-getl/clear clear_getl_trans
-getl/clear getl_clear_trans
-getl/clear getl_clear_bind
-getl/clear getl_clear_conf
-getl/dec getl_dec
-getl/drop getl_drop
-getl/drop getl_drop_conf_lt
-getl/drop getl_drop_conf_ge
-getl/drop getl_conf_ge_drop
-getl/drop getl_drop_conf_rev
-getl/drop drop_getl_trans_lt
-getl/drop drop_getl_trans_le
-getl/drop drop_getl_trans_ge
-getl/drop getl_drop_trans
-getl/flt getl_flt
-getl/fwd getl_gen_all
-getl/fwd getl_gen_sort
-getl/fwd getl_gen_O
-getl/fwd getl_gen_S
-getl/fwd getl_gen_2
-getl/fwd getl_gen_flat
-getl/fwd getl_gen_bind
-getl/getl getl_conf_le
-getl/getl getl_trans
-getl/props getl_refl
-getl/props getl_head
-getl/props getl_flat
-getl/props getl_ctail
-getl/props getl_mono
-iso/fwd iso_gen_sort
-iso/fwd iso_gen_lref
-iso/fwd iso_gen_head
-iso/fwd iso_flats_lref_bind_false
-iso/fwd iso_flats_flat_bind_false
-iso/props iso_refl
-iso/props iso_trans
leq/asucc asucc_repl
leq/asucc asucc_inj
leq/asucc leq_asucc
lift1/props lift1_xhg
lift1/props lifts1_xhg
lift1/props lift1_free
-lift/fwd lift_sort
-lift/fwd lift_lref_lt
-lift/fwd lift_lref_ge
-lift/fwd lift_head
-lift/fwd lift_bind
-lift/fwd lift_flat
-lift/fwd lift_gen_sort
-lift/fwd lift_gen_lref
-lift/fwd lift_gen_lref_lt
-lift/fwd lift_gen_lref_false
-lift/fwd lift_gen_lref_ge
-lift/fwd lift_gen_head
-lift/fwd lift_gen_bind
-lift/fwd lift_gen_flat
lift/props thead_x_lift_y_y
-lift/props lift_r
-lift/props lift_lref_gt
lift/props lifts_tapp
-lift/props lift_inj
-lift/props lift_gen_lift
lift/props lifts_inj
-lift/props lift_free
-lift/props lift_d
-lift/tlt lift_weight_map
-lift/tlt lift_weight
-lift/tlt lift_weight_add
-lift/tlt lift_weight_add_O
-lift/tlt lift_tlt_dx
llt/props lweight_repl
llt/props llt_repl
llt/props llt_trans
pc3/wcpr0 pc3_wcpr0_t
pc3/wcpr0 pc3_wcpr0
pr0/dec nf0_dec
-pr0/fwd pr0_gen_sort
-pr0/fwd pr0_gen_lref
-pr0/fwd pr0_gen_abst
-pr0/fwd pr0_gen_appl
-pr0/fwd pr0_gen_cast
-pr0/fwd pr0_gen_abbr
-pr0/fwd pr0_gen_void
-pr0/fwd pr0_gen_lift
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta
-pr0/pr0 pr0_confluence__pr0_cong_delta
-pr0/pr0 pr0_confluence__pr0_upsilon_upsilon
-pr0/pr0 pr0_confluence__pr0_delta_delta
-pr0/pr0 pr0_confluence__pr0_delta_tau
-pr0/pr0 pr0_confluence
-pr0/props pr0_lift
-pr0/props pr0_subst0_back
-pr0/props pr0_subst0_fwd
-pr0/props pr0_subst0
-pr0/subst1 pr0_delta1
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
-pr0/subst1 pr0_subst1
pr1/pr1 pr1_strip
pr1/pr1 pr1_confluence
pr1/props pr1_pr0
pr1/props pr1_comp
pr1/props pr1_eta
pr2/clen pr2_gen_ctail
+
+# check ######################################################################
+
pr2/clen pr2_gen_cbind
pr2/clen pr2_gen_cflat
pr2/fwd pr2_gen_sort
sty1/props sty1_cast2
subst0/dec dnf_dec2
subst0/dec dnf_dec
-subst0/fwd subst0_gen_sort
-subst0/fwd subst0_gen_lref
-subst0/fwd subst0_gen_head
-subst0/fwd subst0_gen_lift_lt
-subst0/fwd subst0_gen_lift_false
-subst0/fwd subst0_gen_lift_ge
-subst0/props subst0_refl
-subst0/props subst0_lift_lt
-subst0/props subst0_lift_ge
-subst0/props subst0_lift_ge_S
-subst0/props subst0_lift_ge_s
-subst0/subst0 subst0_subst0
-subst0/subst0 subst0_subst0_back
-subst0/subst0 subst0_trans
-subst0/subst0 subst0_confluence_neq
-subst0/subst0 subst0_confluence_eq
-subst0/subst0 subst0_confluence_lift
-subst0/tlt subst0_weight_le
-subst0/tlt subst0_weight_lt
-subst0/tlt subst0_tlt_head
-subst0/tlt subst0_tlt
-subst1/fwd subst1_gen_sort
-subst1/fwd subst1_gen_lref
-subst1/fwd subst1_gen_head
+subst1/fwd subst1_gen_lift_ge
subst1/fwd subst1_gen_lift_lt
subst1/fwd subst1_gen_lift_eq
-subst1/fwd subst1_gen_lift_ge
-subst1/props subst1_head
-subst1/props subst1_lift_lt
subst1/props subst1_lift_ge
+subst1/props subst1_lift_lt
subst1/props subst1_ex
subst1/props subst1_lift_S
subst1/subst1 subst1_subst1
subst1/subst1 subst1_subst1_back
subst1/subst1 subst1_trans
-subst1/subst1 subst1_confluence_neq
-subst1/subst1 subst1_confluence_eq
subst1/subst1 subst1_confluence_lift
subst/fwd subst_sort
subst/fwd subst_lref_lt
tlist/props theads_tapp
tlist/props tcons_tapp_ex
tlist/props tlist_ind_rev
-tlt/props wadd_le
-tlt/props wadd_lt
-tlt/props wadd_O
-tlt/props weight_le
-tlt/props weight_eq
-tlt/props weight_add_O
-tlt/props weight_add_S
-tlt/props tlt_trans
-tlt/props tlt_head_sx
-tlt/props tlt_head_dx
-tlt/props tlt_wf__q_ind
-tlt/props tlt_wf_ind
T/props not_abbr_abst
T/props not_void_abst
T/props not_abbr_void
ty3/sty0 ty3_sty0
ty3/subst1 ty3_gen_cabbr
ty3/subst1 ty3_gen_cvoid
-wcpr0/fwd wcpr0_gen_sort
-wcpr0/fwd wcpr0_gen_head
-wcpr0/getl wcpr0_drop
-wcpr0/getl wcpr0_drop_back
-wcpr0/getl wcpr0_getl
-wcpr0/getl wcpr0_getl_back
wf3/clear wf3_clear_conf
wf3/clear clear_wf3_trans
wf3/fwd wf3_gen_sort1
(* SHIFT OF A CLOSURE *******************************************************)
let rec shift L T on L β match L with
-[ LSort β T
+[ LAtom β T
| LPair L I V β shift L (π{I} V. T)
].
(* Basic properties *********************************************************)
+(* Basic-1: was: flt_wf__q_ind *)
+
+(* Basic-1: was: flt_wf_ind *)
axiom cw_wf_ind: βR:lenvβtermβProp.
(βL2,T2. (βL1,T1. #[L1,T1] < #[L2,T2] β R L1 T1) β R L2 T2) β
βL,T. R L T.
+(* Basic-1: was: flt_shift *)
lemma cw_shift: βK,I,V,T. #[K. π{I} V, T] < #[K, π{I} V. T].
normalize //
qed.
#K #I #V #IHL #T
@transitive_le [3: @IHL |2: /2/ | skip ]
qed.
+
+(* Basic-1: removed theorems 6:
+ flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
+*)
(* local environments *)
inductive lenv: Type[0] β
-| LSort: lenv (* empty *)
+| LAtom: lenv (* empty *)
| LPair: lenv β bind2 β term β lenv (* binary binding construction *)
.
-interpretation "sort (local environment)" 'Star = LSort.
+interpretation "sort (local environment)" 'Star = LAtom.
interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T).
(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
let rec length L β match L with
-[ LSort β 0
+[ LAtom β 0
| LPair L _ _ β length L + 1
].
(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
let rec lw L β match L with
-[ LSort β 0
+[ LAtom β 0
| LPair L _ V β lw L + #[V]
].
interpretation "weight (local environment)" 'Weight L = (lw L).
+
+(* Basic-1: removed theorems 2: clt_cong clt_head *)
axiom tw_wf_ind: βR:termβProp.
(βT2. (βT1. #[T1] < #[T2] β R T1) β R T2) β
βT. R T.
+
+(* Basic-1: removed theorems 11:
+ wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
+ weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
+ removed local theorems 1: q_ind
+*)
/3/ qed.
(* Basic inversion lemmas ***************************************************)
+
+
+(* Basic-1: removed theorems 7:
+ iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans
+ iso_flats_lref_bind_false iso_flats_flat_bind_false
+*)
non associative with precedence 45
for @{ 'RDrop $L1 $d $e $L2 }.
+notation "hvbox( T1 break [ d , break e ] β« break T2 )"
+ non associative with precedence 45
+ for @{ 'PSubst $T1 $d $e $T2 }.
+
notation "hvbox( L β’ break term 90 T1 break [ d , break e ] β« break T2 )"
non associative with precedence 45
for @{ 'PSubst $L $T1 $d $e $T2 }.
lemma cpr_inv_lsort: βT1,T2. β β’ T1 β T2 β T1 β T2.
#T1 #T2 * #T #HT normalize #HT2
-<(tps_inv_refl0 β¦ HT2) -HT2 //
+<(tps_inv_refl_O2 β¦ HT2) -HT2 //
qed.
(* Basic forward lemmas *****************************************************)
"context-free parallel reduction (environment)"
'PRed L1 L2 = (ltpr L1 L2).
+(* Basic properties *********************************************************)
+
+lemma ltpr_refl: βL:lenv. L β L.
+#L elim L -L /2/
+qed.
+
(* Basic inversion lemmas ***************************************************)
-fact ltpr_inv_item1_aux: βL1,L2. L1 β L2 β βK1,I,V1. L1 = K1. π{I} V1 β
+fact ltpr_inv_atom1_aux: βL1,L2. L1 β L2 β L1 = β β L2 = β.
+#L1 #L2 * -L1 L2
+[ //
+| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+]
+qed.
+
+(* Basic-1: was: wcpr0_gen_sort *)
+lemma ltpr_inv_atom1: βL2. β β L2 β L2 = β.
+/2/ qed.
+
+fact ltpr_inv_pair1_aux: βL1,L2. L1 β L2 β βK1,I,V1. L1 = K1. π{I} V1 β
ββK2,V2. K1 β K2 & V1 β V2 & L2 = K2. π{I} V2.
#L1 #L2 * -L1 L2
[ #K1 #I #V1 #H destruct
]
qed.
-lemma ltpr_inv_item1: βK1,I,V1,L2. K1. π{I} V1 β L2 β
+(* Basic-1: was: wcpr0_gen_head *)
+lemma ltpr_inv_pair1: βK1,I,V1,L2. K1. π{I} V1 β L2 β
ββK2,V2. K1 β K2 & V1 β V2 & L2 = K2. π{I} V2.
/2/ qed.
+
+fact ltpr_inv_atom2_aux: βL1,L2. L1 β L2 β L2 = β β L1 = β.
+#L1 #L2 * -L1 L2
+[ //
+| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+]
+qed.
+
+lemma ltpr_inv_atom2: βL1. L1 β β β L1 = β.
+/2/ qed.
+
+fact ltpr_inv_pair2_aux: βL1,L2. L1 β L2 β βK2,I,V2. L2 = K2. π{I} V2 β
+ ββK1,V1. K1 β K2 & V1 β V2 & L1 = K1. π{I} V1.
+#L1 #L2 * -L1 L2
+[ #K2 #I #V2 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/
+]
+qed.
+
+lemma ltpr_inv_pair2: βL1,K2,I,V2. L1 β K2. π{I} V2 β
+ ββK1,V1. K1 β K2 & V1 β V2 & L1 = K1. π{I} V1.
+/2/ qed.
+
+(* Basic-1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
--- /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/tpr_lift.ma".
+include "Basic-2/reduction/ltpr.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Basic-1: was: wcpr0_drop *)
+lemma ltpr_drop_conf: βL1,K1,d,e. β[d, e] L1 β‘ K1 β βL2. L1 β L2 β
+ ββK2. β[d, e] L2 β‘ K2 & K1 β K2.
+#L1 #K1 #d #e #H elim H -H L1 K1 d e
+[ #d #e #X #H >(ltpr_inv_atom1 β¦ H) -H /2/
+| #L1 #K1 #I #V1 #HLK1 #_ #X #H
+ <(drop_inv_refl β¦ HLK1) -HLK1 K1;
+ elim (ltpr_inv_pair1 β¦ H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
+ elim (ltpr_inv_pair1 β¦ H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
+ elim (IHLK1 β¦ HL12) -IHLK1 HL12 /3/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
+ elim (ltpr_inv_pair1 β¦ H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
+ elim (tpr_inv_lift β¦ HV12 β¦ HWV1) -HV12 HWV1;
+ elim (IHLK1 β¦ HL12) -IHLK1 HL12 /3 width=5/
+]
+qed.
+
+(* Basic-1: was: wcpr0_drop_back *)
+lemma ltpr_drop_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 -H L1 K1 d e
+[ #d #e #X #H >(ltpr_inv_atom1 β¦ H) -H /2/
+| #L1 #K1 #I #V1 #HLK1 #_ #X #H
+ >(drop_inv_refl β¦ HLK1) -HLK1 L1;
+ elim (ltpr_inv_pair1 β¦ H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 β¦ HK12) -IHLK1 HK12 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
+ elim (ltpr_inv_pair1 β¦ H) -H #K2 #W2 #HK12 #HW12 #H destruct -X;
+ elim (lift_total W2 d e) #V2 #HWV2
+ lapply (tpr_lift β¦ HW12 β¦ HWV1 β¦ HWV2) -HW12 HWV1;
+ elim (IHLK1 β¦ HK12) -IHLK1 HK12 /3 width=5/
+]
+qed.
T1 = π{Abbr} V. T
| ββV,T. T β #i & T1 = π{Cast} V. T.
/2/ qed.
+(*
+pr0/fwd pr0_gen_sort
+pr0/fwd pr0_gen_lref
+pr0/fwd pr0_gen_abst
+pr0/fwd pr0_gen_appl
+pr0/fwd pr0_gen_cast
+pr0/fwd pr0_gen_abbr
+pr0/fwd pr0_gen_void
+pr0/fwd pr0_gen_lift
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta
+pr0/pr0 pr0_confluence__pr0_cong_delta
+pr0/pr0 pr0_confluence__pr0_upsilon_upsilon
+pr0/pr0 pr0_confluence__pr0_delta_delta
+pr0/pr0 pr0_confluence__pr0_delta_tau
+pr0/pr0 pr0_confluence
+pr0/props pr0_lift
+pr0/props pr0_subst0_back
+pr0/props pr0_subst0_fwd
+pr0/props pr0_subst0
+pr0/subst1 pr0_delta1
+pr0/subst1 pr0_subst1_back
+pr0/subst1 pr0_subst1_fwd
+pr0/subst1 pr0_subst1
+*)
\ No newline at end of file
| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1;
- <(tps_inv_refl1 β¦ HT2 ? ? ?) -HT2 T /2 width=5/
+ <(tps_inv_refl_SO2 β¦ HT2 ? ? ?) -HT2 T /2 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
| #V #T1 #T2 #_ #V0 #T0 #H destruct
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_tps.ma".
-include "Basic-2/reduction/tpr_lift.ma".
include "Basic-2/reduction/tpr_tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
elim (IH β¦ HT01 β¦ HT02) -HT01 HT02 IH // #T #HT1 #HT2
elim (tpr_tps_bind β¦ HV1 HT1 β¦ HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
elim (tpr_tps_bind β¦ HV2 HT2 β¦ HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (tps_conf β¦ HTU1 β¦ HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (tps_conf_eq β¦ HTU1 β¦ HTU2) -HTU1 HTU2 #U #HU1 #HU2
@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
qed.
(* *)
(**************************************************************************)
-include "Basic-2/reduction/ltpr.ma".
+include "Basic-2/substitution/tps_tps.ma".
+include "Basic-2/reduction/ltpr_drop.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-axiom tpr_tps_ltpr: βL1,L2. L1 β L2 β βT1,T2. T1 β T2 β
- βd,e,U1. L1 β’ T1 [d, e] β« U1 β
+axiom tpr_tps_ltpr: βT1,T2. T1 β T2 β
+ βL1,d,e,U1. L1 β’ T1 [d, e] β« U1 β
+ βL2. L1 β L2 β
ββU2. U1 β U2 & L2 β’ T2 [d, e] β« U2.
+(*
+#T1 #T2 #H elim H -H T1 T2
+[ #I #L1 #d #e #X #H
+ elim (tps_inv_atom1 β¦ H) -H
+ [ #H destruct -X /2/
+ | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
+ elim (ltpr_drop_conf β¦ HLK1 β¦ HL12) -HLK1 HL12 #X #HLK2 #H
+ elim (ltpr_inv_pair1 β¦ H) -H #K2 #V2 #_ #HV12 #H destruct -X;
+ elim (lift_total V2 0 (i+1)) #U2 #HVU2
+ lapply (tpr_lift β¦ HV12 β¦ HVU1 β¦ HVU2) -HV12 HVU1 #HU12
+ @ex2_1_intro [2: @HU12 | skip | /2/ ] (**) (* /3 width=6/ is too slow *)
+ ]
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 β¦ H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X;
+ elim (IHV12 β¦ HVW1 β¦ HL12) -IHV12 HVW1;
+ elim (IHT12 β¦ HTU1 β¦ HL12) -IHT12 HTU1 HL12 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 β¦ H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
+ elim (tps_inv_bind1 β¦ HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y;
+ elim (IHV12 β¦ HVV1 β¦ HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
+ elim (IHT12 β¦ HTT1 (L2. π{Abst} W) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ lapply (tps_leq_repl β¦ HTT2 (L2. π{Abbr} V2) ?) -HTT2 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 β¦ H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
+ elim (IHV12 β¦ HVV1 β¦ HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
+ elim (IHT12 β¦ HTT1 (L2. π{I} V2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+(*lapply (tps_leq_repl β¦ HTT2 (L2. π{I} VV2) ?) -HTT2 /2/ #HTT2 *)
+ elim (tps_conf_neq β¦ HTU2 β¦ HTT2 ?) -HTU2 HTT2 T2 /2/ #T2 #HUT2 #HTT2
+ @ex2_1_intro
+ [2: @tpr_delta [4: @HVV12 |5: @HTT12 |1,2: skip |6: ] (*|6: ]1,2: skip ]*)
+ |1: skip
+ |3: @tps_bind [@HVV2 | @HUT2 ]
+ ]
+*)
lemma tpr_tps_bind: βI,V1,V2,T1,T2,U1. V1 β V2 β T1 β T2 β
β. π{I} V1 β’ T1 [0, 1] β« U1 β
ββU2. U1 β U2 & β. π{I} V2 β’ T2 [0, 1] β« U2.
-/3 width=5/ qed.
+/3 width=7/ qed.
]
qed.
-(* Basic-1: removed theorems 18:
+(* Basic-1: removed theorems 49:
drop_skip_flat
cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
drop_clear drop_clear_O drop_clear_S
clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r
- clear_gen_all clear_clear clear_mono clear_trans clear_ctail
- clear_cle
+ clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle
+ getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans
+ getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt
+ getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev
+ drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge
+ getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O
+ getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le
+ getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono
*)
(* RELOCATION ***************************************************************)
+(* Basic-1: includes:
+ lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
+*)
inductive lift: term β nat β nat β term β Prop β
| lift_sort : βk,d,e. lift (βk) d e (βk)
| lift_lref_lt: βi,d,e. i < d β lift (#i) d e (#i)
(* Basic properties *********************************************************)
+(* Basic-1: was: lift_lref_gt *)
lemma lift_lref_ge_minus: βd,e,i. d + e β€ i β β[d, e] #(i - e) β‘ #i.
#d #e #i #H >(plus_minus_m_m i e) in β’ (? ? ? ? %) /3/
qed.
+(* Basic-1: was: lift_r *)
lemma lift_refl: βT,d. β[d, 0] T β‘ T.
#T elim T -T
[ * #i // #d elim (lt_or_ge i d) /2/
]
qed.
+(* Basic-1: was: lift_free (right to left) *)
lemma lift_split: βd1,e2,T1,T2. β[d1, e2] T1 β‘ T2 β βd2,e1.
d1 β€ d2 β d2 β€ d1 + e1 β e1 β€ e2 β
ββT. β[d1, e1] T1 β‘ T & β[d2, e2 - e1] T β‘ T2.
]
qed.
+(* Basic-1: was: lift_gen_sort *)
lemma lift_inv_sort2: βd,e,T1,k. β[d,e] T1 β‘ βk β T1 = βk.
/2 width=5/ qed.
]
qed.
+(* Basic-1: was: lift_gen_lref *)
lemma lift_inv_lref2: βd,e,T1,i. β[d,e] T1 β‘ #i β
(i < d β§ T1 = #i) β¨ (d + e β€ i β§ T1 = #(i - e)).
/2/ qed.
+(* Basic-1: was: lift_gen_lref_lt *)
lemma lift_inv_lref2_lt: βd,e,T1,i. β[d,e] T1 β‘ #i β i < d β T1 = #i.
#d #e #T1 #i #H elim (lift_inv_lref2 β¦ H) -H * //
#Hdi #_ #Hid lapply (le_to_lt_to_lt β¦ Hdi Hid) -Hdi Hid #Hdd
elim (plus_lt_false β¦ Hdd)
qed.
+(* Basic-1: was: lift_gen_lref_false *)
+
+(* Basic-1: was: lift_gen_lref_ge *)
lemma lift_inv_lref2_ge: βd,e,T1,i. β[d,e] T1 β‘ #i β d + e β€ i β T1 = #(i - e).
#d #e #T1 #i #H elim (lift_inv_lref2 β¦ H) -H * //
#Hid #_ #Hdi lapply (le_to_lt_to_lt β¦ Hdi Hid) -Hdi Hid #Hdd
]
qed.
+(* Basic-1: was: lift_gen_bind *)
lemma lift_inv_bind2: βd,e,T1,I,V2,U2. β[d,e] T1 β‘ π{I} V2. U2 β
ββV1,U1. β[d,e] V1 β‘ V2 & β[d+1,e] U1 β‘ U2 &
T1 = π{I} V1. U1.
]
qed.
+(* Basic-1: was: lift_gen_flat *)
lemma lift_inv_flat2: βd,e,T1,I,V2,U2. β[d,e] T1 β‘ π{I} V2. U2 β
ββV1,U1. β[d,e] V1 β‘ V2 & β[d,e] U1 β‘ U2 &
T1 = π{I} V1. U1.
/2/ qed.
+
+(* Basic-1: removed theorems 7:
+ lift_head lift_gen_head
+ lift_weight_map lift_weight lift_weight_add lift_weight_add_O
+ lift_tlt_dx
+*)
(* Main properies ***********************************************************)
+(* Basic-1: was: lift_inj *)
theorem lift_inj: βd,e,T1,U. β[d,e] T1 β‘ U β βT2. β[d,e] T2 β‘ U β T1 = T2.
#d #e #T1 #U #H elim H -H d e T1 U
[ #k #d #e #X #HX
]
qed.
+(* Basic-1: was: lift_gen_lift *)
theorem lift_div_le: βd1,e1,T1,T. β[d1, e1] T1 β‘ T β
βd2,e2,T2. β[d2 + e1, e2] T2 β‘ T β
d1 β€ d2 β
]
qed.
+(* Basic-1: was: lift_free (left to right) *)
theorem lift_trans_be: βd1,e1,T1,T. β[d1, e1] T1 β‘ T β
βd2,e2,T2. β[d2, e2] T β‘ T2 β
d1 β€ d2 β d2 β€ d1 + e1 β β[d1, e1 + e2] T1 β‘ T2.
]
qed.
+(* Basic-1: was: lift_d (right to left) *)
theorem lift_trans_le: βd1,e1,T1,T. β[d1, e1] T1 β‘ T β
βd2,e2,T2. β[d2, e2] T β‘ T2 β d2 β€ d1 β
ββT0. β[d2, e2] T1 β‘ T0 & β[d1 + e2, e1] T0 β‘ T2.
]
qed.
+(* Basic-1: was: lift_d (left to right) *)
theorem lift_trans_ge: βd1,e1,T1,T. β[d1, e1] T1 β‘ T β
βd2,e2,T2. β[d2, e2] T β‘ T2 β d1 + e1 β€ d2 β
ββT0. β[d2 - e1, e2] T1 β‘ T0 & β[d1, e1] T0 β‘ 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/substitution/tps.ma".
+
+(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
+
+(* Basic-1: includes: csubst1_bind *)
+inductive ltps: lenv β nat β nat β lenv β Prop β
+| ltps_atom: βd,e. ltps (β) d e (β)
+| ltps_pair: βL,I,V. ltps (L. π{I} V) 0 0 (L. π{I} V)
+| ltps_tps2: βL1,L2,I,V1,V2,e.
+ ltps L1 0 e L2 β L2 β’ V1 [0, e] β« V2 β
+ ltps (L1. π{I} V1) 0 (e + 1) L2. π{I} V2
+| ltps_tps1: βL1,L2,I,V1,V2,d,e.
+ ltps L1 d e L2 β L2 β’ V1 [d, e] β« V2 β
+ ltps (L1. π{I} V1) (d + 1) e (L2. π{I} V2)
+.
+
+interpretation "parallel substritution (local environment)"
+ 'PSubst L1 d e L2 = (ltps L1 d e L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltps_tps2_lt: βL1,L2,I,V1,V2,e.
+ L1 [0, e - 1] β« L2 β L2 β’ V1 [0, e - 1] β« V2 β
+ 0 < e β L1. π{I} V1 [0, e] β« L2. π{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2/
+qed.
+
+lemma ltps_tps1_lt: βL1,L2,I,V1,V2,d,e.
+ L1 [d - 1, e] β« L2 β L2 β’ V1 [d - 1, e] β« V2 β
+ 0 < d β L1. π{I} V1 [d, e] β« L2. π{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2/
+qed.
+
+(* Basic-1: was by definition: csubst1_refl *)
+lemma ltps_refl: βL,d,e. L [d, e] β« L.
+#L elim L -L //
+#L #I #V #IHL * /2/ * /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact ltps_inv_refl_O2_aux: βd,e,L1,L2. L1 [d, e] β« L2 β e = 0 β L1 = L2.
+#d #e #L1 #L2 #H elim H -H d e L1 L2 //
+[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ #H
+ elim (plus_S_eq_O_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct -e
+ >(IHL12 ?) -IHL12 // >(tps_inv_refl_O2 β¦ HV12) //
+]
+qed.
+
+lemma ltps_inv_refl_O2: βd,L1,L2. L1 [d, 0] β« L2 β L1 = L2.
+/2/ qed.
+
+fact ltps_inv_atom1_aux: βd,e,L1,L2.
+ L1 [d, e] β« L2 β L1 = β β L2 = β.
+#d #e #L1 #L2 * -d e L1 L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma drop_inv_atom1: βd,e,L2. β [d, e] β« L2 β L2 = β.
+/2 width=5/ qed.
+
+fact ltps_inv_tps21_aux: βd,e,L1,L2. L1 [d, e] β« L2 β d = 0 β 0 < e β
+ βK1,I,V1. L1 = K1. π{I} V1 β
+ ββK2,V2. K1 [0, e - 1] β« K2 &
+ K2 β’ V1 [0, e - 1] β« V2 &
+ L2 = K2. π{I} V2.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct -L1 I V1 /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false β¦ H)
+]
+qed.
+
+lemma ltps_inv_tps21: βe,K1,I,V1,L2. K1. π{I} V1 [0, e] β« L2 β 0 < e β
+ ββK2,V2. K1 [0, e - 1] β« K2 & K2 β’ V1 [0, e - 1] β« V2 &
+ L2 = K2. π{I} V2.
+/2 width=5/ qed.
+
+fact ltps_inv_tps11_aux: βd,e,L1,L2. L1 [d, e] β« L2 β 0 < d β
+ βI,K1,V1. L1 = K1. π{I} V1 β
+ ββK2,V2. K1 [d - 1, e] β« K2 &
+ K2 β’ V1 [d - 1, e] β« V2 &
+ L2 = K2. π{I} V2.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #I #K1 #V1 #H destruct
+| #L #I #V #H elim (lt_refl_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct -L1 I V1
+ /2 width=5/
+]
+qed.
+
+lemma ltps_inv_tps11: βd,e,I,K1,V1,L2. K1. π{I} V1 [d, e] β« L2 β 0 < d β
+ ββK2,V2. K1 [d - 1, e] β« K2 &
+ K2 β’ V1 [d - 1, e] β« V2 &
+ L2 = K2. π{I} V2.
+/2/ qed.
+
+fact ltps_inv_atom2_aux: βd,e,L1,L2.
+ L1 [d, e] β« L2 β L2 = β β L1 = β.
+#d #e #L1 #L2 * -d e L1 L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma drop_inv_atom2: βd,e,L1. L1 [d, e] β« β β L1 = β.
+/2 width=5/ qed.
+
+fact ltps_inv_tps22_aux: βd,e,L1,L2. L1 [d, e] β« L2 β d = 0 β 0 < e β
+ βK2,I,V2. L2 = K2. π{I} V2 β
+ ββK1,V1. K1 [0, e - 1] β« K2 &
+ K2 β’ V1 [0, e - 1] β« V2 &
+ L1 = K1. π{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false β¦ H)
+]
+qed.
+
+lemma ltps_inv_tps22: βe,L1,K2,I,V2. L1 [0, e] β« K2. π{I} V2 β 0 < e β
+ ββK1,V1. K1 [0, e - 1] β« K2 & K2 β’ V1 [0, e - 1] β« V2 &
+ L1 = K1. π{I} V1.
+/2 width=5/ qed.
+
+fact ltps_inv_tps12_aux: βd,e,L1,L2. L1 [d, e] β« L2 β 0 < d β
+ βI,K2,V2. L2 = K2. π{I} V2 β
+ ββK1,V1. K1 [d - 1, e] β« K2 &
+ K2 β’ V1 [d - 1, e] β« V2 &
+ L1 = K1. π{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #I #K2 #V2 #H destruct
+| #L #I #V #H elim (lt_refl_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false β¦ H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2
+ /2 width=5/
+]
+qed.
+
+lemma ltps_inv_tps12: βL1,K2,I,V2,d,e. L1 [d, e] β« K2. π{I} V2 β 0 < d β
+ ββK1,V1. K1 [d - 1, e] β« K2 &
+ K2 β’ V1 [d - 1, e] β« V2 &
+ L1 = K1. π{I} V1.
+/2/ qed.
+
+(* Basic-1: removed theorems 27:
+ 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_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
+ csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_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
+
+*)
--- /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/substitution/ltps.ma".
+
+(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
+
+lemma ltps_drop_conf_ge: βL0,L1,d1,e1. L0 [d1, e1] β« L1 β
+ βL2,e2. β[0, e2] L0 β‘ L2 β
+ d1 + e1 β€ e2 β β[0, e2] L1 β‘ L2.
+#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 β¦ H) -H //
+| //
+| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
+ lapply (plus_le_weak β¦ He12) #He2
+ lapply (drop_inv_drop1 β¦ H ?) -H // #HK0L2
+ lapply (IHK01 β¦ HK0L2 ?) -IHK01 HK0L2 /2/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
+ lapply (plus_le_weak β¦ Hd1e2) #He2
+ lapply (drop_inv_drop1 β¦ H ?) -H // #HK0L2
+ lapply (IHK01 β¦ HK0L2 ?) -IHK01 HK0L2 /2/
+]
+qed.
+
+lemma ltps_drop_trans_ge: βL1,L0,d1,e1. L1 [d1, e1] β« L0 β
+ βL2,e2. β[0, e2] L0 β‘ L2 β
+ d1 + e1 β€ e2 β β[0, e2] L1 β‘ L2.
+#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 β¦ H) -H //
+| //
+| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
+ lapply (plus_le_weak β¦ He12) #He2
+ lapply (drop_inv_drop1 β¦ H ?) -H // #HK0L2
+ lapply (IHK10 β¦ HK0L2 ?) -IHK10 HK0L2 /2/
+| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
+ lapply (plus_le_weak β¦ Hd1e2) #He2
+ lapply (drop_inv_drop1 β¦ H ?) -H // #HK0L2
+ lapply (IHK10 β¦ HK0L2 ?) -IHK10 HK0L2 /2/
+]
+qed.
+
+lemma ltps_drop_conf_be: βL0,L1,d1,e1. L0 [d1, e1] β« L1 β
+ βL2,e2. β[0, e2] L0 β‘ L2 β d1 β€ e2 β e2 β€ d1 + e1 β
+ ββL. L2 [0, d1 + e1 - e2] β« L & β[0, e2] L1 β‘ L.
+#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 β¦ H) -H /2/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq β¦ He2) -He2 #H destruct -e2;
+ lapply (drop_inv_refl β¦ HL2) -HL2 #H destruct -L2 /2/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
+ lapply (drop_inv_O1 β¦ H) -H * * #He2 #HK0L2
+ [ destruct -IHK01 He21 e2 L2 <minus_n_O /3/
+ | -HK01 HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 β¦ HK0L2 ? ?) -IHK01 HK0L2 /3/
+ ]
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
+ lapply (plus_le_weak β¦ Hd1e2) #He2
+ <minus_le_minus_minus_comm //
+ lapply (drop_inv_drop1 β¦ H ?) -H // #HK0L2
+ elim (IHK01 β¦ HK0L2 ? ?) -IHK01 HK0L2 /3/
+]
+qed.
+
+lemma ltps_drop_trans_be: βL1,L0,d1,e1. L1 [d1, e1] β« L0 β
+ βL2,e2. β[0, e2] L0 β‘ L2 β d1 β€ e2 β e2 β€ d1 + e1 β
+ ββL. L [0, d1 + e1 - e2] β« L2 & β[0, e2] L1 β‘ L.
+#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 β¦ H) -H /2/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq β¦ He2) -He2 #H destruct -e2;
+ lapply (drop_inv_refl β¦ HL2) -HL2 #H destruct -L2 /2/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
+ lapply (drop_inv_O1 β¦ H) -H * * #He2 #HK0L2
+ [ destruct -IHK10 He21 e2 L2 <minus_n_O /3/
+ | -HK10 HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 β¦ HK0L2 ? ?) -IHK10 HK0L2 /3/
+ ]
+| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
+ lapply (plus_le_weak β¦ Hd1e2) #He2
+ <minus_le_minus_minus_comm //
+ lapply (drop_inv_drop1 β¦ H ?) -H // #HK0L2
+ elim (IHK10 β¦ HK0L2 ? ?) -IHK10 HK0L2 /3/
+]
+qed.
+
+lemma ltps_drop_conf_le: βL0,L1,d1,e1. L0 [d1, e1] β« L1 β
+ βL2,e2. β[0, e2] L0 β‘ L2 β e2 β€ d1 β
+ ββL. L2 [d1 - e2, e1] β« L & β[0, e2] L1 β‘ L.
+#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 β¦ H) -H /2/
+| /2/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
+ lapply (le_n_O_to_eq β¦ He2) -He2 #He2 destruct -e2;
+ lapply (drop_inv_refl β¦ H) -H #H destruct -L2 /3/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
+ lapply (drop_inv_O1 β¦ H) -H * * #He2 #HK0L2
+ [ destruct -IHK01 He2d1 e2 L2 <minus_n_O /3/
+ | -HK01 HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 β¦ HK0L2 ?) -IHK01 HK0L2 /3/
+ ]
+]
+qed.
+
+lemma ltps_trans_conf_le: βL1,L0,d1,e1. L1 [d1, e1] β« L0 β
+ βL2,e2. β[0, e2] L0 β‘ L2 β e2 β€ d1 β
+ ββL. L [d1 - e2, e1] β« L2 & β[0, e2] L1 β‘ L.
+#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
+[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 β¦ H) -H /2/
+| /2/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
+ lapply (le_n_O_to_eq β¦ He2) -He2 #He2 destruct -e2;
+ lapply (drop_inv_refl β¦ H) -H #H destruct -L2 /3/
+| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
+ lapply (drop_inv_O1 β¦ H) -H * * #He2 #HK0L2
+ [ destruct -IHK10 He2d1 e2 L2 <minus_n_O /3/
+ | -HK10 HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 β¦ HK0L2 ?) -IHK10 HK0L2 /3/
+ ]
+]
+qed.
(* Basic inversion lemmas ***************************************************)
-fact tps_inv_lref1_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β βi. T1 = #i β
- T2 = #i β¨
- ββK,V. d β€ i & i < d + e &
- β[O, i] L β‘ K. π{Abbr} V &
- β[O, i + 1] V β‘ T2.
+fact tps_inv_atom1_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β βI. T1 = π{I} β
+ T2 = π{I} β¨
+ ββK,V,i. d β€ i & i < d + e &
+ β[O, i] L β‘ K. π{Abbr} V &
+ β[O, i + 1] V β‘ T2 &
+ I = LRef i.
#L #T1 #T2 #d #e * -L T1 T2 d e
-[ #L #I #d #e #i #H destruct -I /2/
-| #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #j #H destruct -i /3/
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+[ #L #I #d #e #J #H destruct -I /2/
+| #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #I #H destruct -I /3 width=8/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #J #H destruct
]
qed.
+lemma tps_inv_atom1: βL,T2,I,d,e. L β’ π{I} [d, e] β« T2 β
+ T2 = π{I} β¨
+ ββK,V,i. d β€ i & i < d + e &
+ β[O, i] L β‘ K. π{Abbr} V &
+ β[O, i + 1] V β‘ T2 &
+ I = LRef i.
+/2/ qed.
+
+
+(* Basic-1: was: subst1_gen_sort *)
+lemma tps_inv_sort1: βL,T2,k,d,e. L β’ βk [d, e] β« T2 β T2 = βk.
+#L #T2 #k #d #e #H
+elim (tps_inv_atom1 β¦ H) -H //
+* #K #V #i #_ #_ #_ #_ #H destruct
+qed.
+
+(* Basic-1: was: subst1_gen_lref *)
lemma tps_inv_lref1: βL,T2,i,d,e. L β’ #i [d, e] β« T2 β
T2 = #i β¨
ββK,V. d β€ i & i < d + e &
β[O, i] L β‘ K. π{Abbr} V &
β[O, i + 1] V β‘ T2.
-/2/ qed.
+#L #T2 #i #d #e #H
+elim (tps_inv_atom1 β¦ H) -H /2/
+* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct -i /3/
+qed.
fact tps_inv_bind1_aux: βd,e,L,U1,U2. L β’ U1 [d, e] β« U2 β
βI,V1,T1. U1 = π{I} V1. T1 β
U2 = π{I} V2. T2.
/2/ qed.
-fact tps_inv_refl0_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β e = 0 β T1 = T2.
+fact tps_inv_refl_O2_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β e = 0 β T1 = T2.
#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct -e;
]
qed.
-lemma tps_inv_refl0: βL,T1,T2,d. L β’ T1 [d, 0] β« T2 β T1 = T2.
+lemma tps_inv_refl_O2: βL,T1,T2,d. L β’ T1 [d, 0] β« T2 β T1 = T2.
/2 width=6/ qed.
+
+(* Basic-1: removed theorems 23:
+ subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
+ subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
+ subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
+ subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
+ subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
+ subst0_confluence_lift subst0_tlt
+ subst1_head subst1_gen_head
+*)
(* Advanced inversion lemmas ************************************************)
-fact tps_inv_refl1_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β e = 1 β
- βK,V. β[0, d] L β‘ K. π{Abst} V β T1 = T2.
+fact tps_inv_refl_SO2_aux: βL,T1,T2,d,e. L β’ T1 [d, e] β« T2 β e = 1 β
+ βK,V. β[0, d] L β‘ K. π{Abst} V β T1 = T2.
#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ //
| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
]
qed.
-lemma tps_inv_refl1: βL,T1,T2,d. L β’ T1 [d, 1] β« T2 β
- βK,V. β[0, d] L β‘ K. π{Abst} V β T1 = T2.
+lemma tps_inv_refl_SO2: βL,T1,T2,d. L β’ T1 [d, 1] β« T2 β
+ βK,V. β[0, d] L β‘ K. π{Abst} V β T1 = T2.
/2 width=8/ qed.
(* Main properties **********************************************************)
-theorem tps_conf: βL,T0,T1,d,e. L β’ T0 [d, e] β« T1 β βT2. L β’ T0 [d, e] β« T2 β
- ββT. L β’ T1 [d, e] β« T & L β’ T2 [d, e] β« T.
-#L #T0 #T1 #d #e #H elim H -H L T0 T1 d e
+(* Basic-1: was: subst1_confluence_eq *)
+theorem tps_conf_eq: βL,T0,T1,d1,e1. L β’ T0 [d1, e1] β« T1 β
+ βT2,d2,e2. L β’ T0 [d2, e2] β« T2 β
+ ββT. L β’ T1 [d2, e2] β« T & L β’ T2 [d1, e1] β« T.
+#L #T0 #T1 #d1 #e1 #H elim H -H L T0 T1 d1 e1
[ /2/
-| #L #K1 #V1 #T1 #i1 #d #e #Hdi1 #Hi1de #HLK1 #HVT1 #T2 #H
+| #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H
elim (tps_inv_lref1 β¦ H) -H
[ #HX destruct -T2 /4/
- | * #K2 #V2 #_ #_ #HLK2 #HVT2
- lapply (drop_mono β¦ HLK1 β¦ HLK2) -HLK1 #H destruct -V1 K1
- >(lift_mono β¦ HVT1 β¦ HVT2) -HVT1 /2/
+ | -Hd1 Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2
+ lapply (drop_mono β¦ HLK1 β¦ HLK2) -HLK1 HLK2 #H destruct -V1 K1
+ >(lift_mono β¦ HVT1 β¦ HVT2) -HVT1 HVT2 /2/
]
-| #L #I #V0 #V1 #T0 #T1 #d #e #_ #_ #IHV01 #IHT01 #X #HX
+| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_bind1 β¦ HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
elim (IHV01 β¦ HV02) -IHV01 HV02 #V #HV1 #HV2
elim (IHT01 β¦ HT02) -IHT01 HT02 #T #HT1 #HT2
- @ex2_1_intro
- [2: @tps_bind [4: @(tps_leq_repl β¦ HT1) /2/ |2: skip ]
- |1: skip
- |3: @tps_bind [2: @(tps_leq_repl β¦ HT2) /2/ ]
- ] // (**) (* /5/ is too slow *)
-| #L #I #V0 #V1 #T0 #T1 #d #e #_ #_ #IHV01 #IHT01 #X #HX
+ lapply (tps_leq_repl β¦ HT1 (L. π{I} V1) ?) -HT1 /2/
+ lapply (tps_leq_repl β¦ HT2 (L. π{I} V2) ?) -HT2 /3 width=5/
+| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_flat1 β¦ HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
elim (IHV01 β¦ HV02) -IHV01 HV02;
elim (IHT01 β¦ HT02) -IHT01 HT02 /3 width=5/
]
qed.
+(* Basic-1: was: subst1_confluence_neq *)
+theorem tps_conf_neq: βL1,T0,T1,d1,e1. L1 β’ T0 [d1, e1] β« T1 β
+ βL2,T2,d2,e2. L2 β’ T0 [d2, e2] β« T2 β
+ (d1 + e1 β€ d2 β¨ d2 + e2 β€ d1) β
+ ββT. L2 β’ T1 [d2, e2] β« T & L1 β’ T2 [d1, e1] β« T.
+#L1 #T0 #T1 #d1 #e1 #H elim H -H L1 T0 T1 d1 e1
+[ /2/
+| #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2
+ elim (tps_inv_lref1 β¦ H1) -H1
+ [ #H destruct -T2 /4/
+ | -HLK1 HVT1 * #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded
+ [ -Hd1 Hde2;
+ lapply (transitive_le β¦ Hded Hd2) -Hded Hd2 #H
+ lapply (lt_to_le_to_lt β¦ Hde1 H) -Hde1 H #H
+ elim (lt_refl_false β¦ H)
+ | -Hd2 Hde1;
+ lapply (transitive_le β¦ Hded Hd1) -Hded Hd1 #H
+ lapply (lt_to_le_to_lt β¦ Hde2 H) -Hde2 H #H
+ elim (lt_refl_false β¦ H)
+ ]
+ ]
+| #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
+ elim (tps_inv_bind1 β¦ HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
+ elim (IHV01 β¦ HV02 H) -IHV01 HV02 #V #HV1 #HV2
+ elim (IHT01 β¦ HT02 ?) -IHT01 HT02
+ [ -H #T #HT1 #HT2
+ lapply (tps_leq_repl β¦ HT1 (L2. π{I} V1) ?) -HT1 /2/
+ lapply (tps_leq_repl β¦ HT2 (L1. π{I} V2) ?) -HT2 /3 width=5/
+ | -HV1 HV2 >plus_plus_comm_23 >plus_plus_comm_23 in β’ (? ? %) elim H -H #H
+ [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3/ is too slow *)
+ ]
+| #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
+ elim (tps_inv_flat1 β¦ HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
+ elim (IHV01 β¦ HV02 H) -IHV01 HV02;
+ elim (IHT01 β¦ HT02 H) -IHT01 HT02 H /3 width=5/
+]
+qed.
+
theorem tps_trans_down: βL,T1,T0,d1,e1. L β’ T1 [d1, e1] β« T0 β
βT2,d2,e2. L β’ T0 [d2, e2] β« T2 β d2 + e2 β€ d1 β
ββT. L β’ T1 [d2, e2] β« T & L β’ T [d1, e1] β« T2.
projects / helm.git / commitdiff