fin.induction

Stream: general

[Patrick Massot]

Does anyone know what are the equations for fin.induction_on? I was expecting something like:

import data.fin.basic

variables {n : ℕ}

@[simp] lemma fin.induction_on_zero
  {C : fin (n + 1) → Sort*}
  (h0 : C 0)
  (hs : ∀ i : fin n, C i.cast_succ → C i.succ) :
@fin.induction_on n 0 C h0 hs = h0 :=
rfl


@[simp] lemma fin.induction_on_succ
  {C : fin (n + 1) → Sort*}
  (h0 : C 0)
  (hs : ∀ i : fin n, C i.cast_succ → C i.succ)
  (i : fin n)  :
@fin.induction_on n i.succ C h0 hs  = hs i (@fin.induction_on n i.cast_succ C h0 hs) :=
rfl

But the second one fails.

[Patrick Massot]

Am I confused with my fin.succ, fin.cast_succ etc?

[Patrick Massot]

I find it rather suspicious that docs#fin.induction is defined in tactic mode. This seems to ask for trouble when writing the above lemmas.

[Kyle Miller]

It's the rcases at the beginning I think. If you do cases i it unsticks the rfl.

lemma fin.induction_on_succ
  {C : fin (n + 1) → Sort*}
  (h0 : C 0)
  (hs : ∀ i : fin n, C i.cast_succ → C i.succ)
  (i : fin n) (j : C i.cast_succ) :
@fin.induction_on n i.succ C h0 hs  = hs i (@fin.induction_on n i.cast_succ C h0 hs) :=
begin
  cases i,
  refl,
end

[Patrick Massot]

Nice!

[Patrick Massot]

Arguably we should fix docs#fin.induction anyway

[Eric Wieser]

I suspect it's done in tactic mode as the version generated by the equation compiler doesn't reduce in the kernel

[Kyle Miller]

I had some troubles with using the equation compiler for this (as in it didn't reduce nicely when trying to prove fin.induction_on_succ)

[Kyle Miller]

Here's the tactic proof as a term mode proof:

@[elab_as_eliminator]
def fin.induction'
  {C : fin (n + 1) → Sort*}
  (h0 : C 0)
  (hs : ∀ i : fin n, C i.cast_succ → C i.succ)
  (i : fin (n + 1)) : C i :=
subtype.cases_on i $ λ i hi,
  nat.rec (λ hi, h0)
  (λ i IH hi, hs ⟨i, nat.lt_of_succ_lt_succ hi⟩ (IH (nat.lt_of_succ_lt hi)))
  i hi

[Eric Wieser]

Is there any advantage to that proof over the one we have?

[Kyle Miller]

It's pretty much exactly the same.

[Eric Wieser]

I guess it doesn't have the eq.mpr in it, which is nice

[Kyle Miller]

At the h0? That's along a rfl lemma anyway, so I'm not sure it matters