chore: stress test against binder nonsense

Arm/Memory/SeparateAutomation.lean

@@ -92,7 +92,7 @@ namespace SeparateAutomation
 
 structure SimpMemConfig where
   /-- number of times rewrites must be performed. -/
-  rewriteFuel : Nat := 100
+  rewriteFuel : Nat := 1000
 
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
@@ -776,11 +776,16 @@ partial def SimpMemM.improveExpr (e : Expr) (hyps : Array Hypothesis) : SimpMemM
       Lean.Meta.forallTelescope e fun xs b => do
         for x in xs do
           improveExpr x hyps
+          -- we may have a hypothesis like
+          -- ∀ (x : read_mem (read_mem_bytes ...) ... = out).
+          -- we want to simplify the *type* of x.
+          improveExpr (← inferType x) hyps
         improveExpr b hyps
     else if e.isLambda then
       Lean.Meta.lambdaTelescope e fun xs b => do
         for x in xs do
           improveExpr x hyps
+          improveExpr (← inferType x) hyps
         improveExpr b hyps
     else
       -- check if we have expressions.

Proofs/Experiments/MemoryAliasing.lean

@@ -285,15 +285,16 @@ info: 'ExprVisitor.test_quantified_app_1' depends on axioms: [propext, Classical
 #guard_msgs in #print axioms test_quantified_app_1
 
 /--
-Check that we correctly simplify hypotheses as well,
-where the hypotheses are universally quantified variables
+Check that we correctly simplify the *types* of binders as well.
+Here, the bound variable `P` has *type* that involves a memory read.
+We make sure that we simplify these as well.
 -/
 theorem test_quantified_app_2 {val : BitVec (16 * 8)}
     (hlegal : ∀ (addr : Nat), mem_legal' addr 16)
     (f : _ → Nat) :
     f (∀ (P : Memory.read_bytes 16 0 (Memory.write_bytes 16 0 val mem) = irrelevant), Nat) =
     f (∀ (P : val.extractLsBytes 0 16 = irrelevant), Nat) := by
   simp_mem
-  simp
+  rfl
 
 end ExprVisitor