From ff85acedb91537b383b744fcf4639a3a663df90f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 14 May 2025 03:50:12 +0800 Subject: [PATCH] chore: move a `grind` test (#8325) This PR moves a previously failing `grind` test from `tests/lean/grind/` to `tests/lean/run/`. --- .../grind_ite_unused_match.lean} | 32 ++----------------- 1 file changed, 3 insertions(+), 29 deletions(-) rename tests/lean/{grind/grind_ite_funinduction.lean => run/grind_ite_unused_match.lean} (82%) diff --git a/tests/lean/grind/grind_ite_funinduction.lean b/tests/lean/run/grind_ite_unused_match.lean similarity index 82% rename from tests/lean/grind/grind_ite_funinduction.lean rename to tests/lean/run/grind_ite_unused_match.lean index 22af219a8f..fcb255682b 100644 --- a/tests/lean/grind/grind_ite_funinduction.lean +++ b/tests/lean/run/grind_ite_unused_match.lean @@ -1,20 +1,7 @@ import Std.Data.HashMap.Lemmas -/-! -# If normalization - -Rustan Leino, Stephan Merz, and Natarajan Shankar have recently been discussing challenge problems -to compare proof assistants. -(See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rustan's.20challenge) - -Their first suggestion was "if-normalization". - -Here we state the problem in the Lean, -and then construct a clean solution where all verification work is done by `grind`. - -(This solution builds upon an earlier solution by Chris Hughes, which had less automation -but made use of the powerful termination checker.) --/ +-- This is a variant of the "if normalization" example, acting as a regression test for a now-fixed problem in grind. +-- It is not a solution to the "if normalization" challenge. /-- An if-expression is either boolean literal, a numbered variable, or an if-then-else expression where each subexpression is an if-expression. -/ @@ -114,18 +101,6 @@ def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized -- `grind` is currently experimental, but for now we can suppress the warnings about this. set_option grind.warning false --- We first set up some convenient macros for dealing with subtypes using `grind`. - -/-- Construct a term of a subtype, using `grind` to discharge the condition. -/ -macro "g⟨" a:term "⟩" : term => `(⟨$a, by grind (gen := 8) (splits := 9)⟩) -/-- -Replace a term of a subtype with a term of a different subtype, using the same data, -and using `grind` to discharge the new condition (with access to the old condition). --/ -macro "c⟨" a:term "⟩" : term => `(have aux := $a; ⟨aux.1, by grind⟩) - - - namespace IfExpr attribute [grind] List.mem_cons List.not_mem_nil List.mem_append @@ -183,8 +158,7 @@ theorem normalize_correct (assign : Std.HashMap Nat Bool) (e : IfExpr) : ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by fun_induction normalize rotate_left - · -- Note this error disappears if we remove the unused `h` from the match above. - -- Fails with + · -- This used to fail unless we removed the unused `h` from the match above, with the error message: -- [issue] type error constructing proof for IfExpr.normalize.match_1.eq_1 -- when assigning metavariable ?h_1 with -- fun h => var v