How to resolve `HEq u (e ▸ u)`?

Stream: general

[Andrej Bauer]

I must not be the first one who used congr and was left with HEq u (e ▸ u). How do I get rid of this? I am happy to assume UIP or whatever it takes. (Currently I am not using mathlib, if that matters, and would prefer not to.)

[Mario Carneiro]

cases e; rfl seems likely to work

[Mario Carneiro]

there is probably a lemma you can apply as well

[Mario Carneiro]

eqRec_heq.symm, give or take

[Andrej Bauer]

Here's an example:

theorem chicken {α β}
  (P : α → Type)
  (f : ∀ (x : α), P x → β)
  {x y : α}
  (e : x = y) {u : P x} :
  f x u = f y (e ▸ u)
  := by congr ; sorry --left with HEq u (e ▸ u)

[Andrej Bauer]

Indeed, cases e ; rfl (instead of congr) worked. Thanks.

[Notification Bot]

Andrej Bauer has marked this topic as resolved.

[Andrej Bauer]

More generally, is there a way to say "Just get rid of all the ▸, even if you assume UIP"?

[Notification Bot]

Andrej Bauer has marked this topic as unresolved.

[Andrej Bauer]

The problem is that in many other cases I have goals like step p (⋯ ▸ ps) = ⋯ ▸ step p ps and I really don't want to look what's inside ⋯ . Any advice on how to deal with these is most welcome.

[Mario Carneiro]

I believe this is what we affectionately refer to as DTT hell

[Andrej Bauer]

Yes, I know, I helped advertise it under the slogan "homotopy type theory" a while ago.

[Mario Carneiro]

unfortunately there are a lot of non-theorems in this space so it's not that easy to just ignore all the casts

[Andrej Bauer]

But since Lean 4 has choice, excluded middle, and nuclear bombs, perhaps the hell is more enjoyable.

[Andrej Bauer]

In that case, how do I look inside ⋯ ?

[Mario Carneiro]

as long as enough things are variables you can pretty much just cases e1; cases e2; rfl your way to success, but when the equalities are between nontrivial things you first have to generalize various things, and I don't know a general way of doing this correctly

[Andrej Bauer]

Or even better, is there UIP somewhere in the Lean standard library? I think that would solve my problems.

[Andrej Bauer]

(Of course they are not variables.)

[Mario Carneiro]

you can mouse over the ... to see it, or use set_option pp.proofs true

[Mario Carneiro]

UIP is assumed by everything, and it's a definitional equality. That's not the problem

[Mario Carneiro]

I suppose in this example you can kind of just rewrite the cast away because HEq is transitive and casts are HEq to their main argument

[Mario Carneiro]

but rewrite doesn't understand HEq

[Mario Carneiro]

One tool which may help you here is generalize_proofs, which will pull all the ... proofs into variables so you can induct on them or revert them or something

[Mario Carneiro]

but it's in mathlib, you'll have to copy it into your project if you don't want to depend on mathlib

[Andrej Bauer]

I think I'll just have to put on my HoTT hat and deal with the matter. Thanks.

[Sina Hazratpour 𓃵]

Mario Carneiro said:

One tool which may help you here is generalize_proofs, which will pull all the ... proofs into variables so you can induct on them or revert them or something

Interesting! Do you have a mwe or a link to somewhere on Mathlib for a use case of generalize_proofs?

[Mario Carneiro]

basic example:

import Mathlib.Tactic.GeneralizeProofs

example {n} (v : BitVec (n + 5)) (a : BitVec 5) (b : BitVec n) : a ++ b = v.cast (by omega) := by
  -- ⊢ a ++ b = BitVec.cast ⋯ v
  generalize_proofs h
  -- h : n + 5 = 5 + n
  -- ⊢ a ++ b = BitVec.cast h v

[Mario Carneiro]

the next step can vary depending on what you want to do, but what generalize_proofs saves you is the trouble of having to write down whatever nasty proof term was generated by omega in this example in order to use it with generalize