Updated to lean v4.4.0-rc1 but temporarily removed bitvector function…

…ality

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

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

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

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];

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

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
+end Auto

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}"

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"}

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» {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.4.0-rc1