Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC