Inductive relation on inductively defined `Fin` types

Stream: new members

[Rémi Bottinelli]

Hey, in the following, I define Fin types as in the HoTT book, and the obvious order on those types by pattern matching.
This works well, and I can prove properties of that order (transitivity and so on).
I tried doing the same for a different kind of order (sc in the MWE) and the same strategy of pattern matching for proofs doesn't work.
I would venture it's the pattern matching reaching its limit, but maybe I'm doing something else wrong. Any idea?

import tactic

def Fin' : ℕ → Sort*
| 0       := empty
| (n + 1) := (Fin' n) ⊕ unit

@[pattern] def ι {n : ℕ} : Fin' n → Fin' (n+1) := sum.inl
@[pattern] def τ {n : ℕ} : Fin' (n+1) := sum.inr unit.star

def lt : Π {n}, Fin' n → Fin' n → Prop
| (n+1) (ι x) (ι y) := lt x y
| (n+1) (ι x) (τ)   := true
| (n+1) (τ)    _    := false
| (0)    _     _    := false  -- don't need it

/- The `successor` relation -/
def sc : Π {n}, Fin' n → Fin' n → Prop
| (n+1) (ι τ) (τ)   := true
| (n+1) (ι x) (ι y) := sc x y
| (n+1)  _     _    := false
| (0)    _     _    := false -- don't need it

infix ` < ` := lt
infix ` <ₛ `:50 := sc

lemma lt.antirefl : Π {n : ℕ} (x : Fin' n), ¬ (x < x)
| (n+1) (ι x) := @lt.antirefl n x
| (n+1) (τ)   := λ lt, lt

lemma lt.trans : Π {n : ℕ} {x y z : Fin' n}, x < y → y < z → x < z
| (n+1) (ι x) (ι y) (ι z) s t := @lt.trans n x y z s t
| (n+1) (ι x) (ι y) (τ)   _ _ := trivial
| (n+1) (ι x) (τ)    _    _ t := t.elim
| (n+1) (τ)    _     _    s _ := s.elim

lemma sc.lt : Π {n : ℕ} {x y : Fin' n}, x <ₛ y → x < y
| (n+1) (ι τ) (τ)   _  := trivial
| (n+1) (ι x) (ι y) h  := by {apply @sc.lt n x y, exact h,} --@sc.lt n x y h -- Error here
| (n+1)  _     _    h  := by {exfalso, exact h,}                                                      -- Error here

[Matt Diamond]

I believe there's a typo in the first line of the definition of sc, 2nd argument

[Matt Diamond]

you wrote ι τ but I think you meant to write ι x

[Matt Diamond]

correcting that typo appears to fix the first error

[Rémi Bottinelli]

I don't think it's a typo: I see \iota : Fin' n -> Fin' (n+1) as the initial segment: then the top element of Fin' n has as successor the top element of Fin' (n+1).

[Rémi Bottinelli]

But this actually means that the matching goes one level deeper, which might be the reason things don't work? By the way, when #printing either lt or sc, I get pretty ugly terms involving eq.rec, is that to be expected?