Zulip Chat Archive

Stream: new members

Topic: Heterogenous Equality


view this post on Zulip Marcus Rossel (Dec 29 2020 at 15:15):

I'm struggling with heterogenous equality. Say we have the following:

import data.vector

def n0s (n : ) : vector  n := vector.repeat 0 n
def p {z : } (v : vector  z) : Prop := sorry
def q (a : ) (b : p (n0s a)) :  := sorry

theorem same (x x' : ) (h : p (n0s x)) (h' : p (n0s x')) :
  x = x'  (q x h) = (q x' h') :=
  sorry

How would I prove in same that h = h'?

view this post on Zulip Eric Wieser (Dec 29 2020 at 15:20):

At a guess, is the proof for same intro hx, subst hx?

view this post on Zulip Marcus Rossel (Dec 29 2020 at 15:21):

Eric Wieser said:

At a guess, is the proof for same intro hx, subst hx?

:face_palm: yup, that worked.


Last updated: May 14 2021 at 02:15 UTC