hint tactic

Stream: mathlib4

[Scott Morrison]

example (h : 1 < 0) : False := by hint
example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint
example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint
example {a b : ℚ} (h : a < b) : ¬ b < a := by hint
example : 37^2 - 35^2 = 72 * 2 := by hint
example : Nat.Prime 37 := by hint

#8363

[Scott Morrison]

This uses @Thomas Murrills's lovely "Try these:" widget from std4#215.

[Scott Morrison]

New meta-game: when new users' tactic questions are not answered by hint, wonder if hint should be powered up.

[Joachim Breitner]

Cool. Next step: as the user writes :=, in the background fire off hint, and present the first closing tactic as auto completion, so that theorem proving becomes a game of “write lemma, :=, TAB, write lemma, :=, TAB…”

[Ruben Van de Velde]

import Mathlib
example : ∀ n > 2, ∀ a b c : ℕ,
    a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n := by
  hint

Should hint be powered up?

[Scott Morrison]

I have an ancient PR #4109 which fires off exact? every time your cursor is at a sorry. People complained about their CPUs melting, so it was sadly never merged.

[Thomas Murrills]

While auto-running tactics might be too expensive, a code action to replace sorries (or complete :='s?) with by hint or exact?% might still save a keystroke or two!

[Thomas Murrills]

(If we get fancier, maybe we could use an option (e.g. set_option autoRunTactics true) to control whether you see Try this: by hint or whether you eagerly auto-run hint given the cursor position?)

[Thomas Murrills]

Ruben Van de Velde said:

import Mathlib
example : ∀ n > 2, ∀ a b c : ℕ,
    a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n := by
  hint

Should hint be powered up?

Try this: email Kevin Buzzard and ask how it's going

[Joachim Breitner]

Auto-running tactics certainly needs careful tuned settings to not melt the CPU and stay interactive, maybe a fast_hint variant. But it's worth it!

The competition (Isabelle) does it already. Furthermore, it even auto-runs tactics on the negation of the lemma, and an amazing tool called nitpick (like Haskell's quick check), which even gives counterexamples!
This saves a lot of time when otherwise you'd start embarking on a proof only to notice later that you make some typo or forgot an hypothesis.

So much to do… :-)

[Scott Morrison]

We have a basic implementation of slim_check in Mathlib.

[Asei Inoue]

(deleted)