fin has no recursor

Stream: general

[Kenny Lau]

fin doesn’t have the morally correct recursor. we should prove it maybe.

[Mario Carneiro]

There are two obvious approaches: using fz and fs like in fin2, or by peeling off the right end instead, with raise_fin and last or whatever you want to call them

[Mario Carneiro]

there should be more consistent naming here...

[Mario Carneiro]

@[elab_as_eliminator] def fin.succ_rec
  {C : ∀ n, fin n → Sort*}
  (H0 : ∀ n, C (succ n) 0)
  (Hs : ∀ n i, C n i → C (succ n) i.succ) : ∀ {n : ℕ} (i : fin n), C n i
| 0 i := i.elim0
| (succ n) ⟨0, _⟩ := H0 _
| (succ n) ⟨succ i, h⟩ := Hs _ _ (fin.succ_rec ⟨i, lt_of_succ_lt_succ h⟩)

@[elab_as_eliminator] def fin.succ_rec_on {n : ℕ} (i : fin n)
  {C : ∀ n, fin n → Sort*}
  (H0 : ∀ n, C (succ n) 0)
  (Hs : ∀ n i, C n i → C (succ n) i.succ) : C n i :=
i.succ_rec H0 Hs