Zulip Chat Archive

Stream: new members

Topic: fin induction principle


view this post on Zulip Yakov Pechersky (Oct 08 2020 at 16:22):

I have a helper induction principle I like to use:

@[elab_as_eliminator] protected lemma fin.induction_on {n : } (i : fin (n + 1))
  {C : fin (n + 1)  Sort*}
  (h0 : C 0)
  (hs :  i : fin n, C i.cast_succ  C i.succ) : C i :=
begin
  obtain i, hi := i,
  induction i with i IH,
  { rwa [fin.mk_zero] },
  { have : fin.succ i, nat.lt_of_succ_lt_succ hi = i.succ, hi := rfl,
    rw this,
    apply hs,
    apply IH }
end

Should that just be expressed as some version of fin.succ_rec_on?

view this post on Zulip Yakov Pechersky (Oct 08 2020 at 17:31):

Related, why does the cases tactic on fin n unfold the via the subtype defn as opposed to using fin.cases?

view this post on Zulip Kevin Buzzard (Oct 08 2020 at 22:29):

The reason cases does what it does is because it's some primitive tactic in core which is used to take apart inductive types according to their definitions, I'm not sure it can be modified to do what you want.


Last updated: May 10 2021 at 17:39 UTC