feat: use simp manually

I'm still doing it wrong. I want to use "simp at *, instead of doing simp [*]"
leanprover · Sep 24, 2024 · db361ab · db361ab
1 parent 6945443
commit db361ab
Show file tree

Hide file tree

Showing 4 changed files with 56 additions and 57 deletions.
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
@@ -406,23 +406,23 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : TacticM FVarId  := do
     let goal ← getMainGoal
     let hdefTy ← inferType hdefVal
 
-    /- Simp to gain some more juice out of the defn.. -/
-    let mut simpTheorems : Array SimpTheorems := #[]
-    for a in #[`minimal_theory, `bitvec_rules] do
-      let some ext ← (getSimpExtension? a)
-        | throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
-      simpTheorems := simpTheorems.push (← ext.getTheorems)
-
-    -- unfold `state_value.
-    simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
-    let simpCtx : Simp.Context := {
-      simpTheorems,
-      config := { decide := true, failIfUnchanged := false },
-      congrTheorems := (← Meta.getSimpCongrTheorems)
-    }
-    let (simpResult, _stats) ← simp hdefTy simpCtx (simprocs := #[])
-    let hdefVal ← simpResult.mkCast hdefVal
-    let hdefTy ← inferType hdefVal
+    -- /- Simp to gain some more juice out of the defn.. -/
+    -- let mut simpTheorems : Array SimpTheorems := #[]
+    -- for a in #[`minimal_theory, `bitvec_rules] do
+    --   let some ext ← (getSimpExtension? a)
+    --     | throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
+    --   simpTheorems := simpTheorems.push (← ext.getTheorems)
+
+    -- -- unfold `state_value.
+    -- simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
+    -- let simpCtx : Simp.Context := {
+    --   simpTheorems,
+    --   config := { decide := true, failIfUnchanged := false },
+    --   congrTheorems := (← Meta.getSimpCongrTheorems)
+    -- }
+    -- let (simpResult, _stats) ← simp hdefTy simpCtx (simprocs := #[])
+    -- let hdefVal ← simpResult.mkCast hdefVal
+    -- let hdefTy ← inferType hdefVal
 
     let goal ← goal.assert name hdefTy hdefVal
     let (fvar, goal) ← goal.intro1P
@@ -437,42 +437,34 @@ attribute [bv_toNat] BitVec.le_def
 -- simpTargetStar
 
 
-
 /-- SimpMemM's omega invoker -/
 def omega : TacticM Unit := do
-  -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
-  -- @bollu: TODO: understand what precisely we are recovering from.
   let g ← getMainGoal
-
-  -- TODO: use lnsymSimpContext to get minimal_theory.
   let (simpCtx, simprocs) ← LNSymSimpContext
-      (simp_attrs := #[`minimal_theory, `bitvec_rules, `bv_toNat])
-      (simprocs := #[``reduce_mod_omega])
-
-  let (g?, _stats) ← simpAll g simpCtx simprocs
-  let g ← match g? with
-    | some g' =>
-      trace[simp_mem] "omega preprocessed goal to '{g'}'."
-      pure g'
-    | none  =>
-      trace[simp_mem] "omega preprocessor *closed* goal."
-      return ()
-
-  -- preprocess: make tactic a by_contra.
-  let g ← match ← g.falseOrByContra with
-    | .none => do
-      trace[simp_mem] "by_contra *closed* goal."
-      return ()
-    | .some g' =>
-      trace[simp_mem] "by_contra changed goal to '{g'}'."
-      pure g'
-
-  -- Step 2: prove goal with omega.
-  replaceMainGoal [g]
-  g.withContext do
-    -- withoutRecover do
-      (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
-      -- evalTactic (← `(tactic| bv_omega))
+      (config := {})
+      (simp_attrs := #[`bv_toNat]) (useDefaultSimprocs := false) (simprocs := #[])
+  let (result, stats) ← simpTargetStar g simpCtx simprocs
+  trace[simp_mem] "simp stats: {stats.usedTheorems.toArray.map Origin.key}"
+  if let .closed := result then
+    trace[simp_mem] "omega preprocessor *closed* goal."
+    replaceMainGoal []
+    return ()
+  else
+    let g :=
+      match result with
+      | .modified g' => g'
+      | .noChange | .closed => g
+    -- Step 2: prove goal with omega.
+    let g ←
+      match ← g.falseOrByContra with
+      | none =>
+        trace[simp_mem] "omega converting goal to false/contra *closed* goal."
+        return ()
+      | some g' =>
+        pure g'
+    trace[simp_mem] "omega goal: {g}"
+    replaceMainGoal [g]
+    g.withContext (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
 
 section Hypotheses
 

diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
@@ -10,9 +10,9 @@ import Arm.Memory.MemoryProofs
 import Arm.BitVec
 import Arm.Memory.SeparateAutomation
 
--- set_option trace.simp_mem true
--- set_option trace.simp_mem.info true
--- set_option trace.Tactic.addressNormalization true
+set_option trace.simp_mem true
+set_option trace.simp_mem.info true
+set_option trace.Tactic.addressNormalization true
 
 namespace MemLegal
 /-- Show reflexivity of legality. -/
@@ -127,15 +127,15 @@ theorem separate_6 {n : Nat} (hn : n ≠ 0)
     (l : mem_separate' a 100 b m)
     (l : mem_separate' (a+100) 100 b m)  :
     mem_separate' a 200 b m := by
-  simp_mem /- Need better address normalization. -/
+  simp_mem
   trace_state
 
 /-- error: ❌️ simp_mem failed to make any progress. -/
 #guard_msgs in theorem separate_8 {n : Nat} (hn : n ≠ 0) (hm : m ≠ 0)
     (l : mem_separate' a n b m)
     (l : mem_separate' (a+n) n b m)  :
     mem_separate' a (2*n) b m := by
-  simp_mem /- Need better address normalization. -/
+  simp_mem
   trace_state
 
 /--

diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean
@@ -71,6 +71,8 @@ def popcount32_program : Program :=
 
 #genStepEqTheorems popcount32_program
 
+set_option trace.simp_mem true
+set_option trace.simp_mem.info true
 theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
   (h_s0_pc : read_pc s0 = 0x4005b4#64)
   (h_s0_program : s0.program = popcount32_program)

diff --git a/Tactics/Simp.lean b/Tactics/Simp.lean
@@ -52,12 +52,16 @@ def LNSymSimpContext
   (exprs : Array Expr := #[])
   -- Simprocs to add to the default set.
   (simprocs : Array Name := #[])
+  (useDefaultSimprocs : Bool := True)
   -- argument to `DiscrTree.mkPath`
   (noIndexAtArgs : Bool := true)
   : MetaM (Simp.Context ×  Array Simp.Simprocs) := do
   let mut ext_simpTheorems := #[]
   let default_simprocs ← Simp.getSimprocs
-  let mut all_simprocs := (#[default_simprocs] : Simp.SimprocsArray)
+  let mut all_simprocs : Simp.SimprocsArray :=
+    if useDefaultSimprocs then
+      #[default_simprocs]
+    else #[]
 
   for a in simp_attrs do
     let some ext ← (getSimpExtension? a) |
@@ -67,7 +71,8 @@ def LNSymSimpContext
     if let some ext ← (Simp.getSimprocExtension? a) then
       let s ← ext.getSimprocs
       all_simprocs := all_simprocs.push s
-  let mut const_simpTheorems := ({} : SimpTheorems)
+
+  let mut const_simpTheorems : SimpTheorems := {}
   for d in decls_to_unfold do
     const_simpTheorems ← const_simpTheorems.addDeclToUnfold d
   for t in thms do
@@ -86,7 +91,7 @@ def LNSymSimpContext
     const_simpTheorems := newThms.foldl addSimpTheoremEntry const_simpTheorems
 
   let all_simpTheorems := (#[const_simpTheorems] ++ ext_simpTheorems)
-  let (ctx : Simp.Context) := { config := config,
+  let ctx : Simp.Context := { config := config,
                                 simpTheorems := all_simpTheorems,
                                 congrTheorems := (← Meta.getSimpCongrTheorems) }
   for s in simprocs do