(* *)
(**************************************************************************)
-include "Basic-2/grammar/lenv.ma".
+include "Basic_2/grammar/lenv.ma".
(* SHIFT OF A CLOSURE *******************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/lenv_weight.ma".
-include "Basic-2/grammar/cl_shift.ma".
+include "Basic_2/grammar/lenv_weight.ma".
+include "Basic_2/grammar/cl_shift.ma".
(* WEIGHT OF A CLOSURE ******************************************************)
(* Basic properties *********************************************************)
-(* Basic-1: was: flt_wf__q_ind *)
+(* Basic_1: was: flt_wf__q_ind *)
-(* Basic-1: was: flt_wf_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 *)
+(* Basic_1: was: flt_shift *)
lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T].
normalize //
qed.
@transitive_le [3: @IHL |2: /2/ | skip ]
qed.
-(* Basic-1: removed theorems 6:
+(* Basic_1: removed theorems 6:
flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
*)
* [ suggested invocation to start formal specifications with ]
*)
-include "Ground-2/list.ma".
-include "Ground-2/star.ma".
-include "Basic-2/notation.ma".
+include "Ground_2/list.ma".
+include "Ground_2/star.ma".
+include "Basic_2/notation.ma".
(* ITEMS ********************************************************************)
coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
-(* Basic-1: removed theorems 19:
+(* Basic_1: removed theorems 19:
s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc
s_arith0 s_arith1
r_S r_plus r_plus_sym r_minus r_dis s_r r_arith0 r_arith1
(* *)
(**************************************************************************)
-include "Basic-2/grammar/term.ma".
+include "Basic_2/grammar/term.ma".
(* LOCAL ENVIRONMENTS *******************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/lenv.ma".
+include "Basic_2/grammar/lenv.ma".
(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/term_weight.ma".
-include "Basic-2/grammar/lenv.ma".
+include "Basic_2/grammar/term_weight.ma".
+include "Basic_2/grammar/lenv.ma".
(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
interpretation "weight (local environment)" 'Weight L = (lw L).
-(* Basic-1: removed theorems 2: clt_cong clt_head *)
+(* Basic_1: removed theorems 2: clt_cong clt_head *)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "Basic-2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-
-inductive leq: nat → nat → relation lenv ≝
-| leq_sort: ∀d,e. leq d e (⋆) (⋆)
-| leq_OO: ∀L1,L2. leq 0 0 L1 L2
-| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 →
- leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V)
-| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
-.
-
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2).
-
-definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R.
- ∀L1,s1,s2. R L1 s1 s2 →
- ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2.
-
-(* Basic properties *********************************************************)
-
-lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -H s2
-[ /3 width=5/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
- lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
-]
-qed.
-
-lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L /2/
-| #d #IHd #e #L elim L -L /2/
-]
-qed.
-
-lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
-qed.
-
-lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
-
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
+
+inductive lsubs: nat → nat → relation lenv ≝
+| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
+| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2
+| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
+ lsubs 0 (e + 1) (L1. 𝕓{Abbr} V) (L2.𝕓{Abbr} V)
+| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
+ lsubs 0 (e + 1) (L1. 𝕓{Abst} V1) (L2.𝕓{I} V2)
+| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+ lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+.
+
+interpretation "local environment refinement (substitution)" 'SubEq L1 d e L2 = (lsubs d e L1 L2).
+
+definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L1,s1,s2. R L1 s1 s2 →
+ ∀L2,d,e. L1 [d, e] ≼ L2 → R L2 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -H s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+ lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
+]
+qed.
+
+lemma lsubs_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
+ L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
+#L1 #L2 #e #HL12 #I #V elim I -I /2/
+qed.
+
+lemma lsubs_refl: ∀d,e,L. L [d, e] ≼ L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L /2/
+| #d #IHd #e #L elim L -L /2/
+]
+qed.
+
+lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
+ ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≼ L2. 𝕓{I2} V2.
+
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
(* *)
(**************************************************************************)
-include "Ground-2/list.ma".
+include "Ground_2/list.ma".
(* SORT HIERARCHY ***********************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/item.ma".
+include "Basic_2/grammar/item.ma".
(* TERMS ********************************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/term.ma".
+include "Basic_2/grammar/term.ma".
(* SIMPLE (NEUTRAL) TERMS ***************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/term.ma".
+include "Basic_2/grammar/term.ma".
(* WEIGHT OF A TERM *********************************************************)
(∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
∀T. R T.
-(* Basic-1: removed theorems 11:
+(* 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
(* *)
(**************************************************************************)
-include "Basic-2/grammar/term_simple.ma".
+include "Basic_2/grammar/term_simple.ma".
(* HOMOMORPHIC TERMS ********************************************************)
(* Basic inversion lemmas ***************************************************)
-(* Basic-1: removed theorems 7:
+(* 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 @{ 'Simple $T }.
-notation "hvbox( T1 break [ d , break e ] â\89\88 break T2 )"
+notation "hvbox( T1 break [ d , break e ] â\89¼ break T2 )"
non associative with precedence 45
- for @{ 'Eq $T1 $d $e $T2 }.
+ for @{ 'SubEq $T1 $d $e $T2 }.
(* Substitution *************************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/grammar/cl_shift.ma".
-include "Basic-2/unfold/tpss.ma".
-include "Basic-2/reduction/tpr.ma".
+include "Basic_2/grammar/cl_shift.ma".
+include "Basic_2/unfold/tpss.ma".
+include "Basic_2/reduction/tpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-(* Basic-1: includes: pr2_delta1 *)
+(* Basic_1: includes: pr2_delta1 *)
definition cpr: lenv → relation term ≝
λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2.
(* Basic properties *********************************************************)
-(* Basic-1: was by definition: pr2_free *)
+(* Basic_1: was by definition: pr2_free *)
lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
/2/ qed.
/2/ qed.
(* Note: new property *)
-(* Basic-1: was only: pr2_thin_dx *)
+(* Basic_1: was only: pr2_thin_dx *)
lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
(* Basic inversion lemmas ***************************************************)
-(* Basic-1: was: pr2_gen_csort *)
+(* Basic_1: was: pr2_gen_csort *)
lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
#T1 #T2 * #T #HT normalize #HT2
<(tpss_inv_refl_O2 … HT2) -HT2 //
qed.
-(* Basic-1: was: pr2_gen_sort *)
+(* Basic_1: was: pr2_gen_sort *)
lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
#L #T2 #k * #X #H
>(tpr_inv_atom1 … H) -H #H
>(tpss_inv_sort1 … H) -H //
qed.
-(* Basic-1: was: pr2_gen_cast *)
+(* Basic_1: was: pr2_gen_cast *)
lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 &
U2 = 𝕔{Cast} V2. T2
elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
qed.
-(* Basic-1: removed theorems 5:
+(* Basic_1: removed theorems 5:
pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
- Basic-1: removed local theorems 3:
+ Basic_1: removed local theorems 3:
pr2_free_free pr2_free_delta pr2_delta_delta
*)
(* *)
(**************************************************************************)
-include "Basic-2/reduction/tpr_tpr.ma".
-include "Basic-2/reduction/cpr.ma".
+include "Basic_2/reduction/tpr_tpr.ma".
+include "Basic_2/reduction/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *)
qed.
-(* Basic-1: was only: pr2_gen_cbind *)
+(* Basic_1: was only: pr2_gen_cbind *)
lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_leq_repl_dx … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
+lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
lapply (tpss_tps … HT0) -HT0 #HT0
@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2/ ] (**) (* /3 width=5/ is too slow *)
qed.
(* Main properties **********************************************************)
-(* Basic-1: was: pr2_confluence *)
+(* Basic_1: was: pr2_confluence *)
theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ⇒ T1 → L ⊢ U0 ⇒ T2 →
∃∃T. L ⊢ T1 ⇒ T & L ⊢ T2 ⇒ T.
#L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
(* *)
(**************************************************************************)
-include "Basic-2/unfold/tpss_lift.ma".
-include "Basic-2/reduction/tpr_lift.ma".
-include "Basic-2/reduction/cpr.ma".
+include "Basic_2/unfold/tpss_lift.ma".
+include "Basic_2/reduction/tpr_lift.ma".
+include "Basic_2/reduction/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* Advanced inversion lemmas ************************************************)
-(* Basic-1: was: pr2_gen_lref *)
+(* Basic_1: was: pr2_gen_lref *)
lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
T2 = #i ∨
∃∃K,V1,T1. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 &
* /3 width=6/
qed.
-(* Basic-1: was: pr2_gen_abst *)
+(* Basic_1: was: pr2_gen_abst *)
lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
/2/ qed.
(* Relocation properties ****************************************************)
-(* Basic-1: was: pr2_lift *)
+(* Basic_1: was: pr2_lift *)
-(* Basic-1: was: pr2_gen_lift *)
+(* Basic_1: was: pr2_gen_lift *)
(* *)
(**************************************************************************)
-include "Basic-2/reduction/cpr.ma".
+include "Basic_2/reduction/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
(* *)
(**************************************************************************)
-include "Basic-2/reduction/tpr.ma".
+include "Basic_2/reduction/tpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
]
qed.
-(* Basic-1: was: wcpr0_gen_sort *)
+(* Basic_1: was: wcpr0_gen_sort *)
lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆.
/2/ qed.
]
qed.
-(* Basic-1: was: wcpr0_gen_head *)
+(* 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.
∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
/2/ qed.
-(* Basic-1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
+(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
(* *)
(**************************************************************************)
-include "Basic-2/reduction/tpr_lift.ma".
-include "Basic-2/reduction/ltpr.ma".
+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 *)
+(* 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
]
qed.
-(* Basic-1: was: wcpr0_drop_back *)
+(* 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
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps.ma".
+include "Basic_2/substitution/tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-(* Basic-1: includes: pr0_delta1 *)
+(* Basic_1: includes: pr0_delta1 *)
inductive tpr: relation term ≝
| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
/2/ qed.
-(* Basic-1: was by definition: pr0_refl *)
+(* Basic_1: was by definition: pr0_refl *)
lemma tpr_refl: ∀T. T ⇒ T.
#T elim T -T //
#I elim I -I /2/
]
qed.
-(* Basic-1: was: pr0_gen_sort pr0_gen_lref *)
+(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
/2/ qed.
∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
/2/ qed.
-(* Basic-1: was pr0_gen_abbr *)
+(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
(∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
| (U0 ⇒ U2 ∧ I = Cast).
/2/ qed.
-(* Basic-1: was pr0_gen_appl *)
+(* Basic_1: was pr0_gen_appl *)
lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
U2 = 𝕔{Appl} V2. T2
elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
qed.
-(* Basic-1: was: pr0_gen_cast *)
+(* Basic_1: was: pr0_gen_cast *)
lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
(∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2)
∨ T1 ⇒ U2.
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
/2/ qed.
-(* Basic-1: removed theorems 3:
+(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
- Basic-1: removed local theorems: 1: pr0_delta_tau
+ Basic_1: removed local theorems: 1: pr0_delta_tau
*)
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_lift.ma".
-include "Basic-2/reduction/tpr.ma".
+include "Basic_2/substitution/tps_lift.ma".
+include "Basic_2/reduction/tpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* Relocation properties ****************************************************)
-(* Basic-1: was: pr0_lift *)
+(* Basic_1: was: pr0_lift *)
lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
#T1 #T2 #H elim H -H T1 T2
]
qed.
-(* Basic-1: was: pr0_gen_lift *)
+(* Basic_1: was: pr0_gen_lift *)
lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
∀d,e,U1. ↑[d, e] U1 ≡ T1 →
∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
]
qed.
-(* Basic-1: was pr0_gen_abst *)
+(* Basic_1: was pr0_gen_abst *)
lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
/2/ qed.
(* *)
(**************************************************************************)
-include "Basic-2/reduction/tpr_tps.ma".
+include "Basic_2/reduction/tpr_tpss.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
qed.
-(* Basic-1: was: pr0_cong_delta pr0_delta_delta *)
+(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
fact tpr_conf_delta_delta:
∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
qed.
-(* Basic-1: was: pr0_upsilon_upsilon *)
+(* Basic_1: was: pr0_upsilon_upsilon *)
fact tpr_conf_theta_theta:
∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
@ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
(* case 17: tau, tau *)
| #HT02
- /2 by tpr_conf_tau_tau/
+ /3 width=5 by tpr_conf_tau_tau/
]
]
qed.
-(* Basic-1: was: pr0_confluence *)
+(* Basic_1: was: pr0_confluence *)
theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 →
∃∃T. T1 ⇒ T & T2 ⇒ T.
#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/
+++ /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/reduction/ltpr_drop.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Basic-1: was: pr0_subst1 *)
-lemma 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 | /3/ ] (**) (* /4 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} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- lapply (tpss_leq_repl_dx … HTT2 (L2. 𝕓{Abbr} VV2) ?) -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} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
- lapply (tps_leq_repl_dx … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
- elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
- lapply (tpss_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
- lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
- lapply (tpss_leq_repl_dx … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
- lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #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 #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
- elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- elim (lift_total VV2 0 1) #VV #H2VV
- lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
- @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
- elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
- elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
-| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
- elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
-]
-qed.
-
-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.
-#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
-qed.
-
-lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
- ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
-#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
-[ /2/
-| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
- elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
- lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
-]
-qed.
\ No newline at end of file
--- /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/reduction/ltpr_drop.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Basic_1: was: pr0_subst1 *)
+lemma 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 | /3/ ] (**) (* /4 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} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -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} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
+ lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
+ elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
+ lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
+ lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
+ lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
+ lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #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 #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
+ elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
+ elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
+ elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ elim (lift_total VV2 0 1) #VV #H2VV
+ lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
+ @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
+| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
+ elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
+ elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
+| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
+ elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
+]
+qed.
+
+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.
+#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
+qed.
+
+lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
+ ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
+ ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
+#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
+[ /2/
+| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
+ elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
+ lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
+]
+qed.
\ No newline at end of file
(* *)
(**************************************************************************)
-include "Basic-2/grammar/lenv_weight.ma".
-include "Basic-2/grammar/leq.ma".
-include "Basic-2/substitution/lift.ma".
+include "Basic_2/grammar/lenv_weight.ma".
+include "Basic_2/grammar/lsubs.ma".
+include "Basic_2/substitution/lift.ma".
(* DROPPING *****************************************************************)
-(* Basic-1: includes: drop_skip_bind *)
+(* Basic_1: includes: drop_skip_bind *)
inductive drop: nat → nat → relation lenv ≝
| drop_atom: ∀d,e. drop d e (⋆) (⋆)
| drop_pair: ∀L,I,V. drop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
]
qed.
-(* Basic-1: was: drop_gen_refl *)
+(* Basic_1: was: drop_gen_refl *)
lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2.
/2 width=5/ qed.
]
qed.
-(* Basic-1: was: drop_gen_sort *)
+(* Basic_1: was: drop_gen_sort *)
lemma drop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆.
/2 width=5/ qed.
(0 < e ∧ ↓[0, e - 1] K ≡ L2).
/2/ qed.
-(* Basic-1: was: drop_gen_drop *)
+(* Basic_1: was: drop_gen_drop *)
lemma drop_inv_drop1: ∀e,K,I,V,L2.
↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2.
#e #K #I #V #L2 #H #He
]
qed.
-(* Basic-1: was: drop_gen_skip_l *)
+(* Basic_1: was: drop_gen_skip_l *)
lemma drop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d →
∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
]
qed.
-(* Basic-1: was: drop_gen_skip_r *)
+(* Basic_1: was: drop_gen_skip_r *)
lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
(* Basic properties *********************************************************)
-(* Basic-1: was by definition: drop_refl *)
+(* Basic_1: was by definition: drop_refl *)
lemma drop_refl: ∀L. ↓[0, 0] L ≡ L.
#L elim L -L //
qed.
#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
qed.
-lemma drop_leq_drop1: ∀L1,L2,d,e. L1 [d, e] ≈ L2 →
- ∀I,K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{I} V →
- d ≤ i → i < d + e →
- ∃∃K2. K1 [0, d + e - i - 1] ≈ K2 &
- ↓[0, i] L2 ≡ K2. 𝕓{I} V.
+lemma drop_lsubs_drop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
+ ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V →
+ d ≤ i → i < d + e →
+ ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
+ ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V.
#L1 #L2 #d #e #H elim H -H L1 L2 d e
-[ #d #e #I #K1 #V #i #H
+[ #d #e #K1 #V #i #H
lapply (drop_inv_atom1 … H) -H #H destruct
-| #L1 #L2 #I #K1 #V #i #_ #_ #H
+| #L1 #L2 #K1 #V #i #_ #_ #H
elim (lt_zero_false … H)
-| #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie
+| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie
elim (drop_inv_O1 … H) -H * #Hi #HLK1
- [ -IHL12 Hie; destruct -i K1 J W;
+ [ -IHL12 Hie; destruct -i K1 W;
<minus_n_O <minus_plus_m_m /2/
| -HL12;
elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
]
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #I #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
+| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
+ elim (drop_inv_O1 … H) -H * #Hi #HLK1
+ [ -IHL12 Hie Hi; destruct
+ | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+ ]
+| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
lapply (plus_S_le_to_pos … Hdi) #Hi
lapply (drop_inv_drop1 … H ?) -H // #HLK1
elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/
(* Basic forvard lemmas *****************************************************)
-(* Basic-1: was: drop_S *)
+(* Basic_1: was: drop_S *)
lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 →
↓[O, e + 1] L1 ≡ K2.
#L1 elim L1 -L1
]
qed.
-(* Basic-1: removed theorems 49:
+(* 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
(* *)
(**************************************************************************)
-include "Basic-2/substitution/lift_lift.ma".
-include "Basic-2/substitution/drop.ma".
+include "Basic_2/substitution/lift_lift.ma".
+include "Basic_2/substitution/drop.ma".
(* DROPPING *****************************************************************)
(* Main properties **********************************************************)
-(* Basic-1: was: drop_mono *)
+(* Basic_1: was: drop_mono *)
theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 →
∀L2. ↓[d, e] L ≡ L2 → L1 = L2.
#d #e #L #L1 #H elim H -H d e L L1
]
qed.
-(* Basic-1: was: drop_conf_ge *)
+(* Basic_1: was: drop_conf_ge *)
theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
↓[0, e2 - e1] L1 ≡ L2.
]
qed.
-(* Basic-1: was: drop_conf_lt *)
+(* Basic_1: was: drop_conf_lt *)
theorem drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 →
e2 < d1 → let d ≝ d1 - e2 - 1 in
]
qed.
-(* Basic-1: was: drop_trans_le *)
+(* Basic_1: was: drop_trans_le *)
theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
]
qed.
-(* Basic-1: was: drop_trans_ge *)
+(* Basic_1: was: drop_trans_ge *)
theorem drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.
#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
#e1 #e1 #e2 >commutative_plus /2 width=5/
qed.
-(* Basic-1: was: drop_conf_rev *)
+(* Basic_1: was: drop_conf_rev *)
axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L →
∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1.
(* *)
(**************************************************************************)
-include "Basic-2/grammar/term_weight.ma".
+include "Basic_2/grammar/term_weight.ma".
(* RELOCATION ***************************************************************)
-(* Basic-1: includes:
+(* Basic_1: includes:
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
*)
inductive lift: nat → nat → relation term ≝
(* Basic properties *********************************************************)
-(* Basic-1: was: lift_lref_gt *)
+(* 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 *)
+(* 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) *)
+(* 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 *)
+(* 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 *)
+(* 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 *)
+(* 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_false *)
-(* Basic-1: was: lift_gen_lref_ge *)
+(* 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 *)
+(* 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 *)
+(* 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:
+(* 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
(* *)
(**************************************************************************)
-include "Basic-2/substitution/lift.ma".
+include "Basic_2/substitution/lift.ma".
(* RELOCATION ***************************************************************)
(* Main properies ***********************************************************)
-(* Basic-1: was: lift_inj *)
+(* 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 *)
+(* 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) *)
+(* 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) *)
+(* 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) *)
+(* 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.
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps.ma".
+include "Basic_2/substitution/tps.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
-(* Basic-1: includes: csubst1_bind *)
+(* Basic_1: includes: csubst1_bind *)
inductive ltps: nat → nat → relation lenv ≝
| ltps_atom: ∀d,e. ltps d e (⋆) (⋆)
| ltps_pair: ∀L,I,V. ltps 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
>(plus_minus_m_m d 1) /2/
qed.
-(* Basic-1: was by definition: csubst1_refl *)
+(* 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/
L1 = K1. 𝕓{I} V1.
/2/ qed.
-(* Basic-1: removed theorems 27:
+(* 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
(* *)
(**************************************************************************)
-include "Basic-2/substitution/ltps.ma".
+include "Basic_2/substitution/ltps.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_lift.ma".
-include "Basic-2/substitution/ltps_drop.ma".
+include "Basic_2/substitution/tps_lift.ma".
+include "Basic_2/substitution/ltps_drop.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
]
qed.
-(* Basic-1: was: subst1_subst1_back *)
+(* Basic_1: was: subst1_subst1_back *)
lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L0 [d1, e1] ≫ L1 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
]
qed.
-(* Basic-1: was: subst1_subst1 *)
+(* Basic_1: was: subst1_subst1 *)
lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
∀L1,d1,e1. L1 [d1, e1] ≫ L0 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
(* *)
(**************************************************************************)
-include "Basic-2/grammar/cl_weight.ma".
-include "Basic-2/substitution/drop.ma".
+include "Basic_2/grammar/cl_weight.ma".
+include "Basic_2/substitution/drop.ma".
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
(* Basic properties *********************************************************)
-lemma tps_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
- ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫ T2.
+lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
+ ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫ T2.
#L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e
[ //
| #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
- elim (drop_leq_drop1 … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/
+ elim (drop_lsubs_drop1_abbr … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/
| /4/
| /3/
]
elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
elim (IHT12 (i + 1) ? ?) -IHT12 [2: /2 by arith4/ |3: /2/ ] (* just /2/ is too slow *)
-Hdi Hide >arith_c1 >arith_c1x #T #HT1 #HT2
- lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
+ lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
-Hdi Hide /3 width=5/
/2/ qed.
-(* Basic-1: was: subst1_gen_sort *)
+(* 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 *)
+(* 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 &
]
qed.
-(* Basic-1: removed theorems 25:
+(* Basic_1: removed theorems 25:
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
(* *)
(**************************************************************************)
-include "Basic-2/substitution/drop_drop.ma".
-include "Basic-2/substitution/tps.ma".
+include "Basic_2/substitution/drop_drop.ma".
+include "Basic_2/substitution/tps.ma".
(* PARTIAL SUBSTITUTION ON TERMS ********************************************)
(* Relocation properties ****************************************************)
-(* Basic-1: was: subst1_lift_lt *)
+(* Basic_1: was: subst1_lift_lt *)
lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
∀L,U1,U2,d,e. ↓[d, e] L ≡ K →
↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 →
]
qed.
-(* Basic-1: was: subst1_lift_ge *)
+(* Basic_1: was: subst1_lift_ge *)
lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
∀L,U1,U2,d,e. ↓[d, e] L ≡ K →
↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 →
]
qed.
-(* Basic-1: was: subst1_gen_lift_lt *)
+(* Basic_1: was: subst1_gen_lift_lt *)
lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
dt + et ≤ d →
]
qed.
-(* Basic-1: was: subst1_gen_lift_ge *)
+(* Basic_1: was: subst1_gen_lift_ge *)
lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
d + e ≤ dt →
]
qed.
-(* Basic-1: was: subst1_gen_lift_eq *)
+(* Basic_1: was: subst1_gen_lift_eq *)
lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e.
L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
#L #U1 #U2 #d #e #H elim H -H L U1 U2 d e
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_lift.ma".
+include "Basic_2/substitution/tps_lift.ma".
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
(* Main properties **********************************************************)
-(* Basic-1: was: subst1_confluence_eq *)
+(* 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 #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;
- lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02
+ lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02
elim (IHV01 … HV02) -IHV01 HV02 #V #HV1 #HV2
elim (IHT01 … HT02) -IHT01 HT02 #T #HT1 #HT2
- lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /2/
- lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/
+ lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2/
+ lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V) ?) -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;
]
qed.
-(* Basic-1: was: subst1_confluence_neq *)
+(* 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) →
elim (IHV01 … HV02 H) -IHV01 HV02 #V #HV1 #HV2
elim (IHT01 … HT02 ?) -IHT01 HT02
[ -H #T #HT1 #HT2
- lapply (tps_leq_repl_dx … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/
- lapply (tps_leq_repl_dx … HT2 (L1. 𝕓{I} V) ?) -HT2 /3 width=5/
+ lapply (tps_lsubs_conf … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/
+ lapply (tps_lsubs_conf … HT2 (L1. 𝕓{I} V) ?) -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 *)
]
qed.
(* Note: the constant 1 comes from tps_subst *)
-(* Basic-1: was: subst1_trans *)
+(* Basic_1: was: subst1_trans *)
theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 →
∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e →
L ⊢ T1 [d, e] ≫ T2.
<(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2/
| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X;
- lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
+ lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
lapply (IHT10 … HT02 He) -IHT10 HT02 #HT12
- lapply (tps_leq_repl_dx … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/
+ lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/
| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X /3/
]
<(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
- lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
+ lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
elim (IHV10 … HV02 ?) -IHV10 HV02 // #V
elim (IHT10 … HT02 ?) -IHT10 HT02 [2: /2/ ] #T #HT1 #HT2
- lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1;
- lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/
+ lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1;
+ lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X;
elim (IHV10 … HV02 ?) -IHV10 HV02 //
(* *)
(**************************************************************************)
-include "Basic-2/substitution/ltps.ma".
-include "Basic-2/unfold/tpss.ma".
+include "Basic_2/substitution/ltps.ma".
+include "Basic_2/unfold/tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
(*
-include "Basic-2/substitution/ltps.ma".
+include "Basic_2/substitution/ltps.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
(* *)
(**************************************************************************)
-include "Basic-2/unfold/ltpss_tpss.ma".
+include "Basic_2/unfold/ltpss_tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
-include "Basic-2/unfold/tpss_ltps.ma".
-include "Basic-2/unfold/ltpss.ma".
+include "Basic_2/unfold/tpss_ltps.ma".
+include "Basic_2/unfold/ltpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps.ma".
+include "Basic_2/substitution/tps.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
L ⊢ T1 [d, e] ≫ T → L ⊢ T [d, e] ≫* T2 → L ⊢ T1 [d, e] ≫* T2.
/2/ qed.
-lemma tpss_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
- ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫* T2.
+lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
+ ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫* T2.
/3/ qed.
lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T.
| #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
| #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
- lapply (tpss_leq_repl_dx … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12
+ lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12
lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
[ /2 width=5/
| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
- lapply (tpss_leq_repl_dx … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
+ lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
]
qed.
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_lift.ma".
-include "Basic-2/unfold/tpss.ma".
+include "Basic_2/substitution/tps_lift.ma".
+include "Basic_2/unfold/tpss.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
(* *)
(**************************************************************************)
-include "Basic-2/substitution/ltps_tps.ma".
-include "Basic-2/unfold/tpss_tpss.ma".
+include "Basic_2/substitution/ltps_tps.ma".
+include "Basic_2/unfold/tpss_tpss.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X;
lapply (tps_fwd_tw … HV01) #H2
lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H
- lapply (IH … HV01 … HK01 ? ?) -IH HV01 HK01 [1,3: // |2,4: skip | /2/ | /3 width=6/ ]
+ lapply (IH … HV01 … HK01 ? ?) -IH HV01 HK01 [1,3: // |2,4: skip | normalize /2/ | /3 width=6/ ]
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2;
- lapply (tps_leq_repl_dx … HT12 (L. 𝕓{I} V1) ?) -HT12 /2/ #HT12
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: // |2,4: skip ] #HV12
+ lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2/ #HT12
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12
lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH HT12 [1,3,5: /2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_leq_repl_dx … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2/
+ lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2/
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2;
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: // |2,4: skip ]
- lapply (IH … HT12 … HL0 ? ?) -IH HT12 [1,3,5: // |2,4: skip ] -HL0 /2/
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ]
+ lapply (IH … HT12 … HL0 ? ?) -IH HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2/
]
qed.
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_tps.ma".
-include "Basic-2/unfold/tpss_lift.ma".
+include "Basic_2/substitution/tps_tps.ma".
+include "Basic_2/unfold/tpss_lift.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
(**************************************************************************)
include "arithmetics/nat.ma".
-include "Ground-2/xoa_props.ma".
+include "Ground_2/xoa_props.ma".
(* ARITHMETICAL PROPERTIES **************************************************)
(* *)
(**************************************************************************)
-include "Ground-2/arith.ma".
-include "Ground-2/notation.ma".
+include "Ground_2/arith.ma".
+include "Ground_2/notation.ma".
(* LISTS ********************************************************************)
(**************************************************************************)
include "basics/star.ma".
-include "Ground-2/xoa_props.ma".
+include "Ground_2/xoa_props.ma".
(* PROPERTIES of RELATIONS **************************************************)
-->
</section>
<section name="xoa">
- <key name="output_dir">contribs/lambda-delta/Ground-2</key>
+ <key name="output_dir">contribs/lambda_delta/Ground-2/</key>
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
(* *)
(**************************************************************************)
-include "Ground-2/xoa_notation.ma".
-include "Ground-2/xoa.ma".
+include "Ground_2/xoa_notation.ma".
+include "Ground_2/xoa.ma".
lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
#A0 #P0 #P1 * /2/
#!/bin/sh
-for V in `cat Make`; do
- echo ${V}; sed "s/$1/$2/g" ${V} > ${V}.new
- if diff ${V} ${V}.new > /dev/null;
- then rm -f ${V}.new; else mv -f ${V}.new ${V}; fi
+for MA in `find -name "*.ma"`; do
+ echo ${MA}; sed "s/$1/$2/g" ${MA} > ${MA}.new
+ if diff ${MA} ${MA}.new > /dev/null;
+ then rm -f ${MA}.new; else mv -f ${MA}.new ${MA}; fi
done
-unset V
+unset MA
projects / helm.git / commitdiff