Stream: new members

Topic: Heterogenous Equality

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'?

Eric Wieser (Dec 29 2020 at 15:20):

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

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