subtype eq of value eq

Stream: general

[Leonard Wigman]

i'm trying to understand the proof of subtype eq of value eq (at a primitive level using recursors/rewrites).
the kernel terms of the library proofs weren't all that insightful.

when trying it myself, i ran into the following issue:
the idea is to start with eq.refl (subtype.mk a_val a_property) and rewrite the second part of the equality type.
the issue is, trying to rewrite it to eq (subtype.mk a_val a_property) (subtype.mk **b_val** a_property) using a_val = b_val results in a type error. a_property: P a_val, not P b_val. since a_val = b_val these types are the same, but i'm not sure how to tell lean that. in a way, i'd have to rewrite both a_val and a_property to b_val and b_property simultaneously.

this is what i tried:

universes u
variables (T: Sort u) (P: T -> Prop)

theorem subtype.eq_of_value_eq (a b: subtype P): a.val = b.val -> a = b :=
begin
  intro heq,
  cases a,
  cases b,
  have r := eq.refl (subtype.mk a_val a_property),
  have heq': a_val = b_val := heq,
  rw heq' at r,
  sorry
end

[Leonard Wigman]

the general question here is:
if i have a structure with dependent fields (foo: A, bar: B[foo]), and i have two values foo', bar' and proofs that foo = foo', bar = bar', how do i rewrite both in the term { foo, bar }?

[Leonard Wigman]

the issue being that neither can really be replaced individually, due to their dependence at type level.

[Leonard Wigman]

there's probably some trick to do that kind of thing that i'm not aware of.

[Andrew Yang]

You can use subst heq' instead of rw.

[Andrew Yang]

Another option is to congr and then force your way out.
Also, you should not be able to obtain bar = bar' since the types are not definitionally equal.
The best you could have is bar == bar'.

[Leonard Wigman]

huh, that works indeed.
but presumably only because of proof irrelevance.

how would this work if a_property wasn't a Prop and i instead had a proof a_property = b_property?
could i give subst both equality proofs?

[Andrew Yang]

If you had a proof a_property == b_property, then after subst heq' both sides will have the same type, and you can use docs#heq_iff_eq to turn it into an eq that can then be used to rewrite.

[Leonard Wigman]

ok, thanks! :ok:

[Leonard Wigman]

ok, i figured out what's going on:

theorem Subtype.eq_of_value_eq' (v1 v2: T) {P: T -> Prop} (p1: P v1) (p2: P v2)
  : v1 = v2 -> Subtype.mk v1 p1 = Subtype.mk v2 p2
:=
  fun heq =>
    @Eq.rec T v1
      -- this takes `p2` of type `P v2` to avoid the type error.
      (fun v2 _ => forall p2: P v2, Subtype.mk v1 p1 = Subtype.mk v2 p2)
      -- this is expected to yield `{v1, p1} = {v1, p2}`, which is def-eq by proof irrelevance.
      (fun p2 => Eq.refl (Subtype.mk v1 p1))
      v2
      heq
      p2

without proof irrelevance, the motive would look like this:
fun v2 _ => forall p2: P v2, HEq p1 p2 -> Subtype.mk v1 p1 = Subtype.mk v2 p2)

so instead of replacing things simultaneously, it does work sequentially, but you have to "feed the later fields and proofs through the motive" to make sure the types work out.

[Leonard Wigman]

this "feed through" thing essentially rewrites the types of the other fields.
which is the issue i had initially - that the second field's type would cause issues.

[Eric Wieser]

You can try the "without proof irrelevance" version by playing the same game with docs#sigma (the lemma you're proving is docs#sigma.ext)