From 6ec8300c6063ed8096950abb88b7dfc9c4ac2f94 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 21 Feb 2024 10:36:22 +1100 Subject: [PATCH] remove import Std where possible --- Auto/Embedding/LCtx.lean | 89 ++++++++++++------------ Auto/Embedding/Lam2Base.lean | 3 +- Auto/Embedding/LamBase.lean | 3 +- Auto/Embedding/LamBitVec.lean | 12 +--- Auto/Embedding/LamChecker.lean | 4 +- Auto/Embedding/LamConv.lean | 1 - Auto/Embedding/Lift.lean | 1 - Auto/Lib/BinTree.lean | 2 - Auto/Lib/IntExtra.lean | 1 - Auto/Lib/ListExtra.lean | 1 - Auto/Lib/MetaState.lean | 4 +- Auto/Lib/NatExtra.lean | 2 - Auto/Lib/Pos.lean | 1 - Auto/Translation/Assumptions.lean | 1 - Auto/Translation/LamReif.lean | 1 - Test/SmtTranslation/MatchWorkaround.lean | 7 +- lake-manifest.json | 4 +- lakefile.lean | 2 +- lean-toolchain | 2 +- 19 files changed, 60 insertions(+), 81 deletions(-) diff --git a/Auto/Embedding/LCtx.lean b/Auto/Embedding/LCtx.lean index b576334..39e2d3b 100644 --- a/Auto/Embedding/LCtx.lean +++ b/Auto/Embedding/LCtx.lean @@ -4,7 +4,6 @@ import Auto.Lib.NatExtra import Auto.Lib.ListExtra import Auto.Lib.HList import Auto.Lib.BinTree -import Std.Data.List.Lemmas namespace Auto.Embedding @@ -23,7 +22,7 @@ section generic dsimp rw [Nat.sub_add_cancel (Nat.le_of_ble_eq_true h)] | false => rfl - + theorem mapAt_id_eq_id' (pos : Nat) : mapAt pos (fun x => x) = id := mapAt_id_eq_id pos @@ -52,7 +51,7 @@ section generic rw [hble]; dsimp; rw [Nat.add_sub_cancel] | false => dsimp; rw [h] - + @[reducible] def restoreAt {α} (pos : Nat) (restore : (Nat → α) → (Nat → α)) := fun (lctx : Nat → α) (n : Nat) => match pos.ble n with @@ -76,11 +75,11 @@ section generic def coPair {α} (f : Nat → Nat) (restore : (Nat → α) → (Nat → α)) := ∀ (lctx : Nat → α) (n : Nat), (restore lctx) (f n) = lctx n - + def coPairAt {α} (f : Nat → Nat) (restore : (Nat → α) → (Nat → α)) := ∀ (pos : Nat) (lctx : Nat → α) (n : Nat), (restoreAt pos restore lctx) (mapAt pos f n) = lctx n - + theorem coPairAt.ofcoPair (cp : coPair f restore) : coPairAt f restore := by intros pos lctx n; dsimp [restoreAt, mapAt] @@ -238,7 +237,7 @@ end generic section push - + @[reducible] def pushLCtx (x : α) (lctx : Nat → α) (n : Nat) : α := match n with | 0 => x @@ -256,7 +255,7 @@ section push dsimp [pushLCtxAt, restoreAt] rw [show (pos.ble pos = true) by (apply Nat.ble_eq_true_of_le; apply Nat.le_refl)] rw [Nat.sub_self] - + theorem pushLCtxAt_gt (x : α) (pos : Nat) (n : Nat) (hle : n > pos) : pushLCtxAt x pos lctx n = lctx n.pred := by dsimp [pushLCtxAt, restoreAt] rw [show (pos.ble n = true) by (apply Nat.ble_eq_true_of_le; apply Nat.le_of_lt hle)] @@ -274,15 +273,15 @@ section push theorem pushLCtxAt_succ_zero (x : α) (pos : Nat) (lctx : Nat → α) : pushLCtxAt x (.succ pos) lctx 0 = lctx 0 := rfl - + theorem pushLCtxAt_succ_succ (x : α) (pos : Nat) (lctx : Nat → α) (n : Nat) : pushLCtxAt x (.succ pos) lctx (.succ n) = pushLCtxAt x pos (fun n => lctx (.succ n)) n := restoreAt_succ_succ _ _ _ _ - + theorem pushLCtxAt_succ_succ_Fn (x : α) (pos : Nat) (lctx : Nat → α) : (fun n => pushLCtxAt x (.succ pos) lctx (.succ n)) = pushLCtxAt x pos (fun n => lctx (.succ n)) := restoreAt_succ_succ_Fn _ _ _ - + theorem pushLCtxAt_comm (f : α → β) (x : α) (pos : Nat) (lctx : Nat → α) (n : Nat) : f (pushLCtxAt x pos lctx n) = pushLCtxAt (f x) pos (f ∘ lctx) n := by dsimp [pushLCtxAt, restoreAt] @@ -292,11 +291,11 @@ section push | 0 => rfl | _ + 1 => rfl | false => rfl - + theorem pushLCtxAt_commFn (f : α → β) (x : α) (pos : Nat) (lctx : Nat → α) : (fun n => f (pushLCtxAt x pos lctx n)) = (fun n => pushLCtxAt (f x) pos (fun n => f (lctx n)) n) := funext (pushLCtxAt_comm f x pos lctx) - + @[reducible] def pushLCtxDep {lctxty : α → Sort u} {xty : α} (x : lctxty xty) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) : lctxty (pushLCtx xty rty n) := by dsimp [pushLCtx] @@ -315,7 +314,7 @@ section push cases h₁; cases h₂; cases h₃; cases h₄; cases h₅; cases h₆; apply HEq.refl theorem pushLCtxDep_substLCtx - {lctxty : α → Sort u} {ty : α} (x : lctxty ty) + {lctxty : α → Sort u} {ty : α} (x : lctxty ty) {rty₁ : Nat → α} (lctx₁ : ∀ n, lctxty (rty₁ n)) {rty₂ : Nat → α} (lctx₂ : ∀ n, lctxty (rty₂ n)) (h₁ : rty₁ = rty₂) (h₂ : HEq lctx₁ lctx₂) : @@ -333,7 +332,7 @@ section push def pushLCtxAtDep {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) : lctxty (pushLCtxAt xty pos rty n) := restoreAtDep pos (pushLCtxDep x) lctx n - + theorem pushLCtxAtDep_heq {lctxty₁ : α₁ → Sort u} {ty₁ : α₁} (x₁ : lctxty₁ ty₁) (pos₁ : Nat) (rty₁ : Nat → α₁) (lctx₁ : ∀ n, lctxty₁ (rty₁ n)) @@ -367,17 +366,17 @@ section push theorem pushLCtxAtDep_succ_zero {rty : Nat → α} {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) : pushLCtxAtDep x (.succ pos) lctx 0 = lctx 0 := rfl - + theorem pushLCtxAtDep_succ_succ {rty : Nat → α} {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) (n : Nat) : HEq (pushLCtxAtDep x (.succ pos) lctx (.succ n)) (pushLCtxAtDep x pos (fun n => lctx (.succ n)) n) := restoreAtDep_succ_succ _ _ _ _ - + theorem pushLCtxAtDep_succ_succ_Fn {rty : Nat → α} {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) : HEq (fun n => pushLCtxAtDep x (.succ pos) lctx (.succ n)) (pushLCtxAtDep x pos (fun n => lctx (.succ n))) := restoreAtDep_succ_succ_Fn _ _ _ - + def pushLCtxAtDep_comm {α : Sort w} {β : α → Sort x} {rty : Nat → α} {lctxty : α → Sort u} (f : ∀ (x : α), lctxty x → β x) {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) (n : Nat) : @@ -389,11 +388,11 @@ section push | 0 => rfl | _ + 1 => rfl | false => rfl - + def pushLCtxAtDep.nonDep {rty : Nat → α} {lctxty : Sort u} {xty : α} (x : lctxty) (pos : Nat) (lctx : Nat → lctxty) (n : Nat) : @pushLCtxAtDep _ (fun _ => lctxty) xty x pos rty lctx n = pushLCtxAt x pos lctx n := rfl - + def pushLCtxAtDep_absorbAux {rty : Nat → α} {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) (n : Nat) : HEq @@ -407,36 +406,36 @@ section push | 0 => rfl | _ + 1 => rfl | false => rfl - + theorem pushLCtxAtDep_absorb {rty : Nat → α} {lctxty : α → Sort u} {xty : α} (x : lctxty xty) (pos : Nat) (lctx : ∀ n, lctxty (rty n)) : HEq (@pushLCtxAtDep _ lctxty _ x pos rty lctx) (@pushLCtxAtDep _ id _ x pos (lctxty ∘ rty) lctx) := HEq.funext _ _ (pushLCtxAtDep_absorbAux _ _ _) - + theorem pushLCtx_zero (x : α) (lctx : Nat → α) : pushLCtx x lctx 0 = x := rfl theorem pushLCtx_succ (x : α) (lctx : Nat → α) (n : Nat) : pushLCtx x lctx (.succ n) = lctx n := rfl - + theorem pushLCtx_succ_Fn (x : α) (lctx : Nat → α) : (fun n => pushLCtx x lctx (.succ n)) = lctx := rfl - + theorem pushLCtx_comm (f : α → β) (x : α) (lctx : Nat → α) (n : Nat) : f (pushLCtx x lctx n) = pushLCtx (f x) (fun n => f (lctx n)) n := by rw [← pushLCtxAt_zero]; rw [← pushLCtxAt_zero] apply pushLCtxAt_comm f x 0 lctx n - + theorem pushLCtx_commFn (f : α → β) (x : α) (lctx : Nat → α) : (fun n => f (pushLCtx x lctx n)) = (fun n => pushLCtx (f x) (fun n => f (lctx n)) n) := funext (pushLCtx_comm f x lctx) - + theorem pushLCtx_pushLCtxAt (x y : α) (pos : Nat) (lctx : Nat → α) : pushLCtx y (pushLCtxAt x pos lctx) = pushLCtxAt x (Nat.succ pos) (pushLCtx y lctx) := by apply funext; intro n; cases n; rfl; rw [pushLCtxAt_succ_succ]; - + theorem pushLCtxDep_zero {lctxty : α → Sort u} {xty : α} (x : lctxty xty) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) : pushLCtxDep x lctx 0 = x := rfl - + theorem pushLCtxDep_succ {lctxty : α → Sort u} {xty : α} (x : lctxty xty) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) : pushLCtxDep x lctx (.succ n) = lctx n := rfl @@ -444,7 +443,7 @@ section push theorem pushLCtxDep_succ_Fn {lctxty : α → Sort u} {xty : α} (x : lctxty xty) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) : (fun n => pushLCtxDep x lctx (.succ n)) = lctx := rfl - + theorem pushLCtxDep_comm {α : Sort w} {β : α → Sort x} {rty : Nat → α} {lctxty : α → Sort u} (f : ∀ (x : α), lctxty x → β x) (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) (n : Nat) : @@ -455,7 +454,7 @@ section push theorem pushLCtx_commDep {β : α → Sort x} {x : α} {lctx : Nat → α} (f : ∀ (x : α), β x) : HEq (f (pushLCtx x lctx n)) (pushLCtxDep (f x) (fun n => f (lctx n)) n) := by cases n <;> rfl - + theorem pushLCtxDep_absorbAux {rty : Nat → α} {lctxty : α → Sort u} (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) (n : Nat) : HEq @@ -463,12 +462,12 @@ section push (@pushLCtxDep _ id _ x (lctxty ∘ rty) lctx n) := by dsimp [pushLCtx, pushLCtxDep] cases n <;> rfl - + theorem pushLCtxDep_absorb {rty : Nat → α} {lctxty : α → Sort u} (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) : HEq (@pushLCtxDep _ lctxty _ x rty lctx) (@pushLCtxDep _ id _ x (lctxty ∘ rty) lctx) := HEq.funext _ _ (fun n => pushLCtxDep_absorbAux lctx x n) - + theorem pushLCtxDep_pushLCtxAtDep {rty : Nat → α} {lctxty : α → Sort u} (lctx : ∀ n, lctxty (rty n)) {xty : α} (x : lctxty xty) {yty : α} (y : lctxty yty) (pos : Nat) : HEq (pushLCtxDep y (pushLCtxAtDep x pos lctx)) (pushLCtxAtDep x (Nat.succ pos) (pushLCtxDep y lctx)) := by @@ -587,7 +586,7 @@ section push cases h₁; cases h₂; cases h₃; cases h₄; cases h₅; cases h₆; apply HEq.rfl theorem pushLCtxsDep_substLCtx - {tys : List α} {lctxty : _} (xs : HList lctxty tys) + {tys : List α} {lctxty : _} (xs : HList lctxty tys) {rty₁ : Nat → α} (lctx₁ : ∀ n, lctxty (rty₁ n)) {rty₂ : Nat → α} (lctx₂ : ∀ n, lctxty (rty₂ n)) (h₁ : rty₁ = rty₂) (h₂ : HEq lctx₁ lctx₂) : @@ -638,7 +637,7 @@ section push (xs : HList lctxty tys) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) : HEq (fun n => pushLCtxsDep (.cons x xs) lctx (.succ n)) (pushLCtxsDep xs lctx) := HEq.funext _ _ (fun n => pushLCtxsDep_cons_succ x xs lctx n) - + theorem pushLCtxsDep_append {lctxty : α → Sort u} {as bs : List α} (xs : HList lctxty as) (ys : HList lctxty bs) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) : @@ -711,13 +710,13 @@ section push {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) : pushLCtxsAtDep xs (.succ pos) lctx 0 = lctx 0 := rfl - theorem pushLCtxsAtDep_succ_succ + theorem pushLCtxsAtDep_succ_succ {lctxty : α → Sort u} {tys : List α} (xs : HList lctxty tys) (pos : Nat) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) (n : Nat) : HEq (pushLCtxsAtDep xs (.succ pos) lctx (.succ n)) (pushLCtxsAtDep xs pos (fun n => lctx (.succ n)) n) := by dsimp [pushLCtxsAtDep]; apply restoreAtDep_succ_succ - theorem pushLCtxsAtDep_succ_succ_Fn + theorem pushLCtxsAtDep_succ_succ_Fn {lctxty : α → Sort u} {tys : List α} (xs : HList lctxty tys) (pos : Nat) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) : HEq (fun n => pushLCtxsAtDep xs (.succ pos) lctx (.succ n)) (pushLCtxsAtDep xs pos (fun n => lctx (.succ n))) := by @@ -853,7 +852,7 @@ section pushs_pops pushLCtx (lctx 0) (fun n => lctx (.succ n)) = lctx := by apply funext intro n; cases n <;> rfl - + theorem pushs_pops_eq (lctx : Nat → α) : pushLCtxs (List.ofFun lctx lvl) (fun n => lctx (n + lvl)) = lctx := by apply funext; intro n; dsimp [pushLCtxs, List.getD] @@ -868,7 +867,7 @@ section pushs_pops dsimp [Nat.blt] at h; let h' := Nat.lt_of_ble_eq_false h exact Nat.le_of_succ_le_succ h' - + theorem ofFun_pushs (heq : xs.length = n) : List.ofFun (pushLCtxs xs lctx) n = xs := by cases heq; induction xs generalizing lctx @@ -903,14 +902,14 @@ end pushs_pops section add_nat - + @[reducible] def addAt (lvl pos : Nat) := mapAt pos (fun x => x + lvl) @[reducible] def succAt := addAt 1 theorem addAt_succ_zero (lvl pos : Nat) : addAt lvl (.succ pos) 0 = 0 := rfl - + theorem addAt_succ_succ (lvl pos : Nat) (n : Nat) : addAt lvl (.succ pos) (.succ n) = .succ (addAt lvl pos n) := by dsimp [addAt]; rw [mapAt_succ_succ] @@ -919,14 +918,14 @@ section add_nat addAt (.succ lvl) pos n = succAt pos (addAt lvl pos n) := by dsimp [addAt, Nat.add_succ] rw [mapAt_comp pos Nat.succ (fun x => x + lvl) n] - + def addAt_succ_r (lvl pos : Nat) (n : Nat) : addAt (.succ lvl) pos n = addAt lvl pos (succAt pos n) := by dsimp [addAt]; have heq : (fun x => x + Nat.succ lvl) = (fun x => (Nat.succ x) + lvl) := by apply funext; intros x; rw [Nat.succ_add]; rfl rw [heq]; rw [mapAt_comp pos (fun x => x + lvl) Nat.succ n] - + def addAt_zero (pos : Nat) : addAt 0 pos = id := by apply funext; intro n; dsimp [addAt]; @@ -1018,17 +1017,17 @@ section genericInst rw [← IH xs heq lctx n] dsimp [pushLCtxs, Nat.blt, Nat.ble, Nat.add_succ] rw [Nat.succ_sub_succ] - + theorem contraPair.ofPushsPops (lvl : Nat) (xs : List α) (heq : xs.length = lvl) : contraPair (fun n => n + lvl) (fun lctx => List.ofFun lctx lvl = xs) (pushLCtxs xs) := by intro lctx hcstr; cases hcstr; apply pushs_pops_eq - + theorem coPairDep.ofPushsDepPopsDep {lctxty : α → Sort u} (lvl : Nat) {tys : List α} (xs : HList lctxty tys) (heq : tys.length = lvl) : coPairDep lctxty (fun x => x + lvl) (pushLCtxs tys) (pushLCtxsDep xs) := And.intro (coPair.ofPushsPops lvl tys heq) (fun {rty} lctx n => by - dsimp [pushLCtxsDep, pushLCtxs]; + dsimp [pushLCtxsDep, pushLCtxs]; induction lvl generalizing tys lctx n case zero => cases xs; @@ -1051,4 +1050,4 @@ section genericInst And.intro (contraPair.ofPushsPops lvl tys heq) (fun {rty} hcstr lctx hcstrDep => by cases hcstr; cases hcstrDep; apply pushsDep_popsDep_eq) -end genericInst \ No newline at end of file +end genericInst diff --git a/Auto/Embedding/Lam2Base.lean b/Auto/Embedding/Lam2Base.lean index ef2a2c4..7684da6 100644 --- a/Auto/Embedding/Lam2Base.lean +++ b/Auto/Embedding/Lam2Base.lean @@ -1,5 +1,4 @@ import Auto.Embedding.Lift -import Std.Data.List.Lemmas namespace Auto.Embedding.Lam₂ @@ -192,4 +191,4 @@ def Lam₂Type.check_iff_interp | .none, _ => simp; cases cifn : interp val lctx fn <;> simp -end Auto.Embedding.Lam₂ \ No newline at end of file +end Auto.Embedding.Lam₂ diff --git a/Auto/Embedding/LamBase.lean b/Auto/Embedding/LamBase.lean index 1aa5ff9..7a830be 100644 --- a/Auto/Embedding/LamBase.lean +++ b/Auto/Embedding/LamBase.lean @@ -8,6 +8,7 @@ import Auto.Lib.HEqExtra import Auto.Lib.ListExtra -- import Mathlib.Data.Real.Basic import Auto.MathlibEmulator +import Std.Data.List.Lemmas -- Embedding Simply Typed Lambda Calculus into Dependent Type Theory -- Simply Typed Lambda Calculus = HOL (without polymorphism) @@ -3671,7 +3672,7 @@ def LamWF.bvarApps have tyeq : ty = lctxr ex.length := by have exlt : List.length ex < List.length (List.reverse (ty :: ex)) := by rw [List.length_reverse]; apply Nat.le_refl - dsimp; rw [← List.reverseAux, List.reverseAux_eq] + dsimp [lctxr]; rw [← List.reverseAux, List.reverseAux_eq] rw [pushLCtxs_lt (by rw [List.length_append]; apply Nat.le_trans exlt (Nat.le_add_right _ _))] dsimp [List.getD]; rw [List.get?_append exlt]; rw [List.get?_reverse _ (by dsimp [List.length]; apply Nat.le_refl _)] diff --git a/Auto/Embedding/LamBitVec.lean b/Auto/Embedding/LamBitVec.lean index d664917..e52b0ba 100644 --- a/Auto/Embedding/LamBitVec.lean +++ b/Auto/Embedding/LamBitVec.lean @@ -1,8 +1,5 @@ import Auto.Embedding.LamConv import Auto.Lib.NatExtra -import Std.Data.Int.Lemmas -import Std.Data.Fin.Lemmas -import Std.Data.BitVec.Lemmas namespace Auto.Embedding.Lam @@ -96,7 +93,7 @@ namespace BitVec apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h) theorem ushiftRight_ge_length_eq_zero' (a : Std.BitVec n) (i : Nat) : i ≥ n → (a.toNat >>> i)#n = 0#n := by - intro h; apply congr_arg (@Std.BitVec.ofNat n) + intro h; apply congrArg (@Std.BitVec.ofNat n) rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)] apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h) @@ -114,12 +111,7 @@ namespace BitVec rw [Nat.pred_lt_iff_le (Nat.two_pow_pos _)] apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h) rw [hzero]; apply eq_of_val_eq; rw [toNat_not] - rw [toNat_ofNat, toNat_neg, toNat_ofNat, Nat.zero_mod, Nat.sub_zero] - cases n <;> try rfl - case succ n => - have hlt : 2 ≤ 2 ^ Nat.succ n := @Nat.pow_le_pow_of_le_right 2 (.step .refl) 1 (.succ n) (Nat.succ_le_succ (Nat.zero_le _)) - rw [Nat.mod_eq_of_lt (a:=1) hlt] - rw [Nat.mod_eq_of_lt]; apply Nat.sub_lt (Nat.le_trans (.step .refl) hlt) .refl + simp theorem shiftRight_eq_zero_iff (a : Std.BitVec n) (b : Nat) : a >>> b = 0#n ↔ a.toNat < 2 ^ b := by rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩; diff --git a/Auto/Embedding/LamChecker.lean b/Auto/Embedding/LamChecker.lean index 978b901..14ab85a 100644 --- a/Auto/Embedding/LamChecker.lean +++ b/Auto/Embedding/LamChecker.lean @@ -1648,7 +1648,7 @@ theorem EtomStep.eval_correct exists replaceAtDep eVarVal' r.maxEVarSucc eV apply And.intro ?left (And.intro hsk ?right) case left => - intro n hlt; dsimp [replaceAt, replaceAtDep] + intro n hlt; dsimp [replaceAt, replaceAtDep, levt'] rw [Nat.beq_eq_false_of_ne (Nat.ne_of_lt hlt)] case right => apply Nat.le_trans (LamTerm.maxEVarSucc_skolemize? h₂) @@ -1675,7 +1675,7 @@ theorem EtomStep.eval_correct exists replaceAtDep eVarVal' r.maxEVarSucc eV apply And.intro ?left (And.intro hdef ?right) case left => - intro n hlt; dsimp [replaceAt, replaceAtDep] + intro n hlt; dsimp [replaceAt, replaceAtDep, levt'] rw [Nat.beq_eq_false_of_ne (Nat.ne_of_lt hlt)] case right => rw [LamTerm.maxEVarSucc_mkEq]; dsimp [LamTerm.maxEVarSucc] diff --git a/Auto/Embedding/LamConv.lean b/Auto/Embedding/LamConv.lean index c065a3f..a2a9767 100644 --- a/Auto/Embedding/LamConv.lean +++ b/Auto/Embedding/LamConv.lean @@ -1,5 +1,4 @@ import Auto.Embedding.LamSystem -import Std.Data.Array.Basic namespace Auto.Embedding.Lam diff --git a/Auto/Embedding/Lift.lean b/Auto/Embedding/Lift.lean index f9a5c37..5002732 100644 --- a/Auto/Embedding/Lift.lean +++ b/Auto/Embedding/Lift.lean @@ -1,4 +1,3 @@ -import Std.Data.BitVec.Basic import Auto.Lib.IsomType import Auto.Lib.StringExtra import Auto.Lib.BoolExtra diff --git a/Auto/Lib/BinTree.lean b/Auto/Lib/BinTree.lean index 5893752..f34542b 100644 --- a/Auto/Lib/BinTree.lean +++ b/Auto/Lib/BinTree.lean @@ -1,6 +1,4 @@ import Lean -import Std.Data.Nat.Lemmas -import Std.Logic import Auto.MathlibEmulator import Auto.Lib.BoolExtra import Auto.Lib.NatExtra diff --git a/Auto/Lib/IntExtra.lean b/Auto/Lib/IntExtra.lean index 91d0e4d..5e2871e 100644 --- a/Auto/Lib/IntExtra.lean +++ b/Auto/Lib/IntExtra.lean @@ -1,5 +1,4 @@ import Auto.Lib.NatExtra -import Std.Data.Int.Lemmas namespace Auto def Int.beq : Int → Int → Bool diff --git a/Auto/Lib/ListExtra.lean b/Auto/Lib/ListExtra.lean index 190f7bb..0dec1f8 100644 --- a/Auto/Lib/ListExtra.lean +++ b/Auto/Lib/ListExtra.lean @@ -1,4 +1,3 @@ -import Std.Data.List.Lemmas import Auto.Lib.IsomType namespace Auto diff --git a/Auto/Lib/MetaState.lean b/Auto/Lib/MetaState.lean index 72e2b3a..910ede4 100644 --- a/Auto/Lib/MetaState.lean +++ b/Auto/Lib/MetaState.lean @@ -35,7 +35,7 @@ protected def saveState : MetaStateM SavedState := def SavedState.restore (b : SavedState) : MetaStateM Unit := do Core.restore b.core - modify fun s => { s with mctx := b.meta.mctx, zetaFVarIds := b.meta.zetaFVarIds, postponed := b.meta.postponed } + modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed } instance : MonadBacktrack SavedState MetaStateM where saveState := MetaState.saveState @@ -144,4 +144,4 @@ def withLetDecl (n : Name) (type : Expr) (val : Expr) (kind : LocalDeclKind) : M withNewFVar fvar type return fvarId -end Auto.MetaState \ No newline at end of file +end Auto.MetaState diff --git a/Auto/Lib/NatExtra.lean b/Auto/Lib/NatExtra.lean index 41a5ae8..8d779e8 100644 --- a/Auto/Lib/NatExtra.lean +++ b/Auto/Lib/NatExtra.lean @@ -1,5 +1,3 @@ -import Std.Data.Nat.Lemmas -import Std.Data.Nat.Bitwise import Auto.Lib.BoolExtra namespace Auto diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean index b01f6cb..8257134 100644 --- a/Auto/Lib/Pos.lean +++ b/Auto/Lib/Pos.lean @@ -1,5 +1,4 @@ import Auto.MathlibEmulator -import Std.Data.Nat.Lemmas namespace Auto diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean index 6d9eda0..81d5fd1 100644 --- a/Auto/Translation/Assumptions.lean +++ b/Auto/Translation/Assumptions.lean @@ -1,5 +1,4 @@ import Lean -import Std.Data.Array.Basic import Auto.Lib.BoolExtra import Auto.Lib.MessageData import Auto.Lib.ExprExtra diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean index 9070d50..c49d111 100644 --- a/Auto/Translation/LamReif.lean +++ b/Auto/Translation/LamReif.lean @@ -1,5 +1,4 @@ import Lean -import Std.Data.Array.Basic import Auto.Lib.MonadUtils import Auto.Lib.ExprExtra import Auto.Lib.MetaExtra diff --git a/Test/SmtTranslation/MatchWorkaround.lean b/Test/SmtTranslation/MatchWorkaround.lean index 9cbefd7..61be638 100644 --- a/Test/SmtTranslation/MatchWorkaround.lean +++ b/Test/SmtTranslation/MatchWorkaround.lean @@ -1,5 +1,4 @@ import Auto.Tactic -import Std.Data.BitVec set_option auto.smt true set_option auto.smt.trust true set_option trace.auto.smt.printCommands true @@ -22,10 +21,10 @@ def Zone.MinArea1 : Zone → Area abbrev Zone.MinArea1.defeq_spec := Zone.MinArea1 .Z1 = 10000 ∧ Zone.MinArea1 .Z2 = 5000 ∧ Zone.MinArea1 .Z3 = 3500 ∧ Zone.MinArea1 .Z4 = 2500 -theorem Zone.MinArea1.defeq : defeq_spec := by simp +theorem Zone.MinArea1.defeq : defeq_spec := by simp [defeq_spec, Zone.MinArea1] -example (x: Zone) : x.MinArea1 >= 2500 := by cases x <;> simp -- succeeds +example (x: Zone) : x.MinArea1 >= 2500 := by cases x <;> simp [Zone.MinArea1] -- succeeds example (x: Zone) : x.MinArea1 >= 2500 := by auto [Zone.MinArea1.defeq] def Zone.MinArea2 : Zone → Area @@ -38,7 +37,7 @@ abbrev Zone.MinArea2.defeq_spec := Zone.MinArea2 .Z1 = 0 ∧ Zone.MinArea2 .Z2 = 5000 ∧ Zone.MinArea2 .Z3 = 6500 ∧ Zone.MinArea2 .Z4 = 7500 -theorem Zone.MinArea2.defeq : defeq_spec := by simp +theorem Zone.MinArea2.defeq : defeq_spec := by simp [defeq_spec, Zone.MinArea2] example (x: Zone) : x.MinArea1 + x.MinArea2 = 10000 := by auto [Zone.MinArea1.defeq, Zone.MinArea2.defeq] diff --git a/lake-manifest.json b/lake-manifest.json index 5fb2da6..3cc886e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "bfa9e0827f3011b17d6d849546105ec8c64a265c", + "rev": "652a6727c76391d1fc13faf2e53a31208bf1a937", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-02-18", + "inputRev": "nightly-testing-2024-02-20", "inherited": false, "configFile": "lakefile.lean"}], "name": "auto", diff --git a/lakefile.lean b/lakefile.lean index 217d8b1..6411847 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ package «auto» { } require std from git - "https://github.com/leanprover/std4.git"@"nightly-testing-2024-02-18" + "https://github.com/leanprover/std4.git"@"nightly-testing-2024-02-20" @[default_target] lean_lib «Auto» { diff --git a/lean-toolchain b/lean-toolchain index a605e0d..1638e17 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-02-18 \ No newline at end of file +leanprover/lean4:nightly-2024-02-20 \ No newline at end of file