0ba40b798b
This PR re-enables star-indexed lemmas as a fallback for `exact?` and
`apply?`.
Star-indexed lemmas (those with overly-general discrimination tree keys
like `[*]`)
were previously dropped entirely for performance reasons. This caused
useful lemmas
like `Empty.elim`, `And.left`, `not_not.mp`, `Sum.elim`, and
`Function.mtr` to be
unfindable by library search.
The implementation adds a two-pass search strategy:
1. First, search using concrete discrimination keys (the current
behavior)
2. If no results are found, fall back to trying star-indexed lemmas
The star-indexed lemmas are extracted during tree initialization and
cached in an
environment extension, avoiding repeated computation.
Users can disable the fallback with `-star`:
```lean
example {α : Sort u} (h : Empty) : α := by apply? -star -- error: no lemmas found
example {α : Sort u} (h : Empty) : α := by apply? -- finds Empty.elim
```
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
463 lines
13 KiB
Text
463 lines
13 KiB
Text
-- Enable this option for tracing:
|
||
-- set_option trace.Tactic.librarySearch true
|
||
-- And this option to trace all candidate lemmas before application.
|
||
-- set_option trace.Tactic.librarySearch.lemmas true
|
||
|
||
-- Many of the tests here are quite volatile,
|
||
-- and when changes are made to `solve_by_elim` or `exact?`,
|
||
-- or the library itself, the printed messages change.
|
||
-- Hence many of the tests here use `#guard_msgs (drop info)`,
|
||
-- and do not actually verify the particular output, just that `exact?` succeeds.
|
||
-- We keep the most recent output as a comment
|
||
-- (not a doc-comment: so `#guard_msgs` doesn't check it)
|
||
-- for reference.
|
||
-- If you find further tests failing please:
|
||
-- 1. update the comment using the code action on `#guard_msgs`
|
||
-- 2. (optional) add `(drop info)` after `#guard_msgs` and change the doc-comment to a comment
|
||
|
||
set_option linter.unusedVariables false
|
||
|
||
noncomputable section
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.lt_add_one x
|
||
-/
|
||
#guard_msgs in
|
||
example (x : Nat) : x ≠ x.succ := Nat.ne_of_lt (by apply?)
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.zero_lt_succ 1
|
||
-/
|
||
#guard_msgs in
|
||
example : 0 ≠ 1 + 1 := Nat.ne_of_lt (by apply?)
|
||
|
||
example : 0 ≠ 1 + 1 := Nat.ne_of_lt (by exact Fin.pos')
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_comm x y
|
||
-/
|
||
#guard_msgs in
|
||
example (x y : Nat) : x + y = y + x := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact fun a => Nat.add_le_add_right a k
|
||
-/
|
||
#guard_msgs in
|
||
example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.mul_dvd_mul_left a w
|
||
-/
|
||
#guard_msgs in
|
||
example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] Nat.lt_add_one x
|
||
-/
|
||
#guard_msgs in
|
||
example : x < x + 1 := exact?%
|
||
|
||
/-- error: `exact?%` could not close the goal. Try `by apply?` to see partial suggestions. -/
|
||
#guard_msgs in
|
||
example {α : Sort u} (x y : α) : Eq x y := exact?%
|
||
|
||
/-- error: `exact?%` could not close the goal. Try `by apply?` to see partial suggestions. -/
|
||
#guard_msgs in
|
||
example (x y : Nat) : x ≤ y := exact?%
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact p
|
||
-/
|
||
#guard_msgs in
|
||
example (P : Prop) (p : P) : P := by show_term solve_by_elim
|
||
/--
|
||
info: Try this:
|
||
[apply] exact False.elim (np p)
|
||
-/
|
||
#guard_msgs in
|
||
example (P : Prop) (p : P) (np : ¬P) : false := by show_term solve_by_elim
|
||
/--
|
||
info: Try this:
|
||
[apply] exact h x rfl
|
||
-/
|
||
#guard_msgs in
|
||
example (X : Type) (P : Prop) (x : X) (h : ∀ x : X, x = x → P) : P := by show_term solve_by_elim
|
||
|
||
-- Could be any number of results (`fun x => x`, `id`, etc)
|
||
#guard_msgs (drop info) in
|
||
example (α : Prop) : α → α := by show_term solve_by_elim
|
||
|
||
-- These examples work via star-indexed fallback.
|
||
#guard_msgs (drop info) in
|
||
example (p : Prop) : (¬¬p) → p := by apply?
|
||
#guard_msgs (drop info) in
|
||
example (a b : Prop) (h : a ∧ b) : a := by apply?
|
||
#guard_msgs (drop info) in
|
||
example (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_comm a b
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) : a + b = b + a :=
|
||
by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.mul_sub_left_distrib n m k
|
||
-/
|
||
#guard_msgs in
|
||
example (n m k : Nat) : n * (m - k) = n * m - n * k :=
|
||
by apply?
|
||
|
||
attribute [symm] Eq.symm
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Eq.symm (Nat.mul_sub_left_distrib n m k)
|
||
-/
|
||
#guard_msgs in
|
||
example (n m k : Nat) : n * m - n * k = n * (m - k) := by
|
||
apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact eq_comm
|
||
-/
|
||
#guard_msgs in
|
||
example {α : Type} (x y : α) : x = y ↔ y = x := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_pos_right a hb
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) (_ha : 0 < a) (hb : 0 < b) : 0 < a + b := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_pos_right a hb
|
||
-/
|
||
#guard_msgs in
|
||
-- Verify that if maxHeartbeats is 0 we don't stop immediately.
|
||
set_option maxHeartbeats 0 in
|
||
example (a b : Nat) (_ha : 0 < a) (hb : 0 < b) : 0 < a + b := by apply?
|
||
|
||
section synonym
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_pos_right a hb
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) (_ha : a > 0) (hb : 0 < b) : 0 < a + b := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.le_of_dvd w h
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) (h : a ∣ b) (w : b > 0) : a ≤ b :=
|
||
by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.le_of_dvd w h
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) (h : a ∣ b) (w : b > 0) : b ≥ a := by apply?
|
||
|
||
-- TODO: A lemma with head symbol `¬` can be used to prove `¬ p` or `⊥`
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.not_lt_zero a
|
||
-/
|
||
#guard_msgs in
|
||
example (a : Nat) : ¬ (a < 0) := by apply?
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.not_succ_le_zero a h
|
||
-/
|
||
#guard_msgs in
|
||
example (a : Nat) (h : a < 0) : False := by apply?
|
||
|
||
-- An inductive type hides the constructor's arguments enough
|
||
-- so that `apply?` doesn't accidentally close the goal.
|
||
inductive P : Nat → Prop
|
||
| gt_in_head {n : Nat} : n < 0 → P n
|
||
|
||
-- This lemma with `>` as its head symbol should also be found for goals with head symbol `<`.
|
||
theorem lemma_with_gt_in_head (a : Nat) (h : P a) : 0 > a := by cases h; assumption
|
||
|
||
-- This lemma with `false` as its head symbols should also be found for goals with head symbol `¬`.
|
||
theorem lemma_with_false_in_head (a b : Nat) (_h1 : a < b) (h2 : P a) : False := by
|
||
apply Nat.not_lt_zero; cases h2; assumption
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact lemma_with_gt_in_head a h
|
||
-/
|
||
#guard_msgs in
|
||
example (a : Nat) (h : P a) : 0 > a := by apply?
|
||
/--
|
||
info: Try this:
|
||
[apply] exact lemma_with_gt_in_head a h
|
||
-/
|
||
#guard_msgs in
|
||
example (a : Nat) (h : P a) : a < 0 := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact lemma_with_false_in_head a b h1 h2
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) (h1 : a < b) (h2 : P a) : False := by apply?
|
||
|
||
-- TODO this no longer works:
|
||
-- example (a b : Nat) (h1 : a < b) : ¬ (P a) := by apply? -- says `exact lemma_with_false_in_head a b h1`
|
||
|
||
end synonym
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact fun P => iff_not_self
|
||
-/
|
||
#guard_msgs in
|
||
example : ∀ P : Prop, ¬(P ↔ ¬P) := by apply?
|
||
|
||
-- Copy of P for testing purposes.
|
||
inductive Q : Nat → Prop
|
||
| gt_in_head {n : Nat} : n < 0 → Q n
|
||
|
||
theorem p_iff_q (i : Nat) : P i ↔ Q i :=
|
||
Iff.intro (fun ⟨i⟩ => Q.gt_in_head i) (fun ⟨i⟩ => P.gt_in_head i)
|
||
|
||
-- We even find `iff` results:
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact (p_iff_q a).mp h
|
||
-/
|
||
#guard_msgs in
|
||
example {a : Nat} (h : P a) : Q a := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact (p_iff_q a).mpr h
|
||
-/
|
||
#guard_msgs in
|
||
example {a : Nat} (h : Q a) : P a := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact (Nat.dvd_add_iff_left h₁).mpr h₂
|
||
-/
|
||
#guard_msgs in
|
||
example {a b c : Nat} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b := by apply?
|
||
|
||
-- These examples work via star-indexed fallback.
|
||
#guard_msgs (drop info) in
|
||
example {α : Sort u} (h : Empty) : α := by apply?
|
||
#guard_msgs (drop info) in
|
||
example (f : A → C) (g : B → C) : (A ⊕ B) → C := by apply?
|
||
|
||
opaque f : Nat → Nat
|
||
axiom F (a b : Nat) : f a ≤ f b ↔ a ≤ b
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact (F a b).mpr h
|
||
-/
|
||
#guard_msgs in
|
||
example (a b : Nat) (h : a ≤ b) : f a ≤ f b := by apply?
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact L.flatten
|
||
-/
|
||
#guard_msgs in
|
||
example (L : List (List Nat)) : List Nat := by apply? using L
|
||
|
||
-- Could be any number of results
|
||
#guard_msgs (drop info) in
|
||
example (P _Q : List Nat) (h : Nat) : List Nat := by apply? using h, P
|
||
|
||
-- Could be any number of results
|
||
#guard_msgs (drop info) in
|
||
example (l : List α) (f : α → β ⊕ γ) : List β × List γ := by
|
||
apply? using f -- partitionMap f l
|
||
|
||
-- Could be any number of results (`Nat.mul n m`, `Nat.add n m`, etc)
|
||
#guard_msgs (drop info) in
|
||
example (n m : Nat) : Nat := by apply? using n, m
|
||
|
||
#guard_msgs (drop info) in
|
||
example (P Q : List Nat) (_h : Nat) : List Nat := by exact? using P, Q
|
||
|
||
-- Check that we don't use sorryAx:
|
||
-- (see https://github.com/leanprover-community/mathlib4/issues/226)
|
||
theorem Bool_eq_iff {A B : Bool} : (A = B) = (A ↔ B) :=
|
||
by (cases A <;> cases B <;> simp)
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Bool_eq_iff
|
||
-/
|
||
#guard_msgs in
|
||
theorem Bool_eq_iff2 {A B : Bool} : (A = B) = (A ↔ B) := by
|
||
apply? -- exact Bool_eq_iff
|
||
|
||
-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20regression/near/354025788
|
||
-- Disabled for Std
|
||
--/-- info: Try this: exact surjective_quot_mk r -/
|
||
--#guard_msgs in
|
||
--example {r : α → α → Prop} : Function.Surjective (Quot.mk r) := by exact?
|
||
|
||
-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/library_search.20failing.20to.20apply.20symm
|
||
-- Disabled for Std
|
||
-- /-- info: Try this: exact Iff.symm Nat.prime_iff -/
|
||
--#guard_msgs in
|
||
--example (n : Nat) : Prime n ↔ Nat.Prime n := by
|
||
-- exact?
|
||
|
||
-- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exact.3F.20recent.20regression.3F/near/387691588
|
||
-- Disabled for Std
|
||
--lemma ex' (x : Nat) (_h₁ : x = 0) (h : 2 * 2 ∣ x) : 2 ∣ x := by
|
||
-- exact? says exact dvd_of_mul_left_dvd h
|
||
|
||
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/apply.3F.20failure/near/402534407
|
||
-- Disabled for Std
|
||
--example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by
|
||
-- exact? says exact mt h h'
|
||
|
||
-- Removed until we come up with a way of handling nonspecific lemmas
|
||
-- that does not pollute the output or cause too much slow-down.
|
||
-- -- Example from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Exact.3F.20fails.20on.20le_antisymm/near/388993167
|
||
-- set_option linter.unreachableTactic false in
|
||
-- example {x y : ℝ} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
|
||
-- -- This example non-deterministically picks between `le_antisymm hxy hyx` and `ge_antisymm hyx hxy`.
|
||
-- first
|
||
-- | exact? says exact le_antisymm hxy hyx
|
||
-- | exact? says exact ge_antisymm hyx hxy
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] refine Int.mul_ne_zero ?_ h
|
||
-- Remaining subgoals:
|
||
-- ⊢ 2 ≠ 0
|
||
---
|
||
warning: declaration uses 'sorry'
|
||
-/
|
||
#guard_msgs in
|
||
example {x : Int} (h : x ≠ 0) : 2 * x ≠ 0 := by
|
||
apply? using h
|
||
|
||
-- Check that adding `with_reducible` prevents expensive kernel reductions.
|
||
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60exact.3F.60.20failure.3A.20.22maximum.20recursion.20depth.20has.20been.20reached.22/near/417649319
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_comm n m
|
||
-/
|
||
#guard_msgs in
|
||
example (_h : List.range 10000 = List.range 10000) (n m : Nat) : n + m = m + n := by
|
||
with_reducible exact?
|
||
|
||
-- Now finds star-indexed lemmas (e.g., noConfusion) as partial proofs
|
||
#guard_msgs (drop info) in
|
||
example {α : Sort u} (x y : α) : Eq x y := by apply?
|
||
|
||
-- If this lemma is added later to the library, please update this `#guard_msgs`.
|
||
-- The point of this test is to ensure that `Lean.Grind.not_eq_prop` is not reported to users.
|
||
/-- error: `exact?` could not close the goal. Try `apply?` to see partial suggestions. -/
|
||
#guard_msgs in
|
||
example (p q : Prop) : (¬ p = q) = (p = ¬ q) := by exact?
|
||
|
||
-- Verify that there is a `sorry` warning when `apply?` closes the goal.
|
||
#guard_msgs (drop info) in
|
||
example : False := by apply?
|
||
|
||
-- Test the `-star` and `+star` flags for controlling star-indexed lemma fallback.
|
||
-- `Empty.elim` is a star-indexed lemma (polymorphic result type), so `-star` prevents finding it.
|
||
/-- error: apply? didn't find any relevant lemmas -/
|
||
#guard_msgs in
|
||
example {α : Sort u} (h : Empty) : α := by apply? -star
|
||
|
||
-- With `+star`, we find `Empty.elim` via star-indexed lemma fallback.
|
||
#guard_msgs (drop info) in
|
||
example {α : Sort u} (h : Empty) : α := by apply? +star
|
||
|
||
-- Verify that `-star` doesn't break normal (non-star-indexed) lemma search.
|
||
section MinusStar
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.add_comm x y
|
||
-/
|
||
#guard_msgs in
|
||
example (x y : Nat) : x + y = y + x := by apply? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact fun a => Nat.add_le_add_right a k
|
||
-/
|
||
#guard_msgs in
|
||
example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by apply? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.mul_dvd_mul_left a w
|
||
-/
|
||
#guard_msgs in
|
||
example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Nat.lt_add_one x
|
||
-/
|
||
#guard_msgs in
|
||
example : x < x + 1 := by exact? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact eq_comm
|
||
-/
|
||
#guard_msgs in
|
||
example {α : Type} (x y : α) : x = y ↔ y = x := by apply? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact (p_iff_q a).mp h
|
||
-/
|
||
#guard_msgs in
|
||
example {a : Nat} (h : P a) : Q a := by apply? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact (Nat.dvd_add_iff_left h₁).mpr h₂
|
||
-/
|
||
#guard_msgs in
|
||
example {a b c : Nat} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b := by apply? -star
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact L.flatten
|
||
-/
|
||
#guard_msgs in
|
||
example (L : List (List Nat)) : List Nat := by apply? -star using L
|
||
|
||
/--
|
||
info: Try this:
|
||
[apply] exact Bool_eq_iff
|
||
-/
|
||
#guard_msgs in
|
||
example {A B : Bool} : (A = B) = (A ↔ B) := by apply? -star
|
||
|
||
end MinusStar
|