Zulip Chat Archive

Stream: new members

Topic: Proving injectivity over all terms


view this post on Zulip Yakov Pechersky (Aug 21 2020 at 15:47):

I have a state that is

n : ,
x y : fin (n + 1),
h : x.succ_above = y.succ_above,
key :  (a : fin n), ite (a.val < x.val) a.cast_succ a.succ = ite (a.val < y.val) a.cast_succ a.succ
 x = y

as a result of

import data.fin

lemma succ_above_inj_at_pivot {n : } {x y : fin (n + 1)} :
  x.succ_above = y.succ_above  x = y :=
begin
  refine iff.intro _ (λ h, by rw h),
  intro h,
  have key :  a, x.succ_above a = y.succ_above a := λ a, congr_fun h a,
  unfold fin.succ_above at key,
end

view this post on Zulip Yakov Pechersky (Aug 21 2020 at 15:48):

Is there a way to provide an arbitrary a : fin n to key, so that I could split_ifs on it?

view this post on Zulip Yakov Pechersky (Aug 21 2020 at 15:53):

I guess I can have a hypothesis with an existential that encodes a contradiction, then choose on that.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 17:32):

key is just a function, you can feed it anything you like

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 17:33):

Can't you just solve this goal using h though?


Last updated: May 08 2021 at 04:14 UTC