9
$\begingroup$

When writing this answer, I had a hard time finding the lemma I needed to prove 2 ≤ 3. In Agda, when I have a goal, I can press refine and Agda will either insert a constructor or tell me she doesn't know which constructor to use, so I can pick one from the list. In Lean4 if I place a metavariable in the goal, she simply say "don't know how to synthesize this" (I'm paraphrasing, but it's something like that). Even without these error messages, I can click in the IDE to jump to the definition of the type, and I can read the definition to know the available constructors.

In Lean4 the situation is totally different. I looked up the definition of < and it's a macro or a notation definition, which I cannot jump to further definition (I tried clicking but it doesn't do anything). I looked around the code and found the definition -- it's LT, a class. So, to work with it, I need to know which instance I'm using in order to find the available constructors. However, I didn't find an easy way to lookup the instance used in my incomplete proof.

I guess this is probably not the preferred way of programming in Lean4. I guess Lean4 wants me to work with mathematics abstractly, but I am unfamiliar with the Lean4 library and the Lean4 best practices. I can work pretty well with Cubical Agda library without prior knowledge to it by using the IDE extensively, and I wish to learn how can I do similar things in Lean4.

Please tell me anything I can do, even a bunch of keyboard shortcuts will help me a lot.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
8
$\begingroup$

Here are a few ways of getting this goal without really knowing anything about what the definition of LT is etc. In rough order of low-tech to high-tech, we have:

  • a tactic that tries to apply constructors of inductive types directly
  • using the simplifier (which is one of the main Lean workhorses)
  • a mathlib4 tactic that will search all available declarations for something that can be applied to your goal
import Mathlib.Tactic.LibrarySearch -- only for theorem c

theorem a : 2 ≤ 3 :=
by
  constructor
  constructor

theorem b : 2 ≤ 3 :=
by
  simp

theorem c : 2 ≤ 3 :=
by
  library_search -- exact Nat.le_succ 2
Improve this answer
$\endgroup$
5
  • $\begingroup$ Exactly what I was looking for -- except that I can't use mathlib with Lean4 yet $\endgroup$
    – ice1000 ♦
    Commented Feb 21, 2022 at 23:58
  • 2
    $\begingroup$ @ice1000 Alex' answer is using github.com/leanprover-community/mathlib4 $\endgroup$
    – Sebastian Ullrich
    Commented Feb 22, 2022 at 8:25
  • 1
    $\begingroup$ I was thinking of asking when it would be a good idea to switch from Lean 3 to Lean 4. I know there is ongoing work transporting mathlib...I wonder if it would be best to wait for that to finish? $\endgroup$
    – Jon Bannon
    Commented Feb 22, 2022 at 11:25
  • 2
    $\begingroup$ @JonBannon for sure you could ask this as another question, it is a fair bit subjective of course, but maybe thats ok. My personal take is that in order to do deep mathematics its better to wait for the first working version of the mathlib port to be done (not necessarily complete and final, just something that works). This is in order to avoid frustration reinventing the mathematical wheel. But it is already possible to do very interesting things in Lean 4 and well worth using if you don't need a large maths library. $\endgroup$
    – Alex J Best
    Commented Feb 22, 2022 at 14:42
  • $\begingroup$ I think I agree. So I've been sticking with Lean 3 thus far. $\endgroup$
    – Jon Bannon
    Commented Feb 23, 2022 at 16:18

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