From 8a8b9e4556ac75e6c418c59e7485225abffaca5e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Apr 2025 23:02:08 +1000 Subject: [PATCH] chore: further cleanup of the if-normalization example (#8176) --- tests/lean/run/grind_ite.lean | 20 +++----------------- 1 file changed, 3 insertions(+), 17 deletions(-) diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean index 06a26f97a1..d6f3056d78 100644 --- a/tests/lean/run/grind_ite.lean +++ b/tests/lean/run/grind_ite.lean @@ -115,26 +115,12 @@ set_option grind.warning false namespace IfExpr -attribute [grind] List.mem_cons List.not_mem_nil List.mem_append - Option.getD_some Option.getD_none - -attribute [local grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars +-- We tell `grind` it can unfold our definitions above. +attribute [grind] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars eval -- I'd prefer to use `TreeMap` here, but its `getElem?_insert` lemma is not useful. attribute [grind] Std.HashMap.getElem?_insert -/-! -Lemmas for `eval`. --/ -@[grind] theorem eval_lit : (lit b).eval f = b := rfl -@[grind] theorem eval_var : (var i).eval f = f i := rfl -@[grind] theorem eval_ite_lit : - (ite (.lit b) t e).eval f = bif b then t.eval f else e.eval f := rfl -@[grind] theorem eval_ite_var : - (ite (.var i) t e).eval f = bif f i then t.eval f else e.eval f := rfl -@[grind] theorem eval_ite_ite {a b c d e : IfExpr} : - (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by grind [eval] - /-- Custom size function for if-expressions, used for proving termination. It is designed so that if we decrease the size of the "if" condition by one, @@ -149,7 +135,7 @@ we are allowed to increase the size of the branches by one, and still be smaller def normalize (assign : Std.HashMap Nat Bool) : IfExpr → IfExpr | lit b => lit b | var v => - match assign[v]? with -- Note unused `h`: if we remove this things work again. + match assign[v]? with | none => var v | some b => lit b | ite (lit true) t _ => normalize assign t