From 7de928055eb4f717303fa36e287196c6d93cea78 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 18 Jul 2014 09:49:00 +0000
Subject: [PATCH] - irreflexivity of static type assignment iterated at least
 once - some traces added for auto

---
 .../lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma     |  4 ++--
 .../lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma     |  2 +-
 .../contribs/lambdadelta/basic_2/static/da_sta.ma   | 12 ++++++++++++
 .../contribs/lambdadelta/basic_2/unfold/lstas_da.ma | 13 +++++++++++++
 .../contribs/lambdadelta/ground_2/lib/arith.ma      |  9 +++++++++
 5 files changed, 37 insertions(+), 3 deletions(-)

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 97c77b05d..b170892ea 100644
--- 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 b7eac381a..cd96040bf 100644
--- 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 26f83c888..4f45a8165 100644
--- 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 c1726ff5d..8b11d1dc0 100644
--- 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 066d9a1f0..26898d348 100644
--- 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 *)
-- 
2.39.2