From cf10254638dab42421a9281a9418001d9bdbc8c0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi 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: // ]