From 89fc31fc5cc01e8860cf67a8e096c24125370d31 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 14 Oct 2019 21:33:52 +0200
Subject: [PATCH] some added lemmas removed from auto

+ they make auto very slow in some cases,
for instance the /7 width=6 by .../ of contribs/lambdadelta/static_2/relocation/drops.ma

+ WIP on lambdadelta ...
---
 matita/components/ng_tactics/nnAuto.ml        | 13 +++---
 .../basic_2/dynamic/cnv_cpce_etc.ma           | 30 +++++++++++++
 .../basic_2/rt_conversion/cpce_drops.ma       | 44 +++++++++++++++++++
 .../lambdadelta/static_2/relocation/lifts.ma  | 16 +++++++
 .../static_2/relocation/lifts_lifts.ma        |  7 +++
 5 files changed, 105 insertions(+), 5 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce_etc.ma

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 3ac6040dc..d371409d2 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1925,11 +1925,14 @@ let candidates_from_ctx univ ctx status =
             let status, res = disambiguate status ctx t `XTNone in 
             let _,res = term_of_cic_term status res (ctx_of res) 
             in Ast.NCic res 
-        in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
-                                        Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
-                                        Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
-                                        Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
-                                       ])
+        in Some (List.map to_Ast l)
+(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases 
+                                    @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
+                                       Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
+                                       Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
+                                       Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
+                                      ]
+*)
 
 let auto_lowtac ~params:(univ,flags) status goal =
     let gty = get_goalty status goal in
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce_etc.ma
new file mode 100644
index 000000000..861161f21
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce_etc.ma
@@ -0,0 +1,30 @@
+include "basic_2/dynamic/cnv_cpce.ma".
+
+lemma pippo (h) (a) (G) (L0):
+      ∀T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
+      ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
+      ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 →
+      ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L0⦄ ⊢ T2 ➡[n,h] T. 
+#h #a #G #L0 * *
+[ #s #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01
+  elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
+  lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+  /3 width=3 by cpce_sort, cpm_sort, ex2_intro/
+| #i #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01
+  elim (drops_F_uni L0 i)
+  [
+  | *    
+
+(*
+lemma cpce_inv_eta_drops (h) (n) (G) (L) (i):
+      ∀X. ⦃G,L⦄ ⊢ #i ⬌η[h] X →
+      ∀K,W. ⇩*[i] L ≘ K.ⓛW →
+      ∀p,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
+      ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
+      ∀W2. ⇧*[↑i] V2 ≘ W2 → X = +ⓛW2.ⓐ#0.#↑i.
+
+theorem cpce_mono_cnv (h) (a) (G) (L):
+        ∀T. ⦃G,L⦄ ⊢ T ![h,a] →
+        ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → T1 = T2.
+#h #a #G #L #T #HT
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
index 6e8afb63c..985f9f8f4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "static_2/relocation/drops.ma".
+include "static_2/relocation/lifts_lifts.ma".
 include "basic_2/rt_conversion/cpce.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
@@ -44,3 +45,46 @@ lemma cpce_zero_drops (h) (G):
   /5 width=8 by cpce_lref, drops_drop/
 ]
 qed.
+
+(* Inversion lemmas with uniform slicing for local environments *************)
+
+lemma cpce_inv_lref_sn_drops (h) (G) (i) (L):
+      ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 →
+      ∀I,K. ⇩*[i] L ≘ K.ⓘ{I} →
+      ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2
+       | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
+                           & ⇧*[↑i] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#(↑i) = X2.
+#h #G #i elim i -i
+[ #L #X2 #HX2 #I #K #HLK
+  lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct
+  /2 width=1 by cpce_inv_zero_sn/
+| #i #IH #L0 #X0 #HX0 #J #K #H0
+  elim (drops_inv_succ … H0) -H0 #I #L #HLK #H destruct
+  elim (cpce_inv_lref_sn … HX0) -HX0 #X2 #HX2 #HX20
+  elim (IH … HX2 … HLK) -IH -I -L *
+  [ #HJ #H destruct
+    lapply (lifts_inv_lref1_uni … HX20) -HX20 #H destruct
+    /4 width=7 by or_introl, conj/
+  | #n #p #W #V1 #V2 #W2 #U #HWU #HV12 #HVW2 #H1 #H2 destruct
+    elim (lifts_inv_bind1 … HX20) -HX20 #X2 #X #HWX2 #HX #H destruct
+    elim (lifts_inv_flat1 … HX) -HX #X0 #X1 #H0 #H1 #H destruct
+    lapply (lifts_inv_push_zero_sn … H0) -H0 #H destruct
+    elim (lifts_inv_push_succ_sn … H1) -H1 #j #Hj #H destruct
+    lapply (lifts_inv_lref1_uni … Hj) -Hj #H destruct
+    /4 width=12 by lifts_trans_uni, ex5_7_intro, or_intror/
+  ]
+]
+qed-.
+
+lemma cpce_inv_zero_sn_drops (h) (G) (i) (L):
+      ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 →
+      ∀I,K. ⇩*[i] L ≘ K.ⓘ{I} →
+      (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+      #i = X2.
+#h #G #i #L #X2 #HX2 #I #K #HLK #HI
+elim (cpce_inv_lref_sn_drops … HX2 … HLK) -L *
+[ #_ #H //
+| #n #p #W #V1 #V2 #W2 #U #HWU #_ #_ #H destruct
+  elim (HI … HWU) -n -p -K -X2 -V1 -V2 -W2 -U -i //
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index b888af22d..1b3835699 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -287,6 +287,22 @@ lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⇧*[f] ②{I}V.T ≘ T → ⊥.
 ]
 qed-.
 
+lemma lifts_inv_push_zero_sn (f):
+      ∀X. ⇧*[⫯f]#0 ≘ X → #0 = X.
+#f #X #H
+elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct
+lapply (at_inv_ppx … Hi ???) -Hi //
+qed-.
+
+lemma lifts_inv_push_succ_sn (f) (i1):
+      ∀X. ⇧*[⫯f]#(↑i1) ≘ X →
+      ∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X.
+#f #i1 #X #H
+elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
+elim (at_inv_npx … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
+/3 width=3 by lifts_lref, ex2_intro/
+qed-.
+
 (* Inversion lemmas with uniform relocations ********************************)
 
 lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧*[l] #i ≘ Y → Y = #(l+i).
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
index e55582cb9..971d23ac9 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
@@ -133,3 +133,10 @@ lemma deliftable2_sn_bi: ∀R. deliftable2_sn R → deliftable2_bi R.
 elim (HR … HU12 … HTU1) -HR -U1 #X #HUX #HTX
 <(lifts_inj … HUX … HTU2) -U2 -T2 -f //
 qed-.
+
+lemma lifts_trans_uni (T):
+      ∀l1,T1. ⇧*[l1] T1 ≘ T →
+      ∀l2,T2. ⇧*[l2] T ≘ T2 → ⇧*[l1+l2] T1 ≘ T2.
+#T #l1 #T1 #HT1 #l2 #T2 #HT2
+@(lifts_trans … HT1 … HT2) //
+qed-.
-- 
2.39.2