calculating with `Nat.lor`

Stream: Is there code for X?

[Jeremy Avigad]

Can anyone help me with this?

import Mathlib.Data.Nat.Prime.Basic

example (n m : Nat) (h : m < 2^7) : n <<< 7 ||| m = n <<< 7 + m := by
  sorry

I know about Nat.shiftLeft_eq, but I am struggling to do anything with the |||.

[Jeremy Avigad]

Nevermind, leansearch found Nat.mul_add_lt_is_or.

[Kim Morrison]

That is really not named correctly... (lean#7563)

[Kim Morrison]

We really should update #leansearch so that when it is invoked in tactic mode with no argument, it just sends the goal state.

[Kim Morrison]

Any takers to do that? @Siddhartha Gadgil?

[Siddhartha Gadgil]

Sure. I can do this.

But the new command #statesearch does exactly this, querying a server that is designed for accepting the goal state (and written by the same people as #leansearch's server). Should we instead be advising people to use that (I don't know how stable their server is).

[Kim Morrison]

Oh, great, I didn't know.

That suggests that maybe we should try to simplify life and not require people to know what backend they're actually getting, e.g. #search just does something.

[Siddhartha Gadgil]

Agreed. We can keep the present commands, and also have an option to set the backend for #search. In tactic mode we can have the proof-state based backend if #search is given without a parameter.

My only mild concern is triggering #search without arguments while the user has not yet typed the argument. Given the automatic delay before elaboration, this may not be such an issue.

I can go ahead and implement this if the design seem fine.

[Siddhartha Gadgil]

Made a PR with the commands, tests for all cases and README updated.

[Kim Morrison]

Looks great, 'd!