calculations with eq

Stream: general

[Reid Barton]

Is this provable?

lemma eq_mpr_val {α : Type} {p q : α → Prop} (e : subtype p = subtype q)
  (x : subtype q) : (eq.mpr e x).val = x.val :=
sorry

[Reid Barton]

(subtype here is just an example of a type which has a field whose type doesn't depend on the type indices being changed by e.)

[Reid Barton]

Or if I find myself needing to prove this sort of thing, do I need to back up and make sure that instead of this eq.mpr e x, I have an expression that recurses on a proof of p = q?

[Simon Hudon]

Yeah, I don't see an alternative. eq.mpr is going to be difficult to get rid of. I tried various things with generalize and congr but to no avail

[Chris Hughes]

I think it's probably not provable. I don't see a reason why @subtype.val α p == @subtype.val α q without p = q. I think in lean two types of the same size are indistinguishable, so if p ≠ q, but subtype p = subtype q, there's no contradiction, provided they're the same size, but there's no canonical isomorphism or way of identifying @subtype.val α p with @subtype.val α q. Mario will know.

[Chris Hughes]

I couldn't actually prove a contradiction from assuming subtype p = subtype q, where p ≠ q and your lemma though.

[Mario Carneiro]

These sorts of things are independent in lean. Injectivity of inductive type constructors is either independent or false in every case I'm aware of.