Zulip Chat Archive

Stream: new members

Topic: fin induction principle


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?

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?

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: Dec 20 2023 at 11:08 UTC