From b2db9280ab57481983a70ddabaf856fb4c132228 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 19 Dec 2023 11:46:59 -0500 Subject: [PATCH] Updated to lean v4.4.0-rc1 but temporarily removed bitvector functionality --- Auto/Embedding/LamChecker.lean | 15 ++++++++++++--- Auto/Embedding/LamConv.lean | 4 ++-- Auto/Embedding/LamSystem.lean | 1 - Auto/Lib/BinTree.lean | 2 +- Auto/Lib/NatExtra.lean | 4 ++-- Auto/Lib/Pos.lean | 6 +++--- Auto/Translation/LamReif.lean | 2 ++ lake-manifest.json | 24 +++++++++++++----------- lakefile.lean | 5 ++--- lean-toolchain | 2 +- 10 files changed, 38 insertions(+), 27 deletions(-) diff --git a/Auto/Embedding/LamChecker.lean b/Auto/Embedding/LamChecker.lean index 616fae2..9d62fa0 100644 --- a/Auto/Embedding/LamChecker.lean +++ b/Auto/Embedding/LamChecker.lean @@ -3,7 +3,8 @@ import Auto.Embedding.LamConv import Auto.Embedding.LamInference import Auto.Embedding.LamLCtx import Auto.Embedding.LamPrep -import Auto.Embedding.LamBitVec +-- Temporarily removing this input until I can get this file to build on Lean v4.4.0-rc1 +-- import Auto.Embedding.BitVec import Auto.Embedding.LamInductive import Auto.Lib.BinTree open Lean @@ -601,8 +602,10 @@ inductive PrepConvStep where | validOfPropEq : PrepConvStep /-- (a = b) ↔ (a ∨ b) ∧ (¬ a ∨ ¬ b) -/ | validOfPropNe : PrepConvStep + /- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1 /-- Basic BitVec simplification operations -/ | validOfPushBVCast : PrepConvStep + -/ deriving Inhabited, Hashable, BEq, Lean.ToExpr inductive WFStep where @@ -703,7 +706,9 @@ def PrepConvStep.toString : PrepConvStep → String | .validOfNotImpEquivAndNot => s!"validOfNotImpEquivAndNot" | .validOfPropEq => s!"validOfPropEq" | .validOfPropNe => s!"validOfPropNe" +/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1 | .validOfPushBVCast => s!"validOfPushBVCast" +-/ def WFStep.toString : WFStep → String | .wfOfCheck lctx t => s!"wfOfCheck {lctx} {t}" @@ -1145,7 +1150,9 @@ def InferenceStep.evalValidOfBVarLowers (r : RTable) (lctx : List LamSort) (pns | .validOfNotImpEquivAndNot => LamTerm.not_imp_equiv_and_not? | .validOfPropEq => LamTerm.propeq? | .validOfPropNe => LamTerm.propne? +/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1 | .validOfPushBVCast => fun t => LamTerm.pushBVCast .none t +-/ @[reducible] def WFStep.eval (lvt lit : Nat → LamSort) (r : RTable) : (cs : WFStep) → EvalResult | .wfOfCheck lctx t => @@ -2110,9 +2117,11 @@ theorem PrepConvStep.eval_correct (lval : LamValuation) : | .validOfPropNe => And.intro LamGenConv.propne? (LamTerm.evarBounded_of_evarEquiv @LamTerm.maxEVarSucc_propne?) +/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1 | .validOfPushBVCast => And.intro LamGenConv.pushBVCast (LamTerm.evarBounded_of_evarEquiv LamTerm.evarEquiv_pushBVCast) +-/ theorem WFStep.eval_correct (r : RTable) (cv : CVal.{u} r.lamEVarTy) (inv : r.inv cv) : @@ -2320,12 +2329,12 @@ theorem Checker.getValidExport_indirectReduceAux LamThmValid cpv.toLamValuationEraseEtom lctx t := by apply RTable.getValidExport_correct _ heq have lvtEq : (fun n => (lvt.get? n).getD (.base .prop)) = cpv.toLamVarTy := by - cases cpv; dsimp [CPVal.toLamVarTy]; apply funext; intro n + cases cpv; unfold CPVal.toLamVarTy; apply funext; intro n rw [← Option.getD_map (f:=@Sigma.fst LamSort _)]; dsimp apply congrFun; apply congrArg; rw [hlvt, BinTree.get?_mapOpt] apply Eq.symm; apply Option.map_eq_bind have litEq : (fun n => (lit.get? n).getD (.base .prop)) = cpv.toLamILTy := by - cases cpv; dsimp [CPVal.toLamILTy]; apply funext; intro n + cases cpv; unfold CPVal.toLamILTy; apply funext; intro n rw [← Option.getD_map (f:=@Sigma.fst LamSort _)]; dsimp apply congrFun; apply congrArg; rw [hlit, BinTree.get?_mapOpt] apply Eq.symm; apply Option.map_eq_bind diff --git a/Auto/Embedding/LamConv.lean b/Auto/Embedding/LamConv.lean index ffbb3d1..c065a3f 100644 --- a/Auto/Embedding/LamConv.lean +++ b/Auto/Embedding/LamConv.lean @@ -1607,7 +1607,7 @@ def LamTerm.mpAll? (rw : LamTerm) (t : LamTerm) : Option LamTerm := | _ => .none theorem LamTerm.evarBounded_mpAll? : evarBounded (LamTerm.mpAll? rw) rw.maxEVarSucc := by - dsimp [LamTerm.mpAll?] + unfold LamTerm.mpAll? cases rw <;> try dsimp <;> try apply evarBounded_none case app s fn rhs => cases fn <;> try dsimp <;> try apply evarBounded_none @@ -1621,7 +1621,7 @@ theorem LamTerm.evarBounded_mpAll? : evarBounded (LamTerm.mpAll? rw) rw.maxEVarS theorem LamGenConv.mpAll? (hvalid : LamThmValid lval [] rw) : LamGenConv lval (LamTerm.mpAll? rw) := by - dsimp [LamTerm.mpAll?] + unfold LamTerm.mpAll? cases rw <;> try dsimp <;> try apply LamGenConv.none case app s fn rhs => cases fn <;> try dsimp <;> try apply LamGenConv.none diff --git a/Auto/Embedding/LamSystem.lean b/Auto/Embedding/LamSystem.lean index 69c678c..189b642 100644 --- a/Auto/Embedding/LamSystem.lean +++ b/Auto/Embedding/LamSystem.lean @@ -1636,7 +1636,6 @@ theorem LamGenModify.rwGenAtIfSign {modify} (H : LamGenModify lval modify weaken induction l generalizing occ weaken? weaken?' case zero => cases List.length_eq_zero.mp (Nat.le_zero.mp hl) - dsimp [LamTerm.rwGenAtIfSign, LamTerm.isSign] match h : weaken? == weaken?' with | true => cases (Bool.beq_to_eq _ _).mp h; exact H | false => dsimp [LamGenModify]; intro t₁ t₂ h; cases h diff --git a/Auto/Lib/BinTree.lean b/Auto/Lib/BinTree.lean index 2ffeac3..2130e53 100644 --- a/Auto/Lib/BinTree.lean +++ b/Auto/Lib/BinTree.lean @@ -432,7 +432,7 @@ theorem allp'_node (p : α → Prop) : have h' := h (2 * n + 5) rw [get?'_succSucc] at h' have eq₁ : (2 * n + 5) % 2 = 1 := by - rw [Nat.add_mod]; simp + rw [Nat.add_mod]; simp; rfl have eq₂ : (2 * n + 5) / 2 = n + 2 := by rw [Nat.add_comm _ 5]; rw [Nat.add_mul_div_left]; diff --git a/Auto/Lib/NatExtra.lean b/Auto/Lib/NatExtra.lean index c73f52f..7efd0ea 100644 --- a/Auto/Lib/NatExtra.lean +++ b/Auto/Lib/NatExtra.lean @@ -109,8 +109,8 @@ theorem Nat.max_add {a b c : Nat} : max a b + c = max (a + c) (b + c) := by simp [h, naleb] theorem Nat.max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by - rw [← Nat.lt_eq]; dsimp [Nat.lt]; rw [← Nat.add_one]; rw [Nat.max_add] - rw [Nat.max_le]; apply Iff.intro id id + rw [← Nat.lt_eq, Nat.lt]; dsimp only [Nat.le_eq]; rw [← Nat.add_one]; + rw [Nat.max_add]; rw [Nat.max_le]; apply Iff.intro id id theorem Nat.max_zero_left {a : Nat} : max 0 a = a := by rw [Nat.max_def]; simp diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean index 991513a..3e9c303 100644 --- a/Auto/Lib/Pos.lean +++ b/Auto/Lib/Pos.lean @@ -30,7 +30,7 @@ theorem toNat'_not_zero (p : Pos) : toNat' p ≠ 0 := by case inl H' => revert H'; exact IH case inr H' => cases H' case xI p' _ => - simp [toNat'] + simp [toNat'] private theorem ofNat'WFAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by intro H; apply Nat.div_lt_self @@ -96,7 +96,7 @@ theorem ofNat'WF.doubleSucc_xI (n : Nat) : rw [ofNat'WF.succSucc]; have heq : (2 * n' + 3 + 2) % 2 = 1 := by rw [Nat.add_mod_right]; rw [Nat.add_mod] - rw [Nat.mul_mod]; simp + rw [Nat.mul_mod]; simp; rfl rw [heq]; simp have heq' : Nat.succ ((2 * n' + 3) / 2) = n' + 2 := by apply congrArg; rw [Nat.add_comm]; @@ -297,4 +297,4 @@ theorem succ_inj (p q : Pos) : succ p = succ q → p = q := fun H => end Pos -end Auto \ No newline at end of file +end Auto diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean index d2a43c5..fe1d0f5 100644 --- a/Auto/Translation/LamReif.lean +++ b/Auto/Translation/LamReif.lean @@ -1050,7 +1050,9 @@ section CheckerUtils else return (vs, minds)) let vs ← vs.mapM validOfBetaReduce + /- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1 let vs ← vs.mapM (fun re => validOfPrepConv .validOfPushBVCast re []) + -/ let vs ← vs.mapM validOfRevertAll for v in vs do trace[auto.lamReif.prep.printResult] "{v}" diff --git a/lake-manifest.json b/lake-manifest.json index 88bb395..9410f55 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,12 +1,14 @@ -{"version": 6, - "packagesDir": "lake-packages", +{"version": 7, + "packagesDir": ".lake/packages", "packages": - [{"git": - {"url": "https://github.com/leanprover/std4.git", - "subDir?": null, - "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": false}}], - "name": "auto"} + [{"url": "https://github.com/leanprover/std4.git", + "type": "git", + "subDir": null, + "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "auto", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 2dea24a..d4c2188 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,12 +2,11 @@ import Lake open Lake DSL package «auto» { - precompileModules := true - preferReleaseBuild := true + -- add any package configuration options here } require std from git - "https://github.com/leanprover/std4.git"@"main" + "https://github.com/leanprover/std4.git"@"9e37a01f8590f81ace095b56710db694b5bf8ca0" @[default_target] lean_lib «Auto» { diff --git a/lean-toolchain b/lean-toolchain index 734efdd..91ccf6a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.3.0-rc1 \ No newline at end of file +leanprover/lean4:v4.4.0-rc1