simp under binders

Stream: mathlib4

[James Gallicchio]

A small example:

example : ∀ x y, 0 < x → y < x + y :=
  by simp [Nat.lt_add_of_pos_left]

This does not work, because (I think) simp does not introduce the LHS of implications when it descends into binders. But simp, I think, could do exactly that -- when it descends into the RHS of an arrow, add the LHS to simp's hypothesis context.

Is there a reason why it doesn't do that?

[James Gallicchio]

I'm mainly asking because I am unsure I understand how the Logic.lean simp lemmas are designed. What is the simp-normal form for first-order logical statements, if there is one?

[Mario Carneiro]

(config := {contextual := true})

[James Gallicchio]

Is there a reason that's not the default behavior? Seems useful.

[Floris van Doorn]

For the same reason that simp* or erw are not the default: it is more expensive, and not always what you want.
It might be useful to have a shorter notation for it though.

[James Gallicchio]

Yeah. One of those situations where you probably want the expensive version to be easy to try, since it's pretty much strictly more powerful.

I am trying to prove some Pairwise lemmas for std4#38; first lemma, simp did not do anything, but contextual simp solved it entirely :)

[James Gallicchio]

It also just seems odd to me that something like this isn't solved by plain simp:

example {p : α → Prop} : ∀ {x y}, (p x → ¬p y) → p y → ¬p x :=
  by simp (config := {contextual := true}) [Not]

But perhaps I have too high expectations for simp.

[James Gallicchio]

(it's also odd to me that I have to unpack Not there, but I can see why, since otherwise I assume simp won't enter the final p x -> False binder)

[Mario Carneiro]

it's presumably solved by simp with the relevant comm lemma

[James Gallicchio]

Oh? This is in Std, so that's possible

[Mario Carneiro]

it appears to be literally the forward direction of a std lemma

[James Gallicchio]

It feels odd to me that we rely on simp lemmas to solve FOL problems, instead of having a dedicated solver routine for it. I'm not sure what the tradeoff is there.

[Mario Carneiro]

the tradeoff is that it takes time and people to make a sat solver

[Mario Carneiro]

in std itself FOL problems are mostly done using manual term proofs in Std.Logic, and afterward you can use simp or proof-structural tactics like cases, apply etc to do most FOL stuff

[Mario Carneiro]

it's pretty rare to have a pure FOL problem as a goal

[Mario Carneiro]

it's usually mixed with definitional unfolding or other lemmas and that's where simp does well