csubv/getl csubv_getl_conf_void
csubv/props csubv_bind_same
csubv/props csubv_refl
-
-# check #############################################################
-
-drop1/fwd drop1_gen_pnil
-drop1/fwd drop1_gen_pcons
-drop1/props drop1_skip_bind
drop1/props drop1_cons_tail
-
-# waiting ####################################################################
-
drop/props drop_ctail
ex0/props aplus_gz_le
ex0/props aplus_gz_ge
leq/props leq_ahead_false_1
leq/props leq_ahead_false_2
lift1/fwd lift1_cons_tail
+
+# check #############################################################
+
lift1/fwd lifts1_flat
lift1/fwd lifts1_nil
lift1/fwd lifts1_cons
lift1/props lift1_free
lift/props thead_x_lift_y_y
lift/props lifts_tapp
+
+# waiting ####################################################################
+
lift/props lifts_inj
llt/props lweight_repl
llt/props llt_repl
pc3/wcpr0 pc3_wcpr0_t
pc3/wcpr0 pc3_wcpr0
pr0/fwd pr0_gen_void
+
+# check #############################################################
+
pr0/dec nf0_dec
pr0/subst1 pr0_subst1_back
pr0/subst1 pr0_subst1_fwd
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/reducibility/trf.ma".
include "Basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE NORMAL TERMS ************************************************)
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@(discr_tpair_xy_y … H)
qed-.
-
-(* Basic properties *********************************************************)
-
-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
- [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (tif_inv_cast … H)
- ]
-| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
- elim (tif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
- [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
- | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
- elim (tif_inv_abst … H) -H #HV1 #HT1
- >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- ]
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (tif_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-| #V1 #T1 #T2 #T #_ #_ #_ #H
- elim (tif_inv_abbr … H)
-| #V1 #T1 #T #_ #_ #H
- elim (tif_inv_cast … H)
-]
-qed.
-
-theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1].
-/2 width=1/ qed.
-
-(* Note: this property is unusual *)
-theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
-#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/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #H elim (tnf_inv_abbr … H)
-| #V #T #H elim (tnf_inv_cast … H)
-| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
- elim (simple_inv_bind … H)
-]
-qed.
-
-theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
-/2 width=3/ qed.
-
-lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T].
-/4 width=1/ qed.
-
-lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T].
-/4 width=1/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/substitution/tps_lift.ma".
+include "Basic_2/reducibility/trf.ma".
+include "Basic_2/reducibility/tnf.ma".
+
+(* CONTEXT-FREE NORMAL TERMS ************************************************)
+
+(* Main properties properties ***********************************************)
+
+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
+ [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (tif_inv_cast … H)
+ ]
+| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (tif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
+ [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
+ | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
+ elim (tif_inv_abst … H) -H #HV1 #HT1
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ ]
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (tif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #V1 #T1 #T2 #T #_ #_ #_ #H
+ elim (tif_inv_abbr … H)
+| #V1 #T1 #T #_ #_ #H
+ elim (tif_inv_cast … H)
+]
+qed.
+
+theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1].
+/2 width=1/ qed.
+
+(* Note: this property is unusual *)
+lemma tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
+#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/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
+| #V #T #H elim (tnf_inv_abbr … H)
+| #V #T #H elim (tnf_inv_cast … H)
+| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+qed.
+
+theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
+/2 width=3/ qed.
+
+lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T].
+/4 width=1/ qed.
+
+lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T].
+/4 width=1/ qed.
(* Basic inversion lemmas ***************************************************)
+fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ÷⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsuba_inv_atom1: ∀L2. ⋆ ÷⊑ L2 → L2 = ⋆.
+/2 width=3/ qed-.
+
+fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
+ (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+ L2 = K2. ⓛW & I = Abbr.
+#L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/
+]
+qed.
+
+lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ÷⊑ L2 →
+ (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+ L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ÷⊑ L2 → L2 = ⋆ → L1 = ⋆.
+#L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubc_inv_atom2: ∀L1. L1 ÷⊑ ⋆ → L1 = ⋆.
+/2 width=3/ qed-.
+
fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
(∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨
∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/static/aaa_aaa.ma".
+include "Basic_2/static/lsuba_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+
+(* Properties concerning atomic arity assignment ****************************)
+
+lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ÷ A → ∀L2. L1 ÷⊑ L2 → L2 ⊢ V ÷ A.
+#L1 #V #A #H elim H -L1 -V -A
+[ //
+| #I #L1 #K1 #V1 #B #i #HLK1 #HV1B #IHV1 #L2 #HL12
+ elim (lsuba_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
+ elim (lsuba_inv_pair1 … H) -H * #K2
+ [ #HK12 #H destruct /3 width=5/
+ | #V2 #A1 #HV1A1 #HV2 #_ #H1 #H2 destruct
+ >(aaa_mono … HV1B … HV1A1) -B -HV1A1 /2 width=5/
+ ]
+| /4 width=2/
+| /4 width=1/
+| /3 width=3/
+| /3 width=1/
+]
+qed.
+
+lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ÷ A → ∀L1. L1 ÷⊑ L2 → L1 ⊢ V ÷ A.
+#L2 #V #A #H elim H -L2 -V -A
+[ //
+| #I #L2 #K2 #V2 #B #i #HLK2 #HV2B #IHV2 #L1 #HL12
+ elim (lsuba_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsuba_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct /3 width=5/
+ | #V1 #A1 #HV1 #HV2A1 #_ #H1 #H2 destruct
+ >(aaa_mono … HV2B … HV2A1) -B -HV2A1 /2 width=5/
+ ]
+| /4 width=2/
+| /4 width=1/
+| /3 width=3/
+| /3 width=1/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/static/lsuba.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+
+lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ÷⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. K1 ÷⊑ K2 & ⇩[0, e] L2 ≡ K2.
+#L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #K1 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK1
+ [ destruct
+ elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+]
+qed-.
+
+lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ÷⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. K1 ÷⊑ K2 & ⇩[0, e] L1 ≡ K1.
+#L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #K2 #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #HLK2
+ [ destruct
+ elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+ | elim (IHL12 … HLK2) -L2 /3 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/static/lsuba_aaa.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+
+(* Main properties **********************************************************)
+
+theorem lsuba_trans: ∀L1,L. L1 ÷⊑ L → ∀L2. L ÷⊑ L2 → L1 ÷⊑ L2.
+#L1 #L #H elim H -L1 -L
+[ #X #H >(lsuba_inv_atom1 … H) -H //
+| #I #L1 #L #V #HL1 #IHL1 #X #H
+ elim (lsuba_inv_pair1 … H) -H * #L2
+ [ #HL2 #H destruct /3 width=1/
+ | #V #A #HLV #HL2V #HL2 #H1 #H2 destruct /3 width=3/
+ ]
+| #L1 #L #V1 #W #A1 #HV1 #HW #HL1 #IHL1 #X #H
+ elim (lsuba_inv_pair1 … H) -H * #L2
+ [ #HL2 #H destruct /3 width=5/
+ | #V #A2 #_ #_ #_ #_ #H destruct
+ ]
+]
+qed.
#L1 #L #L2 #d #e #des #_ #_ #H destruct
qed.
+(* Basic_1: was: drop1_gen_pnil *)
lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2.
/2 width=3/ qed-.
/2 width=3/
qed.
+(* Basic_1: was: drop1_gen_pcons *)
lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 →
∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
+(* Basic_1: was: drop1_skip_bind *)
lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
∀I. ⇩*[des + 1] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
#L1 #L2 #des #H elim H -L1 -L2 -des
(* Properties concerning basic term relocation ******************************)
-(* Basic_1: was: lift1_xhg *)
+(* Basic_1: was: lift1_xhg (right to left) *)
lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 →
∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[des + 1] T0 ≡ T2.
#T1 #T #des #H elim H -T1 -T -des
>(lifts_inv_nil … H) -T1 /2 width=3/
| #d #e #des #IHdes #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02
elim (at_inv_cons … H1) -H1 * #Hid #Hi0
- [ elim (minuss_inv_cons1_lt … H2 ?) -H2 [2: /2 width=1/ ] #des1 #Hdes1 <plus_minus // <minus_plus <plus_minus_m_m /2 width=1/ #H
+ [ elim (minuss_inv_cons1_lt … H2 ?) -H2 [2: /2 width=1/ ] #des1 #Hdes1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
elim (pluss_inv_cons2 … H) -H #des2 #H1 #H2 destruct
elim (lifts_inv_cons … HT10) -HT10 #T >minus_plus #HT1 #HT0
elim (IHdes … Hi0 … Hdes1 … HT0 … HT02) -IHdes -Hi0 -Hdes1 -T0 #T0 #HT0 #HT02
(* Main properties **********************************************************)
-(* Basic_1: was: lifts1_xhg *)
+(* Basic_1: was: lifts1_xhg (right to left) *)
lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.
(* Main properties **********************************************************)
-(* Basic_1: was: lift1_lift1 *)
+(* Basic_1: was: lift1_lift1 (left to right) *)
theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 →
⇧*[des1 @ des2] T1 ≡ T2.
#T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
projects / helm.git / commitdiff