simp_all behavior

Stream: lean4

[Xavier Généreux]

Hi everyone,

I use simp_all a lot, usually via aesop. Today, I encountered the following behavior which I am having a hard time understanding.

See here.

Could someone help me understand what is happening here?
Thanks!

[Riccardo Brasca]

simp_all only [P] tranforms h into True → True, that is sospicius...

[Riccardo Brasca]

There must a stupid thing that confuses us (us = humans)

[Riccardo Brasca]

Maybe what it does is that it realizes p 0 is true, so also P 1, and now it has lost the implication

[Jakub Nowak]

example (h : p 0 → P 1) (h0 : P 0) : p 4 := by
  have h1 : P 1 := by sorry
  simp_all only [P]

Like this it also removes h1 : P 1.

[Riccardo Brasca]

It looks like a bug

[Jakub Nowak]

I looks like simp_all used used h and h0 to realize p 1 is True. The bug is in the fact, that it completely got rid of p 1 assumption.

[Xavier Généreux]

Yes I don't understand why P 1 gets transformed into True.

[Riccardo Brasca]

Well, this happens often with simp calls. I guess it also transforms x = x into True, or something similar.

[Jakub Nowak]

But p 1 is not universally true like x = x. That's not the same. Here h h0 is a proof of p 1. The bug is that simp_all simplified h to True using h h0, without adding h h0 to the context.

[Aaron Liu]

It used the assumption to simplify itself

[Riccardo Brasca]

Yes, I totally agree it's a bug

[Kim Morrison]

Could you please write this up as an issue?

[Xavier Généreux]

See 11291