Zulip Chat Archive

Stream: general

Topic: pattern matching 101


view this post on Zulip Scott Morrison (Apr 25 2018 at 08:39):

Easy question: how do I do pattern matching against values? Given k : nat, naively I could try writing

match n with
| k := something
| _ := something_else
end

a glorified if n = k then something else something_else, but of course this doesn't work, because Lean doesn't treat the k in the pattern as related to the earlier k.

Am I just meant to use if ... then ... else? Or can I get the pattern matcher to help me?

view this post on Zulip Kenny Lau (Apr 25 2018 at 08:40):

you need to use if then else. match only deals with constructors.

view this post on Zulip Scott Morrison (Apr 25 2018 at 08:43):

That's what I feared. How sad. So if I want to write something that given some n where n = k does X, and given any other some n or none does Y... What's the idiomatic way to write this?

view this post on Zulip Scott Morrison (Apr 25 2018 at 08:43):

(Preferably your answer shouldn't use option.is_some or friends, just pretend option is a bare inductive type with no dressing up.)

view this post on Zulip Scott Morrison (Apr 25 2018 at 08:44):

In particular, how can I do this without writing the symbol Y twice?

view this post on Zulip Sebastian Ullrich (Apr 25 2018 at 08:55):

Other languages have pattern guards for this, but Lean doesn't... yet. You'll have to factor Y out into a let.

view this post on Zulip Sean Leather (Apr 25 2018 at 08:55):

That's what I feared. How sad. So if I want to write something that given some n where n = k does X, and given any other some n or none does Y... What's the idiomatic way to write this?

This sounds like something you'd use pattern match guards for in Haskell:

case n of
  Just k | n == k -> something
  _ -> something_else

view this post on Zulip Kenny Lau (Apr 25 2018 at 08:56):

In particular, how can I do this without writing the symbol Y twice?

if o = some k then _ else Y

view this post on Zulip Scott Morrison (Apr 25 2018 at 08:57):

okay, good, except I've over-minimised of course, and there are lots of other fields that I don't care about matching :-)

view this post on Zulip Kenny Lau (Apr 25 2018 at 08:58):

so maybe give us more context?

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:30):

Is it possible that your type is like the following?

inductive my_type
| constr : a -> b -> c -> d -> e -> my_type
| other : a' -> b' -> my_type

In Haskell, a common advice is to make that two or more types, separate the sum aspect and the product aspect.

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:31):

Then, you can use selectors on to access whatever part of the product that you care about

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:33):

hmm, my type

inductive edit_distance_progress (l₁: list α) (l₂: list α)
| exactly : ℕ → edit_distance_progress
| at_least : ℕ → partial_edit_distance_data α → edit_distance_progress

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:33):

and I need to check if I have an exactly _ _ k for some specified value of k.

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:38):

Ok, it's not as bad as I thought. I thought because you didn't want to repeat Y. Is it a pattern for partial_edit_distance_data α?

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:43):

I'm not sure what you mean. The offending code (which works, just looks gross) is <https://github.com/semorrison/lean-tidy/blob/master/src/tidy/rewrite_search.lean#L64-L84>. You can see lines 72-74 and lines 76-78 are almost identical because of this.

view this post on Zulip Sean Leather (Apr 25 2018 at 13:49):

Why can't you do something like if update_edit_distance h.distance = exactly _ _ k then ... else ... as Kenny suggested?

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:51):

Oh... somehow I thought those _s would be a problem, but of course they're not. Thank you!

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:53):

I will need an extra decidable instance for this. I remember there is some trick for synthesising decidable instances for boring inductive types....? Anyone remember?

view this post on Zulip Sean Leather (Apr 25 2018 at 13:54):

@[derive decidable_eq]
inductive ...

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:55):

Lovely! And where do I find out what derive is doing? :-)

view this post on Zulip Sean Leather (Apr 25 2018 at 13:57):

I'm sure there's a #print that'll tell you, but I never remember which one. :blush:

view this post on Zulip Sean Leather (Apr 25 2018 at 13:58):

Perhaps #print <type-name>.decidable_eq?


Last updated: May 13 2021 at 22:15 UTC