From 8a373cbebe8fee28c4bd041acbe44a6a86ee6f45 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 7 Apr 2025 14:05:20 +1000 Subject: [PATCH] chore: add failing grind tests about decide (#7845) --- tests/lean/grind/decide.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/lean/grind/decide.lean diff --git a/tests/lean/grind/decide.lean b/tests/lean/grind/decide.lean new file mode 100644 index 0000000000..304592a7ef --- /dev/null +++ b/tests/lean/grind/decide.lean @@ -0,0 +1,21 @@ +--- + +example {P Q : Prop} [Decidable P] [Decidable Q] : (decide P || decide Q) = decide (P ∨ Q) := by grind + +--- + +@[grind] theorem eq_head_or_mem_tail_of_mem_cons {a b : α} {l : List α} : + a ∈ b :: l → a = b ∨ a ∈ l := List.mem_cons.mp + +attribute [grind] List.mem_cons_self, List.mem_cons_of_mem + +-- This succeeds: +example [DecidableEq α] {l : List α} : + (y ∈ a :: l) = (y = a) ∨ y ∈ l := by + grind + + +-- but inserting some `decide`s fails: +example [BEq α] [LawfulBEq α] {l : List α} : + decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by + grind