# Zulip Chat Archive

## Stream: new members

### Topic: Inductive relation on inductively defined `Fin` types

#### Rémi Bottinelli (Sep 30 2022 at 13:42):

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 (Oct 01 2022 at 04:03):

I believe there's a typo in the first line of the definition of `sc`

, 2nd argument

#### Matt Diamond (Oct 01 2022 at 04:04):

you wrote `ι τ`

but I think you meant to write `ι x`

#### Matt Diamond (Oct 01 2022 at 04:06):

correcting that typo appears to fix the first error

#### Rémi Bottinelli (Oct 01 2022 at 05:51):

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 (Oct 01 2022 at 05:52):

But this actually means that the matching goes one level deeper, which might be the reason things don't work? By the way, when `#print`

ing either `lt`

or `sc`

, I get pretty ugly terms involving `eq.rec`

, is that to be expected?

Last updated: Dec 20 2023 at 11:08 UTC