## Stream: new members

### Topic: cases alternative

#### Sarah Mameche (Dec 18 2018 at 21:32):

Hi, using cases on an hypothesis sometimes gives me really huge terms in the resulting hypotheses. It's happened if the hypothesis contains recursive definitions, and I fixed it in one case by marking the definition as irreducible.
However, now I get the same problem for the definition

def Fin : nat → Type
| 0 := empty
| (n+1) := option (Fin n)


as soon as I call cases on something like x: Fin (n+1). In Coq, this goes through, so I guess it has something to do with definitions being compiled to recursors? Is there another way to use cases without unfolding the definition/getting this huge expression? (Marking Fin as irreducible didn't work because I want to match on it in other proofs)

#### Kevin Buzzard (Dec 18 2018 at 22:25):

Definitions made with the equation compiler in Lean can sometimes come out quite unwieldy. Does it make any difference if you just apply the recursor directly?

#### Kevin Buzzard (Dec 18 2018 at 22:26):

def Fin' : nat → Type :=
λ n, nat.rec_on n (empty) (λ n Fn, option Fn)


#### Chris Hughes (Dec 18 2018 at 22:30):

A definition like this one in number_theory/dioph is probably easier to use, and gives a similar induction principle

inductive fin2 : ℕ → Type
| fz {n} : fin2 (succ n)
| fs {n} : fin2 n → fin2 (succ n)


#### Sarah Mameche (Dec 18 2018 at 23:05):

That helped, thanks!

Last updated: May 15 2021 at 23:13 UTC