## Stream: new members

### Topic: named match constructs

#### Henning Dieterichs (Nov 30 2020 at 15:06):

These _match_{n} names really start to annoy me (I have quite a few of them).
Here is a very simple example:

def test (p: nat × nat): nat × nat := match p with
| (a, b) := (a, b)
end

lemma baz (p: (nat × nat)): test p = p :=
begin
rw test,
cases p,
rw test._match_1,
end

Can I somehow name them without introducing another function?

#### Rob Lewis (Nov 30 2020 at 15:43):

You should never really need to deal with these manually. Do the cases first and use simp instead of rw to unfold test.

lemma baz (p: (nat × nat)) (h : test p = p) : false :=
begin
cases p,
simp only [test] at h,
end

#### Mario Carneiro (Nov 30 2020 at 15:55):

You should also try to use the equation compiler instead of match because it gets better names:

def test : nat × nat -> nat × nat
| (a, b) := (a, b)

#### Eric Wieser (Nov 30 2020 at 15:56):

Is there any way to use the equation compiler in a lambda? Or is λ x, match x with ... | ... end unavoidable?

#### Henning Dieterichs (Nov 30 2020 at 15:58):

In my case, both things don't work always.
I have definitions like this:

def ant_eval' : Ant (bool)  option Result
| (Ant.leaf matches leaf) := if matches
then some $Result.leaf leaf else some$ Result.no_match
| (Ant.branch tr1 tr2) :=  match (ant_eval' tr1, ant_eval' tr2) with
| (some Result.no_match, r) := r
| (r, some Result.no_match) := r
| _ := none
end
| (Ant.diverge matches tr) := match (matches, ant_eval' tr) with
| (ff, r) := r
| (tt, some Result.no_match) := some Result.diverged
| _ := none
end

I often need to do cases on both arguments of the match, which then leads to 16 cases - that gets very confusing very quickly. I'd like to name the matches, so I can add lemmas that help to deal with them. I already to this, but find the _match_{n} very confusing.

#### Mario Carneiro (Nov 30 2020 at 16:02):

You don't need to match on a pair, you can just match two things

#### Mario Carneiro (Nov 30 2020 at 16:08):

But you can always hoist a match statement out of whatever context it is in and make your own definition. Something like this:

def merge_result : option Result  option Result  option Result
| (some Result.no_match) r := r
| r (some Result.no_match) := r
| _ _ := none

def diverge_result : bool  option Result  option Result
| ff r := r
| tt (some Result.no_match) := some Result.diverged
| _ _ := none

def ant_eval' : Ant (bool)  option Result
| (Ant.leaf matches leaf) := if matches
then some $Result.leaf leaf else some$ Result.no_match
| (Ant.branch tr1 tr2) :=  merge_result (ant_eval' tr1) (ant_eval' tr2)
| (Ant.diverge matches tr) := diverge_result matches (ant_eval' tr)

This is what lean is doing anyway when you use match. But this gives you the opportunity to prove theorems specifically about merge_result and diverge_result too, which means you don't have as many nested cases to deal with

#### Mario Carneiro (Nov 30 2020 at 16:09):

Given the structure of these matches, it might be better to just use cases on r = some Result.no_match instead of a pattern match

#### Mario Carneiro (Nov 30 2020 at 16:10):

that will cut your 16 cases down to 3

#### Henning Dieterichs (Nov 30 2020 at 16:11):

I understand, and probably this is what I should do. However, I don't like that you cannot see by simply looking at ant_eval' that it resembles the algorithm of the paper that I want to prove correct, as many interesting details are scattered into smaller functions.

#### Henning Dieterichs (Nov 30 2020 at 16:12):

use cases on r = some Result.no_match instead of a pattern match

I though lean cannot unfold the definition if I just have r != some Result.no_match? I guess I need assisting lemmas to make this more comfortable to use?

#### Mario Carneiro (Nov 30 2020 at 16:22):

If you have r != some Result.no_match and you wrote if r = some Result.no_match then .. else .. in the definition then lean will be able to rewrite it away using split_ifs

#### Henning Dieterichs (Nov 30 2020 at 16:24):

So do you suggest to replace the matchs in ant_eval' with two nested if/elses?

yes

#### Mario Carneiro (Nov 30 2020 at 16:25):

although I think merge_result looks like a good side definition anyway

#### Mario Carneiro (Nov 30 2020 at 16:26):

diverge_result looks like a nested if-then to me

#### Henning Dieterichs (Nov 30 2020 at 16:26):

and merge_result?

#### Mario Carneiro (Nov 30 2020 at 16:27):

def merge_result (r₁ r₂ : option Result) : option Result :=
if r₁ = some Result.no_match then r₂ else
if r₂ = some Result.no_match then r₁ else none

#### Henning Dieterichs (Nov 30 2020 at 16:28):

oh these subscripts look great, I forgot that I can use them, thanks for pointing that out ;) Yeah, you are right, this definition might even be more readable

Last updated: May 11 2021 at 21:10 UTC