(h₂ ▸ h₁) ▸ x = h₂ ▸ (h₁ ▸ x)

Stream: Is there code for X?

[Max Nowak 🐉]

I am trying to prove the following, which feels like it probably exists somewhere in std or mathlib already, but I just can't find it, and Loogle doesn't turn up anything either. Without notation, this is Eq (Eq.rec x (Eq.rec h₁ h₂)) (Eq.rec (Eq.rec x h₁) h₂).
This is actually a xy problem, with the x problem being h ▸ h.symm ▸ T = T.

theorem eq_cast_trans {h₁ : A = B} {h₂ : B = C} {x : A}
  : (h₂ ▸ h₁) ▸ x = h₂ ▸ h₁ ▸ x
  := sorry

[Joachim Breitner]

theorem eq_cast_trans {h₁ : A = B} {h₂ : B = C} {x : A}
  : (h₂ ▸ h₁) ▸ x = h₂ ▸ h₁ ▸ x
  := by cases h₁; cases h₂; rfl

but are you asking for the proof, or are you asking why you don’t find something like this in the library?
(I don’t have an answer for the latter; I think I searched for it myself at some point in the past.)

[Max Nowak 🐉]

Oh wow that was quick! I was asking for the proof, but if you have tips for finding theorems like these I'm all ears. So far I'm just trying to guess the theorem name and if that doesn't turn anything up, I am hitting a wall haha.

[Kyle Miller]

Something to watch out for with ▸ is that it's not just notation, it entails running an elaborator that tries rewriting using a few different approaches.

[Max Nowak 🐉]

Yeah I noticed that sometimes it applies Eq.symm and so on.

[Kyle Miller]

Could you xy further? Why do you have a h ▸ h.symm ▸ T term? Could you be better served having a custom cast definition that rewrites a type's indices, for example?

[Max Nowak 🐉]

I had another instance of the same problem as in this thread, just a bit more complicated, and that somehow resulted in this situation. I can try to minimise today's problem if you want? Alternatively, it's one (large) self-contained Lean file.

[Kyle Miller]

It looks like I already made the cast suggestion

[Kyle Miller]

While making a cast means you don't get library lemmas and have to write your own, there aren't so many general lemmas about Eq.rec that you'd be missing out on.

[Max Nowak 🐉]

I hadn't even thought of making a custom cast for this. I might, it is a good suggestion. I will try to finish the proof with what I have thus far, and then try to extract a useful specialised cast.
However, the whole reason I need two casts in the first place is (as far as I understand it, i.e. not very well) because of a definition which doesn't reduce even though I think it should, and thus I have to use def f | args => (proof of reduction rule) ▸ (rhs of f). This cast then spreads and messes up the approach from the other thread. I could come back or open another thread once I have a better grasp of what's going on, because maybe I just got some basics very very wrong. There is also a failure to generate injective theorems for an inductive type that is at the heart of this, that might be related.

[Max Nowak 🐉]

...meanwhile the agda code that I am porting to Lean just shrugs this off as completely trivial.

[Kyle Miller]

Is there a recursive definition here? Sometimes all you need to do is cases on enough arguments to "unlock" reduction, and do rfl on each case.

[Kyle Miller]

Max Nowak 🐉 said:

There is also a failure to generate injective theorems for an inductive type that is at the heart of this, that might be related.

That possible sounds like a big problem. Is that something you think is a Lean bug?

[Max Nowak 🐉]

Kyle Miller said:

That possible sounds like a big problem. Is that something you think is a Lean bug?

Yeah I am pretty sure. This is the third time I encounter the same or similar bug with generating injective theorems. I should open an issue about it some day.

[Max Nowak 🐉]

Kyle Miller said:

Is there a recursive definition here? Sometimes all you need to do is cases on enough arguments to "unlock" reduction, and do rfl on each case.

Yes and no. I have the following, but if I get rid of the recursive branch, then the h ▸ VarD v in the non-recursive case is still necessary, and removing the cast breaks. This is also not a theorem, but an actual function.

def TmₛD
| .var v => h ▸  VarₛD v
| .app t u => sorry -- this was the recursive branch

[Max Nowak 🐉]

This is simplifying a lot. I think I'll try to get it working in this ugly way first.

[Max Nowak 🐉]

You have helped greatly btw, I appreciate it a lot!

[Max Nowak 🐉]

So far: Inductive type Tmₛ fails to generate injective theorems. Recursive definition TmₛA has (imo) broken reduction behaviour, need to use casts with equation theorems. TmₛD completely fails to generate equation theorems; it uses TmₛA in its type. My next step would be to prove the equation theorems for TmₛD, but I feel like this is a spiral that will never end and cause problems in the future.

[Eric Rodriguez]

can you post your code? this seems like a major bug

[Max Nowak 🐉]

Here is the code, it is a rather large but self-contained file. If you search for ! you will find the relevant trouble points (four of them). I also left three relevant errors which should help navigate a little.
I copy-pasted the original Agda bits into comments for reference.

[Max Nowak 🐉]

I can try to minimise it if this is too much.

[Max Nowak 🐉]

Nevermind, I managed to make it generate equation theorems after all. It's still a bit of a paper cut that a definition typechecks just fine but then fails to derive equation theorems. And the other issues remain.