Pass hypotheses to omega?

Stream: lean4

[Michael Stoll]

Would it be possible to have omega [h, ...] as a shortcut for have := h; ...; omega?

I frequently need to provide additional facts so that omega can finish a proof, like in the following simple example (where in the concrete case, P = Nat.Prime).

def P (n : Nat) : Prop := sorry

theorem P.gt_one {n} (h : P n) : 1 < n := sorry

example {n : Nat} (h : P n) : 0 < n - 1 := by
  have := h.gt_one -- without this, `omega` does not work
  omega -- `omega [h.gt_one]` gives an error

I would much prefer the compact omega [h.gt_one] here.

[Kyle Miller]

I get the draw of having terser syntax, but it does go against the idea that by having lots of smaller tactics, we can combine them to do what we want.

1. Why make omega more complicated? What does omega [e] do that have := e; omega cannot? It appears the only savings is 7 characters.

2. Maybe there's something about have that's lacking. Do we want some sort of have [...] tactic that introduces expressions into the local context?

An issue I've run into with have before is that it wants to know the full type (you know, those "cannot synthesize placeholder" errors). If there were a convenient way to add facts to the local context despite this (like maybe those placeholders get universally quantified to make local theorems) that would be really nice.

I think this is the only possible value proposition to adding it to omega, that it could be tolerant to placeholders, like simp and rw. (In fact, this is why I added bracket syntax to the subsingleton tactic.) However, if we had a generic such mechanism, then all tactics would benefit.

[Julian Berman]

Is it really just to be terser? To me the draw is more about encapsulation, and that these kinds of things get added to the context strictly to get a tactic to make progress, but then they're noise in the local context afterwards, and when reading the proof it's not immediately clear why some random extra proof is there because it's just being used in a "hidden" way by a tactic which may not even be on the next line sometimes. Isn't it a somewhat general thing that often one wants to run a tactic with some extra stuff in its purview but while making it quite clear that the extra stuff is being added strictly for use with this tactic?

E.g. (brainstorming uninformedly) isn't it [...] that seems a bit like it'd be nice to generalize so that it means "locally give this tactic some more stuff to work with while it works", and then [foo, bar] -> omega and [foo, bar] -> simp and other cases where there's something "transient" added just for a tactic to make more progress than it would automatically make end up looking like each other?

[Kyle Miller]

Regarding "after", omega is a finishing tactic, so there's no cluttered local context to worry about there.

I like the idea of a combinator like you're suggesting. Maybe with [e1, e2] => tac adds e1 and e2 to the local context, runs tac, and then clears them?

[Julian Berman]

Yes I ignored the finishing tactic bit :) I assume the argument doesn't strictly rely on that fact so I made believe it wasn't one because I couldn't remember my own examples where I was annoyed by this where it wasn't a finishing tactic. (I guess a have that itself wanted to use omega where I put the temporary stuff in the surrounding proof or something).

[Kyle Miller]

If there were a way to add a local hypothesis that's marked as "tactics, please use this!" that would be neat. Then you could write with [e1, e2] => simp rather than with [e1, e2] => simp [*]

[Kyle Miller]

Separately, it would also be nice if there were a way to get have to be OK with placeholders... Like, downgrading the error to a warning, turn the placeholders into new goals, and let us move on and later fill in what's missing.

[Floris van Doorn]

Kyle Miller said:

Separately, it would also be nice if there were a way to get have to be OK with placeholders... Like, downgrading the error to a warning, turn the placeholders into new goals, and let us move on and later fill in what's missing.

I believe have' is doing this

[Kim Morrison]

omega will be redundant in a few months, and grind, which will subsume it, already has this functionality.

[Michael Stoll]

Will grind be similarly (oe even more) efficient on goals that omega solves?

[Kim Morrison]

We expect so. It will implement the algorithm from "Cutting to the chase" https://leodemoura.github.io/files/cutsat-jar2013.pdf. In fact, not only should it be similarly performant, it will give counterexamples, actually be a complete algorithm (omega was only ever a partial implementation; the shadows part is not there), and allow for improvements like generating diverse models, which enables guessing relevant new identities.

[Kim Morrison]

... plus tightly integrated into powerful congruence closure+ematching automation, all designed with Lean's type theory and typeclass system in mind.