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
--- /dev/null
+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
+*)
(**************************************************************************)
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 **********************)
/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-.
]
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).
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-.
projects / helm.git / commitdiff