Zulip Chat Archive

Stream: new members

Topic: cases alternative


view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 18 2018 at 22:26):

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

view this post on Zulip 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)

view this post on Zulip Sarah Mameche (Dec 18 2018 at 23:05):

That helped, thanks!


Last updated: May 15 2021 at 23:13 UTC