Zulip Chat Archive

Stream: general

Topic: inductive type <-> disjunction of constructors


view this post on Zulip Hunter Freyer (Oct 03 2020 at 01:18):

Let's say I have a type family like this:

inductive typed : fn2 -> val -> val -> Prop
| zero : typed fn2.zero val.nil val.nat
| succ : typed fn2.succ val.nat val.nat
....

There's only the one constructor that has fn2.zero in the first argument position. I'm trying to prove decidable (typed fn2.zero a b). I feel like the easiest thing is to convert this to decidable ((a = val.nil) /\ (b = val.nat)). Is there a way to do that? To convert an inductive type into an "or" over all its constructors?

view this post on Zulip Hunter Freyer (Oct 03 2020 at 01:19):

(I could do case splits as well, of course, but the more complex the constructors get, the harder it is to just split on everything)

view this post on Zulip Yury G. Kudryashov (Oct 03 2020 at 01:43):

See https://leanprover-community.github.io/mathlib_docs/commands.html#mk_iff_of_inductive_prop

view this post on Zulip Yury G. Kudryashov (Oct 03 2020 at 01:44):

BTW, does @[derive decidable] work?

view this post on Zulip Mario Carneiro (Oct 03 2020 at 02:55):

no

view this post on Zulip Hunter Freyer (Oct 03 2020 at 14:11):

Can anyone give an example of how to use mk_iff_of_inductive_prop?

view this post on Zulip Hunter Freyer (Oct 03 2020 at 14:15):

I think I got it: run_cmd tactic.mk_iff_of_inductive_prop `typed `typed_iff

view this post on Zulip Simon Hudon (Oct 03 2020 at 14:30):

Or you can do

mk_iff_of_inductive_prop typed typed_iff

as a declaration

view this post on Zulip Simon Hudon (Oct 03 2020 at 14:30):

I think it would fit in better as an attribute though

view this post on Zulip Hunter Freyer (Oct 03 2020 at 14:38):

aye. Thanks!


Last updated: May 09 2021 at 19:11 UTC