How to prove `x ≍ x'` where `x'` was created via `simp at x`

Stream: lean4

[David Richter]

Sometimes simp at ... creates a new hypothesis instead of simplifying the given one. I think this happens when simp applies non-definitionally equalties. However, by simply creating a new hypothesis which is unrelated to the old, it sometimes becomes difficult to prove something. Here is a contrived example:

theorem test (x : Option (if n+1 > n then Bool else String)): IsBool x := by
  simp at x
  rename_i x'
  have : x ≍ x' := by sorry
  sorry

After simp has created an equivalent but different hypothesis, is it possible to prove that these two are still the same? In short, how to prove: x ≍ x', where x' has been created by simp at x.

[Aaron Liu]

I don't think this is possible

[Aaron Liu]

if you look at the context there's nothing that connects x with x'

[Ruben Van de Velde]

I fear the best advice here is "don't get yourself into this situation"

[Eric Wieser]

Can you make that a #mwe?

[David Richter]

Aaron Liu: I don't think this is possible
Aaron Liu: if you look at the context there's nothing that connects x with x'

Yes, after having performed simp at x, there is nothing that connects these two. Maybe there is a variant or configuration option to simp that retains a proof that connects the new and the old hypothesis?

[Kevin Buzzard]

docs#IsBool (404)

[Aaron Liu]

maybe you can revert x first before rewriting with docs#if_pos

[David Richter]

sorry, forgot the IsBool definition

inductive IsBool {α: Type} : Option α → Prop where
  | mk (h: α = Bool) : IsBool o

theorem test (x : Option (if n+1 > n then Bool else String)): IsBool x := by
  simp at x
  rename_i x'
  have : x ≍ x' := by sorry
  sorry

but really, this is not about proving specifically this goal, as it can be solved much easier in another way. to come up with an example where i actually need x=x' i probably need quite a few more lines...

[Kevin Buzzard]

Type equality in lean is in general undecidable, for example if X is any type with two terms which isn't defeq to Bool (for example Fin 2 or Option Unit) then X = Bool is neither provable nor disprovable in Lean's type theory. Are you sure that this is what you want?

[Aaron Liu]

you can also have teq : Foo = Bar := by simp and then have hx : x ≍ x := .rfl and then rewrite the right side of hx using teq

[Ruben Van de Velde]

It's probably worth stepping back and thinking if you can solve your original problem without conditional types

[David Richter]

Thanks, for the thoughts!

Type equality in lean is in general undecidable, for example if X is any type with two terms which isn't defeq to Bool (for example Fin 2 or Option Unit) then X = Bool is neither provable nor disprovable in Lean's type theory. Are you sure that this is what you want?

I'm not trying to prove equality for arbitrary types. I'm specifically interested in retaining a proof that anything produced by simp is still equal to what was given to simp.

Most often, when you apply simp at x to the hypothesis x, the hypothesis x only changes its type. For example given a hypothesis x: Fin (1+2) we can simp it to x: Fin 3. These definitional-equalities can also be performed by using dsimp instead of simp, limiting the applicable equalities to only definitional ones.

But simp can also perform non-definitional equalities, like for example associativity of natural addition, or simplification of if-then-else here. When simp performs non-definitional equalities, it seems it produces a new hypothesis which takes the name x with the simplified type, while graying out the old hypothesis x(and renaming it to x†, which retains its old type). This is a problem, when the old hypothesis was used anywhere else in the goal, as these references continue to use the old x†.

Consider the proof states before and after simp.

inductive IsBool {α: Type} : Option α → Prop where
  | mk (h: α = Bool) : IsBool o

theorem test (x : Option (if n+1 > n then Bool else String)): IsBool x := by
  -- at this point the proof state is:
  --   n : ℕ
  --   x : Option (if n + 1 > n then Bool else String)
  --   ⊢ IsBool x
  simp at x
  -- now the proof state is
  --   n : ℕ
  --   x✝ : Option (if n + 1 > n then Bool else String)   <- the x gets renamed but retains its type
  --   x : Option Bool -- <- a new x appears with the simplified type
  --   ⊢ IsBool x✝ -- <- the problem is that the proof continues to use the old x, and that there is no relationship between the old and the new x

Clearly, simponly uses equalities (whether definitional or not) to simplify the type, so it should be possible to retain that the newly produced hypothesis is the same as the old. But it seems that is not the case...

maybe you can revert x first before rewriting with docs#if_pos

yes, in this case doing revert first, then simp, and then intro, etc. works. i tried that in my attempts, but if the code is sufficiently additionally complex, then simp doesnt apply the rule anymore, and using explicit rewriting leads to motive is not type correct.

i guess i should produce a self-contained example, and return with that, but that will take some more time...

[Aaron Liu]

David Richter said:

maybe you can revert x first before rewriting with docs#if_pos

yes, in this case doing revert first, then simp, and then intro, etc. works. i tried that in my attempts, but if the code is sufficiently additionally complex, then simp apply the rule anymore, and using explicit rewriting leads to motive is not type correct.

I will once again advertise file#Tactic/DepRewrite

[Yaël Dillies]

The module doc of this file doesn't tell you what the syntax of the tactic is

[David Richter]

The file defines only two syntaxes, so I guess your proposing to use rw! instead of rw/simp?
Hm... let's see.

[Aaron Liu]

Yaël Dillies said:

The module doc of this file doesn't tell you what the syntax of the tactic is

oh no, I'll add that to the list of things I have to fix