- irreflexivity of static type assignment iterated at least once

- some traces added for auto

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
index 97c77b05d4cdd4a19a48e0d21bc203264804ff73..b170892ea56403863ec25ad8731658848fb3120c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
@@ -20,12 +20,12 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Forward lemmas on lenv refinement for atomic arity assignment ************)
 
 lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃⁝ L2.
-#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
 #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #_ #_ #IHL12
 lapply (snv_scast … HV H1W HVW H1l) -HV -H1W -HVW -H1l #HV
 elim (snv_fwd_aaa … HV) -HV #A #HV
 elim (snv_fwd_aaa … H2W) -H2W #B #HW
 elim (aaa_inv_cast … HV) #HWA #_
 lapply (lsuba_aaa_trans … HW … IHL12) #HWB
-lapply (aaa_mono … HWB … HWA) -HWB -HWA #H destruct /2 width=3/
+lapply (aaa_mono … HWB … HWA) -HWB -HWA #H destruct /2 width=3 by lsuba_beta/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma
index b7eac381af2b3c2a55ba02b3100e4f6e8aefe05c..cd96040bf894f15ec63048196a750dc9c959e72a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma
@@ -20,5 +20,5 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Forward lemmas on lenv refinement for degree assignment ******************)
 
 lemma lsubsv_fwd_lsubd: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃▪[h, g] L2.
-#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=3/
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=3 by lsubd_pair, lsubd_beta/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da_sta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da_sta.ma
index 26f83c888792a9881892edbdcb451946ccf71df6..4f45a81658d6ec92c54db96dda78a51697b47f9d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/da_sta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/da_sta.ma
@@ -51,6 +51,18 @@ lemma sta_da: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U →
 ]
 qed-.
 
+lemma sta_da_ge: ∀h,G,L,T,U,l0. ⦃G, L⦄ ⊢ T •[h] U →
+                 ∃∃g,l. ⦃G, L⦄ ⊢ T ▪[h, g] l & l0 ≤ l.
+#h #G #L #T #U #l0 #H elim H -G -L -T -U
+[ /3 width=4 by da_sort, ex2_2_intro/
+| #G #L #K #V #W #W0 #i #HLK #_ #_ * /3 width=5 by da_ldef, ex2_2_intro/
+| #G #L #K #W #V #W0 #i #HLK #_ #_ * /4 width=5 by da_ldec, lt_to_le, le_S_S, ex2_2_intro/
+| #a #I #G #L #V #T #U #_ * /3 width=4 by da_bind, ex2_2_intro/
+| #G #L #V #T #U #_ * /3 width=4 by da_flat, ex2_2_intro/
+| #G #L #W #T #U #_ * /3 width=4 by da_flat, ex2_2_intro/
+]
+qed-.
+
 (* Inversion lrmmas on static type assignment for terms *********************)
 
 lemma da_inv_sta: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma
index c1726ff5d863558d1d8b762bf6c82c1d7049d877..8b11d1dc0199ea32e7a1ae6dc451c1f00dbd9071 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma
@@ -25,3 +25,16 @@ lemma lstas_da_conf: ∀h,g,G,L,T,U,l1. ⦃G, L⦄ ⊢ T •*[h, l1] U →
 #l1 #U #U0 #_ #HU0 #IHTU #l2 #HT
 <minus_plus /3 width=3 by da_sta_conf/
 qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lstas_inv_refl_pos: ∀h,G,L,T,l. ⦃G, L⦄ ⊢ T •*[h, l+1] T → ⊥.
+#h #G #L #T #l #H elim (lstas_inv_step_sn … H)
+#U #HTU #_ elim (sta_da_ge … (l+1) HTU) -U
+#g #l0 #HT #Hl0 lapply (lstas_da_conf … H … HT) -H
+#H0T lapply (da_mono … HT … H0T) -h -G -L -T
+#H elim (discr_x_minus_xy … H) -H
+[ #H destruct /2 width=3 by le_plus_xSy_O_false/
+| -Hl0 <plus_n_Sm #H destruct 
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 066d9a1f04a9e17f3d826ce4ae3e978fc270b2b8..26898d348056f3367d1c7729c47eedf322d82c9a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -138,6 +138,15 @@ lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
 lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
 /2 width=4 by plus_xySz_x_false/ qed-.
 
+(* Note this should go in nat.ma *)
+lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
+#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
+#y #_ >minus_plus_plus_l
+#H lapply (discr_plus_xy_minus_xz … H) -H
+#H destruct
+qed-.
+
 (* Iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetics/bigops.ma *)