cases alternative

Stream: new members

[Sarah Mameche]

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]

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]

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

[Chris Hughes]

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]

That helped, thanks!