Zulip Chat Archive

Stream: general

Topic: calculations with eq


Reid Barton (Jun 22 2018 at 17:31):

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 (Jun 22 2018 at 17:32):

(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 (Jun 22 2018 at 17:34):

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 (Jun 22 2018 at 17:44):

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 (Jun 22 2018 at 21:00):

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 (Jun 22 2018 at 21:03):

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

Mario Carneiro (Jun 23 2018 at 02:46):

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.


Last updated: Dec 20 2023 at 11:08 UTC