linarith not discharging goals involving Nat and Nat.sub

Stream: new members

[wellhidden]

Hi all

I am a long time Coq user but a rank novice to Lean(4). I am trying to find an equivalent of lia in Lean4, and linarith is supposed to discharge such goals. But I am not able to discharge a simple theorem:

theorem lin: forall a b: Nat, a - (a - b) < b -> a - b = 0 := by
intros a b H;
linarith

(Informally, if a > b, a - (a-b) = b leading to a contradiction of b < b. Else if a < b, then it's already 0)

On a related note, is there a way to search for theorems containing specific type (similar to Ctrl-c Ctrl-a Ctrl-a in proofgeneral?) on the web browser based engine?

[Eric Wieser]

omega can do it

[wellhidden]

Thanks, that did it. Didn't know about the existence of omega in Lean4.

[wellhidden]

If I get stuck in something that even omega cannot discharge, how do I search for the relevant available theorems ? As I mentioned, with Coq, it's pretty easy to search based on the definitions used in the theorem (for example, Search nat Nat.lt.)

[Niels Voss]

There's the API documentation (which is what I use the most), the #find command, the exact?, apply? and rw? tactics, Loogle for pattern matching (similar to #find), Leansearch, Leanexplore and Moogle for LLM-based search, and then the #loogle, #moogle, #leansearch commands

[Niels Voss]

I would recommend learning how to use the API documentation and loogle, as those will probably be what you use the most. Loogle seems the closest to what Coq had based on your description