pattern matching 101

Stream: general

[Scott Morrison]

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?

[Kenny Lau]

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

[Scott Morrison]

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?

[Scott Morrison]

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

[Scott Morrison]

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

[Sebastian Ullrich]

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

[Sean Leather]

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

[Kenny Lau]

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

if o = some k then _ else Y

[Scott Morrison]

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

[Kenny Lau]

so maybe give us more context?

[Simon Hudon]

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.

[Simon Hudon]

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

[Scott Morrison]

hmm, my type

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

[Scott Morrison]

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

[Simon Hudon]

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 α?

[Scott Morrison]

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.

[Sean Leather]

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

[Scott Morrison]

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

[Scott Morrison]

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?

[Sean Leather]

@[derive decidable_eq]
inductive ...

[Scott Morrison]

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

[Sean Leather]

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

[Sean Leather]

Perhaps #print <type-name>.decidable_eq?