Matching on Fin

Stream: new members

[Dax Fohl]

I've been banging my head against the wall, but can't get anything like this to work. It works fine if I change k to Nat. But I can't get it to work for Fin.

def bounded_decrement (k: Fin 20) : Nat :=
match k with
| Nat.zero => 0
| Nat.succ n => n

[Dax Fohl]

I'm ultimately looking for def bounded_decrement (n: Nat) (k: Fin n) : Fin (n - 1)

[Yury G. Kudryashov]

docs#Fin.predAbove ?

[Niels Voss]

For the first half of your question, maybe something like this?

def bounded_decrement (k: Fin 20) : Nat :=
match k with
| ⟨Nat.zero, hk⟩ => 0
| ⟨Nat.succ n, hk⟩ => n

hk will be a proof that the natural number is less than 20. What you have to be put in the match clause must be the same as how Fin is defined. A term k of type Fin n is essentially a Nat and a proof that k < n, so to match on it you have to have a variable that stores that proof.

[Niels Voss]

(In case it isn't clear, ⟨Nat.zero, hk⟩ is in this context shorthand for Fin.mk (Nat.zero) hk and ⟨Nat.succ n, hk⟩ is shorthand for Fin.mk (Nat.succ n) hk.)

[Dax Fohl]

Thanks! yeah I stumbled across that notation when looking at the def for Fin.succ.

[Niels Voss]

You could also check out Fin2, which is like Fin but defined recursively. I don't know when you'd use it, but I found it interesting