5
$\begingroup$

In the lean 4 version of the natural number game at https://adam.math.hhu.de/#/g/leanprover-community/NNG4/ , I can use tactics like apply x at h and induction b with d hd.

In my local copy of lean, which I believe is v4.4.0-rc1, these things cause errors. For example, induction fails when given a with d hd suffix:

theorem lt_implies_le (a b : Nat)
  (h: a < b)
  : a <= b
  := by
    induction b with d hd  -- "unknown tactic"

and apply fails when given an at h suffix:

theorem lt_implies_le (a b : Nat)
  (h: a < b)
  : a <= b
  := by
    induction b
    trivial
    induction a
    simp
    apply Nat.succ_le_succ
    apply Nat.succ_le_succ at h  -- unexpected token 'at'; expected command

What is going on? Why is it behaving differently?

$\endgroup$
5
  • 1
    $\begingroup$ Perhaps you need to import Mathlib? $\endgroup$ Dec 5, 2023 at 1:12
  • $\begingroup$ @FrançoisG.Dorais Why would importing Mathlib change the availability of syntax like an "at" clause on apply? $\endgroup$ Dec 5, 2023 at 1:17
  • 1
    $\begingroup$ Because it's defined in Mathlib. Lean's syntax is extendible. $\endgroup$ Dec 5, 2023 at 1:18
  • $\begingroup$ @FrançoisG.Dorais This does seem to be the problem. Definitely very confusing. Especially because the natural number game doesn't include the import in its example code. $\endgroup$ Dec 5, 2023 at 1:20
  • $\begingroup$ I think NNG automatically includes Mathlib in the background. $\endgroup$ Dec 5, 2023 at 1:22

1 Answer 1

4
$\begingroup$

You need to install Mathlib and then import it with import Mathlib.

Also you need to use induction' instead of induction to get the equivalent behavior to the natural number game.

With Mathlib installed, this example from the game works with an import:

import Mathlib

example
  (x y : ℕ)
  (h1 : x = 37)
  (h2 : x = 37 → y = 42)
  : y = 42 := by
  apply h2 at h1
  exact h1

and it doesn't work without the import:

example
  (x y : ℕ)
  (h1 : x = 37)          -- failed to synthesize instance
  (h2 : x = 37 → y = 42) -- failed to synthesize instance
  : y = 42 := by         -- failed to synthesize instance
  apply h2 at h1         -- unexpected token 'at'
  exact h1
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.