From cf10254638dab42421a9281a9418001d9bdbc8c0 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 5 Oct 2014 14:48:46 +0000
Subject: [PATCH] catched typecheker failures in auto allow more applications
 of the tactic

---
 .../lambdadelta/basic_2/dynamic/snv_lift.ma   |  9 ++++---
 .../lambdadelta/basic_2/dynamic/snv_scpes.ma  |  2 +-
 .../basic_2/equivalence/scpes_scpes.ma        |  8 ++-----
 .../contribs/lambdadelta/basic_2/names.txt    | 10 ++++----
 .../lambdadelta/basic_2/web/basic_2_src.tbl   | 24 +++++++++----------
 5 files changed, 24 insertions(+), 29 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index 09acef6c3..b1b995c2b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -38,10 +38,9 @@ lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⬇[s, d
   /4 width=5 by snv_bind, drop_skip/
 | #a #G #K #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
-  elim (lift_total W0 d e) #W1 #HW01
-  elim (lift_total U0 (d+1) e) #U1 #HU01
-  @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by scpds_lift/ ] -IHV -IHT
-  @(scpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *)
+  elim (lift_total W0 d e)
+  elim (lift_total U0 (d+1) e)
+  /4 width=17 by snv_appl, scpds_lift, lift_bind/
 | #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
   elim (lift_total U0 d e)
@@ -66,7 +65,7 @@ lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⬇[
   /4 width=5 by snv_bind, drop_skip/
 | #a #G #L #W #W1 #U #U1 #l #_ #_ #HW1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
-  elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0  
+  elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0
   elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0
   elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct
   lapply (lift_inj … HY … HW01) -HY #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
index 4895a5105..9ed7e06cb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma
@@ -187,7 +187,7 @@ lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hl12 … HTX2 … HT20) -HT20
 [1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX2 ]
 lapply (lstas_scpes_trans … Hl11 … HTX1 … HX1) [ // ] -Hl11 -HTX1 -HX1 -H1 #H1
 lapply (lstas_scpes_trans … Hl12 … HTX2 … HX2) [ // ] -Hl12 -HTX2 -HX2 -H2 #H2
-lapply (scpes_canc_dx … H1 … H2) // (**) (* full auto raises NTypeChecker failure *)
+/2 width=4 by scpes_canc_dx/ (**) (* full auto fails *)
 qed-.
 
 (* Advanced properties ******************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
index 15c0efacf..e0f79b1c0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
@@ -62,12 +62,8 @@ qed-.
 
 theorem scpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 →
                        ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T #T1 #l #l1 #HT1
-@scpes_trans /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
-qed-.
+/3 width=4 by scpes_trans, scpes_sym/ qed-.
 
 theorem scpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
                        ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2
-@(scpes_trans … HT1) -T1 -l1 /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
-qed-.
+/3 width=4 by scpes_trans, scpes_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 583105a8d..9a3319f5c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -73,17 +73,17 @@ s: strongly normalizing form
 
 - third letter
 
-b: "big tree" reduction
+b: (q)rst-reduction
 c: conversion
-d: decomposed extended reduction
-e: decomposed extended conversion
+d: decomposed rt-reduction
+e: decomposed rt-conversion
 q: restricted reduction
 r: reduction
 s: substitution
 u: supclosure
 w: reserved for generic pointwise extension
-x: extended reduction
-y: extended substitution
+x: rt-reduction
+y: rt-substitution
 
 - forth letter (if present)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 1aeb5138b..9ac05c7b6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -59,7 +59,7 @@ table {
    ]
    class "blue"
    [ { "equivalence" * } {
-        [ { "decomposed extended equivalence" * } {
+        [ { "decomposed rt-equivalence" * } {
              [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
           }
         ]
@@ -79,7 +79,7 @@ table {
    ]
    class "cyan"
    [ { "computation" * } {
-        [ { "evaluation for context-sensitive extended reduction" * } {
+        [ { "evaluation for context-sensitive rt-reduction" * } {
              [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
           }
         ]
@@ -91,7 +91,7 @@ table {
              [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ]
           }
         ]
-        [ { "strongly normalizing extended computation" * } {
+        [ { "strongly normalizing rt-computation" * } {
              [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
              [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ]
@@ -103,11 +103,11 @@ table {
              [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
           }
         ]
-        [ { "decomposed extended computation" * } {
+        [ { "decomposed rt-computation" * } {
              [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
           }
         ]
-        [ { "context-sensitive extended computation" * } {
+        [ { "context-sensitive rt-computation" * } {
              [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
              [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
           }
@@ -134,20 +134,20 @@ table {
              [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_lleq" + "fpb_fleq" * ]
           }
         ]
-        [ { "normal forms for context-sensitive extended reduction" * } {
+        [ { "normal forms for context-sensitive rt-reduction" * } {
              [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
           }
         ]
-        [ { "context-sensitive extended reduction" * } {
+        [ { "context-sensitive rt-reduction" * } {
              [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]
-        [ { "irreducible forms for context-sensitive extended reduction" * } {
+        [ { "irreducible forms for context-sensitive rt-reduction" * } {
              [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
           }
         ]
-        [ { "reducible forms for context-sensitive extended reduction" * } {
+        [ { "reducible forms for context-sensitive rt-reduction" * } {
              [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
           }
         ]
@@ -229,7 +229,7 @@ table {
              [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_leq" + "frees_lift" * ]
           }
         ]
-        [ { "contxt-sensitive extended multiple substitution" * } {
+        [ { "contxt-sensitive multiple rt-substitution" * } {
              [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
           }
         ]
@@ -264,11 +264,11 @@ table {
              [ "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ]
           }
         ]
-        [ { "contxt-sensitive extended ordinary substitution" * } {
+        [ { "contxt-sensitive ordinary rt-substitution" * } {
              [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
           }
         ]
-        [ { "local env. ref. for extended substitution" * } {
+        [ { "local env. ref. for rt-substitution" * } {
              [ "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
           }
         ]
-- 
2.39.2