]> matita.cs.unibo.it Git - helm.git/commitdiff
- more properties on strongly normalizing terms
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 14 Feb 2012 20:07:50 +0000 (20:07 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 14 Feb 2012 20:07:50 +0000 (20:07 +0000)
- bugfix in Basic_1 annotations

17 files changed:
matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma
matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma
matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
matita/matita/contribs/lambda_delta/Basic_2/notation.ma
matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma
matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma
matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma
matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma

index 0570c48b302df1aede6b416482a43a18969ce1ec..f7e55be6343cadd5a5dafac7d42e98509d35bb27 100644 (file)
@@ -290,7 +290,6 @@ sn3/props sn3_shift
 sn3/props sn3_change
 sn3/props sn3_gen_def
 sn3/props sn3_cdelta
-sn3/props sn3_beta
 sn3/props sn3_appl_lref
 sn3/props sn3_appl_abbr
 sn3/props sn3_appl_cast
@@ -302,7 +301,6 @@ sn3/props sn3_appls_lref
 sn3/props sn3_appls_cast
 sn3/props sn3_appls_bind
 sn3/props sn3_appls_beta
-sn3/props sn3_abbr
 sn3/props sn3_appls_abbr
 sn3/props sns3_lifts
 
index 20bf4ebe59b07a3b246c8b557b6b7584865d89fd..e198001045b9f727e571dcf427ad0af18cd9e147 100644 (file)
@@ -36,3 +36,9 @@ lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
 #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT2 /3 width=5/
 qed.
+
+lemma cpr_abbr: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 →
+                L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+#L #V1 #V2 #HV12 #T1 #T2 #HT12
+@(cprs_strap2 … (ⓓV1.T2)) /2 width=1/ /3 width=1/
+qed.
index b4106047214d2b20ed303e4280cdaa7564d552d2..f5d8b739017588a8c6ea96faaf7562b9551ac55f 100644 (file)
@@ -72,19 +72,14 @@ qed.
 
 (* Basic forward lemmas *****************************************************)
 
-fact csn_fwd_flat2_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T.
+fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T.
 #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
 @csn_intro #T2 #HLT2 #HT2
 @(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
 qed.
 
 (* Basic_1: was: sn3_gen_flat *)
-lemma csn_fwd_flat2: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
+lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
 /2 width=5/ qed-.
 
-(*
-sn3/fwd sn3_gen_bind
-sn3/fwd sn3_gen_head
-*)
-
 (* Basic_1: removed theorems 3: sn3_gen_cflat sn3_cflat sn3_bind *)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma
new file mode 100644 (file)
index 0000000..11647e9
--- /dev/null
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/reducibility/cpr_cpr.ma".
+include "Basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* Advanced forvard lemmas **************************************************)
+
+fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬇* V.
+#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+@csn_intro #V2 #HLV2 #HV2
+@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
+qed.
+
+(* Basic_1: was: sn3_gen_head *)
+lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬇* ②{I} V. T → L ⊢ ⬇* V.
+/2 width=5/ qed.
+
+fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬇* U →
+                          ∀I,V,T. U = ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬇* T.
+#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+@csn_intro #T2 #HLT2 #HT2
+@(IH (ⓑ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+qed.
+
+(* Basic_1: was: sn3_gen_bind *)
+lemma csn_fwd_bind_dx: ∀I,L,V,T. L ⊢ ⬇* ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬇* T.
+/2 width=3/ qed.
index ace3b9feab2764fcb41615cc2508e783744b46d2..4a936f607864a36067ed488aa7b4bdc18ea1ebdb 100644 (file)
@@ -25,10 +25,6 @@ interpretation
    "context-sensitive strong normalization (term)"
    'SNStar L T = (csns L T).
 
-notation "hvbox( L ⊢ ⬇ * * T )"
-   non associative with precedence 45
-   for @{ 'SNStar $L $T }.
-
 (* Basic eliminators ********************************************************)
 
 lemma csns_ind: ∀L. ∀R:predicate term.
index 88c492779d2eb78a605c251f74cfc75f30e0c411..8121a0ac1f60910d3a82cf8468fc03677cfc1a3b 100644 (file)
 (**************************************************************************)
 
 include "Basic_2/reducibility/lcpr_cpr.ma".
-include "Basic_2/computation/cprs_lcpr.ma".
-include "Basic_2/computation/csn_cprs.ma".
+include "Basic_2/computation/cprs_cprs.ma".
 include "Basic_2/computation/csn_lift.ma".
+include "Basic_2/computation/csn_cpr.ma".
+include "Basic_2/computation/csn_cprs.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
 (* Advanced properties ******************************************************)
 
-lemma csn_lcpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T.
+lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T.
 #L1 #L2 #HL12 #T #H @(csn_ind_cprs … H) -T #T #_ #IHT
 @csn_intro #T0 #HLT0 #HT0
 @IHT /2 width=2/ -IHT -HT0 /2 width=3/
 qed.
 
 lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T.
-#L #V #HV @(csn_ind … HV) -V #V #_ #IHV #T #HT @(csn_ind_cprs … HT) -T #T #HT #IHT
+#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_cprs … HT) -T #T #HT #IHT
 @csn_intro #X #H1 #H2
 elim (cpr_inv_abbr1 … H1) -H1 *
 [ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
@@ -36,10 +37,39 @@ elim (cpr_inv_abbr1 … H1) -H1 *
   lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1
   elim (eq_false_inv_tpair … H2) -H2
   [ #HV1 @IHV // /2 width=1/ -HV1
-    @(csn_lcpr_trans (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
+    @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
   | -IHV -HLV1 * #H destruct /3 width=1/
   ]
 | -IHV -IHT -H2 #T0 #HT0 #HLT0
   lapply (csn_inv_lift … HT … HT0) -HT /2 width=3/
 ]
 qed.
+
+fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U →
+                        ∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T.
+#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_cprs … H) -X #X #HVT #IHVT #V #T #H destruct
+lapply (csn_fwd_pair_sn … HVT) #HV
+lapply (csn_fwd_bind_dx … HVT) #HT -HVT
+@csn_intro #X #H #H2
+elim (cpr_inv_appl1 … H) -H *
+[ #V0 #Y #HLV0 #H #H0 destruct
+  elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+  elim (eq_false_inv_beta … H2) -H2
+  [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
+    @csn_abbr /2 width=3/ -HV
+    @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
+  | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
+    @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/
+  ]
+| -IHW -IHVT -H2 #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
+  lapply (lcpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01
+  @csn_abbr /2 width=3/ -HV
+  @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
+| -IHW -IHVT -HV -HT -H2 #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: sn3_beta *)
+lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* (ⓓV. T) → (**)
+                     L ⊢ ⬇* ⓐV. ⓛW. T.
+/2 width=3/ qed.
index 605e78db110f0c89e344cc58e84e3c12eed9d386..29872f92903bc01b67aad87a15967554a6154ec8 100644 (file)
@@ -18,28 +18,6 @@ include "Basic_2/computation/csn.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
 
-(* Advanced properties ******************************************************)
-
-lemma csn_acp: acp cpr (eq …) (csn …).
-@mk_acp
-[ /2 width=1/
-| /2 width=3/
-| /2 width=5/
-| @cnf_lift
-]
-qed.
-
-lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T.
-#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT
-@csn_intro #X #H1 #H2
-elim (cpr_inv_abst1 … H1 I V) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair … H2) -H2
-[ /3 width=5/
-| -HLW0 * #H destruct /3 width=1/
-]
-qed.
-
 (* Relocation properties ****************************************************)
 
 (* Basic_1: was: sn3_lift *)
@@ -62,3 +40,40 @@ lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10
 @(IHT1 … HLT10) // -L1 -L2 #H destruct
 >(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1/
 qed.
+
+(* Advanced properties ******************************************************)
+
+lemma csn_acp: acp cpr (eq …) (csn …).
+@mk_acp
+[ /2 width=1/
+| /2 width=3/
+| /2 width=5/
+| @cnf_lift
+]
+qed.
+
+(* Basic_1: was: sn3_abbr *)
+lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i.
+#L #K #V #i #HLK #HV
+@csn_intro #X #H #Hi
+elim (cpr_inv_lref1 … H) -H
+[ #H destruct elim (Hi ?) //
+| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1 #_
+  lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct
+  lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK
+  @(csn_lift … HLK HV1) -HLK -HV1
+  @(csn_cpr_trans … HV) -HV
+  @(cpr_intro … HV01) -HV01 //
+]
+qed.
+
+lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T.
+#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT
+@csn_intro #X #H1 #H2
+elim (cpr_inv_abst1 … H1 I V) -H1
+#W0 #T0 #HLW0 #HLT0 #H destruct
+elim (eq_false_inv_tpair … H2) -H2
+[ /3 width=5/
+| -HLW0 * #H destruct /3 width=1/
+]
+qed.
index 7a5a9d91db03acf45dec551d4df1f99bb0626b4d..32f8272dcd217727db74222bd06063124189020d 100644 (file)
@@ -89,6 +89,21 @@ elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
 @or_intror @conj // #HT12 destruct /2 width=1/ 
 qed-.
 
+lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2.
+                         (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →False) →
+                         (W1 = W2 → False) ∨
+                         (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → False)).
+#V1 #V2 #W1 #W2 #T1 #T2 #H
+elim (eq_false_inv_tpair … H) -H
+[ #HV12 elim (term_eq_dec W1 W2) /3 width=1/
+  #H destruct @or_intror @conj // #H destruct /2 width=1/
+| * #H1 #H2 destruct
+  elim (eq_false_inv_tpair … H2) -H2 /3 width=1/
+  * #H #HT12 destruct
+  @or_intror @conj // #H destruct /2 width=1/
+]
+qed.
+
 (* Basic_1: removed theorems 3:
             not_void_abst not_abbr_void not_abst_void
 *)
index 9f2d54df0cc5c8b8553d7501050e753ea5f2a28b..08ff46477bd79af4ba948c86aad64a0ea6325593 100644 (file)
@@ -278,6 +278,10 @@ notation "hvbox( L ⊢ ⬇ * T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
 
+notation "hvbox( L ⊢ ⬇ * * T )"
+   non associative with precedence 45
+   for @{ 'SNStar $L $T }.
+
 notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )"
    non associative with precedence 45
    for @{ 'InEInt $R $L $T $A }.
index fca70da65141863270ffc4f2c13035995c5dd143..0ad09e4b4c22a1bd0dec07b9ed2645d2a143a073 100644 (file)
@@ -107,8 +107,8 @@ elim (tpr_inv_cast1 … H) -H /3 width=3/
 elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
 qed-.
 
-(* Basic_1: removed theorems 5
-            pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
+(* Basic_1: removed theorems 4
+            pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
    Basic_1: removed local theorems 3:
             pr2_free_free pr2_free_delta pr2_delta_delta
 *)
index 5553449943695983896ec6f6b8f3ce10ab944a46..236b953d8d104c4ff23f5b35c5d589df80a2a72c 100644 (file)
@@ -21,7 +21,7 @@ include "Basic_2/reducibility/cpr.ma".
 
 lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
                    L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 
+#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
 @ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
 qed.
 
@@ -35,6 +35,13 @@ lapply (tpss_tps … HT0) -HT0 #HT0
 @ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
 
+
+(* Basic_1: was only: pr2_head_1 *) 
+lemma cpr_pair_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
+                   L ⊢ ②{I} V1. T1 ➡ ②{I} V2. T2.
+* /2 width=1/ /3 width=1/
+qed.
+
 (* Advanced forward lemmas **************************************************)
 
 lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L @ T1 ➡ L @ T2.
index ae26fa75daf98f67de27d48ca25504b66700c24f..fcf4de993b76aace208648325c988d4517ee53b7 100644 (file)
@@ -17,7 +17,7 @@ include "Basic_2/reducibility/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
 
-(* Unfold properties ********************************************************)
+(* Properties concerning parallel unfold on terms ***************************)
 
 (* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
 (* Basic_1: was only: pr2_subst1 *)
index 5c725a948508bdc620f0a5dd8be197f737e3ff1b..090e8cfbf7c1be444d53f4b7327e6ae7d7187851 100644 (file)
@@ -17,7 +17,7 @@ include "Basic_2/reducibility/ltpr.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 
-(* Basic_1: was: wcpr0_ldrop *)
+(* Basic_1: was: wcpr0_drop *)
 lemma ltpr_ldrop_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 -L1 -K1 -d -e
@@ -34,7 +34,7 @@ lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 
 ]
 qed.
 
-(* Basic_1: was: wcpr0_ldrop_back *)
+(* Basic_1: was: wcpr0_drop_back *)
 lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 →
                         ∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2.
 #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
index 32ddb3a1fc71ab162313f014e6289ae22d01b96f..91b30b0144485257e3d9209b334f4503c8909494 100644 (file)
@@ -35,3 +35,21 @@ lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡
   elim (IHT12 … HL12) -L2 /3 width=5/
 ]
 qed.
+
+lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → ∀L2. L1 ➡ L2 →
+                     ∃∃T. L2 ⊢ T1 [d, e] ▶ T & T2 ➡ T.
+#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
+[ /2 width=3/
+| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L2 #HL12
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #HLK2 #H
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1
+  elim (lift_total V2 0 (i+1)) #W2 #HVW2
+  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=4/
+| #L1 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L2 #HL12
+  elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2
+  elim (IHT12 (L2.ⓑ{I}V) ?) /2 width=1/ -L1 /3 width=5/
+| #L1 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L2 #HL12
+  elim (IHV12 … HL12) -IHV12
+  elim (IHT12 … HL12) -L1 /3 width=5/
+]
+qed.
index c7fc055e7cacf84d8c68f64bd3686c951865b562..c00819a7454644157340366ca2dd9e59c0f2bef8 100644 (file)
@@ -18,7 +18,7 @@ include "Basic_2/substitution/lift.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
-(* Basic_1: includes: ldrop_skip_bind *)
+(* Basic_1: includes: drop_skip_bind *)
 inductive ldrop: nat → nat → relation lenv ≝
 | ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆)
 | ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
@@ -41,7 +41,7 @@ fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 → e = 0 
 ]
 qed.
 
-(* Basic_1: was: ldrop_gen_refl *)
+(* Basic_1: was: drop_gen_refl *)
 lemma ldrop_inv_refl: ∀L1,L2. ⇩[0, 0] L1 ≡ L2 → L1 = L2.
 /2 width=5/ qed-.
 
@@ -55,7 +55,7 @@ fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ →
 ]
 qed.
 
-(* Basic_1: was: ldrop_gen_sort *)
+(* Basic_1: was: drop_gen_sort *)
 lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆.
 /2 width=5/ qed-.
 
@@ -76,7 +76,7 @@ lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 →
                     (0 < e ∧ ⇩[0, e - 1] K ≡ L2).
 /2 width=3/ qed-.
 
-(* Basic_1: was: ldrop_gen_ldrop *)
+(* Basic_1: was: drop_gen_drop *)
 lemma ldrop_inv_ldrop1: ∀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
@@ -97,7 +97,7 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
 ]
 qed.
 
-(* Basic_1: was: ldrop_gen_skip_l *)
+(* Basic_1: was: drop_gen_skip_l *)
 lemma ldrop_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 & 
@@ -117,7 +117,7 @@ fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
 ]
 qed.
 
-(* Basic_1: was: ldrop_gen_skip_r *)
+(* Basic_1: was: drop_gen_skip_r *)
 lemma ldrop_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.
@@ -125,7 +125,7 @@ lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 <
 
 (* Basic properties *********************************************************)
 
-(* Basic_1: was by definition: ldrop_refl *)
+(* Basic_1: was by definition: drop_refl *)
 lemma ldrop_refl: ∀L. ⇩[0, 0] L ≡ L.
 #L elim L -L //
 qed.
@@ -166,7 +166,7 @@ qed.
 
 (* Basic forvard lemmas *****************************************************)
 
-(* Basic_1: was: ldrop_S *)
+(* Basic_1: was: drop_S *)
 lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
                         ⇩[O, e + 1] L1 ≡ K2.
 #L1 elim L1 -L1
@@ -212,16 +212,16 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e.
 qed-.
 
 (* Basic_1: removed theorems 49:
-            ldrop_skip_flat
+            drop_skip_flat
             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
-            ldrop_clear ldrop_clear_O ldrop_clear_S
+            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
             getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans
-            getl_clear_bind getl_clear_conf getl_dec getl_ldrop getl_ldrop_conf_lt
-            getl_ldrop_conf_ge getl_conf_ge_ldrop getl_ldrop_conf_rev
-            ldrop_getl_trans_lt ldrop_getl_trans_le ldrop_getl_trans_ge
-            getl_ldrop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O
+            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
 *)
index 91c0c6b705bb0a3b656b5b3f804ca7fb25b6c37e..90f724ad36f93a19d2570ccbc88d62eae1bae8e0 100644 (file)
@@ -19,7 +19,7 @@ include "Basic_2/substitution/ldrop.ma".
 
 (* Main properties **********************************************************)
 
-(* Basic_1: was: ldrop_mono *)
+(* Basic_1: was: drop_mono *)
 theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 →
                     ∀L2. ⇩[d, e] L ≡ L2 → L1 = L2.
 #d #e #L #L1 #H elim H -d -e -L -L1
@@ -36,7 +36,7 @@ theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 →
 ]
 qed-.
 
-(* Basic_1: was: ldrop_conf_ge *)
+(* Basic_1: was: drop_conf_ge *)
 theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
                        ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
                        ⇩[0, e2 - e1] L1 ≡ L2.
@@ -55,7 +55,7 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
 ]
 qed.
 
-(* Basic_1: was: ldrop_conf_lt *)
+(* Basic_1: was: drop_conf_lt *)
 theorem ldrop_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
@@ -77,7 +77,7 @@ theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
 ]
 qed.
 
-(* Basic_1: was: ldrop_trans_le *)
+(* Basic_1: was: drop_trans_le *)
 theorem ldrop_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.
@@ -99,7 +99,7 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
 ]
 qed.
 
-(* Basic_1: was: ldrop_trans_ge *)
+(* Basic_1: was: drop_trans_ge *)
 theorem ldrop_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 -d1 -e1 -L1 -L
@@ -121,6 +121,6 @@ theorem ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
 #e1 #e1 #e2 >commutative_plus /2 width=5/
 qed.
 
-(* Basic_1: was: ldrop_conf_rev *)
+(* Basic_1: was: drop_conf_rev *)
 axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L →
                  ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1.
index c4b6c87f0c2831e38f632753e584d455278c3ea5..4f30025d31ce166d86fe2391364f4b0cbc9c7be5 100644 (file)
@@ -179,9 +179,9 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d 
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 27:
-            csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq
+            csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
             csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
-            csubst0_ldrop_gt_back csubst0_ldrop_eq_back csubst0_ldrop_lt_back
+            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