From 804658b2401ffd7b66ace3200bb51661b74f9cc6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 26 May 2025 09:00:55 +1000 Subject: [PATCH] chore: update syntax in grind_ite example --- tests/lean/run/grind_ite.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean index da9dfc8573e6..a47a6ec57363 100644 --- a/tests/lean/run/grind_ite.lean +++ b/tests/lean/run/grind_ite.lean @@ -66,7 +66,7 @@ def vars : IfExpr → List Nat /-- A helper function to specify that two lists are disjoint. -/ -@[grind] def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool +def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool | [], _ => true | x::xs, ys => x ∉ ys && xs.disjoint ys @@ -150,13 +150,13 @@ def normalize (assign : Std.HashMap Nat Bool) : IfExpr → IfExpr termination_by e => e.normSize -- We tell `grind` to unfold our definitions above. -attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval +attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval List.disjoint theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) : (normalize assign e).normalized ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → ¬ v ∈ assign := by - fun_induction normalize <;> grind (gen := 7) + fun_induction normalize with grind (gen := 7) -- We can also prove other variations, where we spell "`v` is not in `assign`" -- different ways, and `grind` doesn't mind. @@ -165,13 +165,13 @@ example (assign : Std.HashMap Nat Bool) (e : IfExpr) : (normalize assign e).normalized ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign.contains v = false := by - fun_induction normalize <;> grind (gen := 7) + fun_induction normalize with grind (gen := 7) example (assign : Std.HashMap Nat Bool) (e : IfExpr) : (normalize assign e).normalized ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by - fun_induction normalize <;> grind (gen := 8) + fun_induction normalize with grind (gen := 8) /-- We recall the statement of the if-normalization problem. @@ -207,18 +207,18 @@ theorem normalize'_spec (assign : Std.TreeMap Nat Bool) (e : IfExpr) : (normalize' assign e).normalized ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → ¬ v ∈ assign := by - fun_induction normalize' <;> grind (gen := 7) + fun_induction normalize' with grind (gen := 7) example (assign : Std.TreeMap Nat Bool) (e : IfExpr) : (normalize' assign e).normalized ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign.contains v = false := by - fun_induction normalize' <;> grind (gen := 7) + fun_induction normalize' with grind (gen := 7) example (assign : Std.TreeMap Nat Bool) (e : IfExpr) : (normalize' assign e).normalized ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w)) ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign[v]? = none := by - fun_induction normalize' <;> grind (gen := 8) + fun_induction normalize' with grind (gen := 8) end IfExpr