Zulip Chat Archive

Stream: new members

Topic: named match constructs


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

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

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

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

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

view this post on Zulip Mario Carneiro (Nov 30 2020 at 16:02):

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

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

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

view this post on Zulip Mario Carneiro (Nov 30 2020 at 16:10):

that will cut your 16 cases down to 3

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

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

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

view this post on Zulip Henning Dieterichs (Nov 30 2020 at 16:24):

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

view this post on Zulip Mario Carneiro (Nov 30 2020 at 16:24):

yes

view this post on Zulip Mario Carneiro (Nov 30 2020 at 16:25):

although I think merge_result looks like a good side definition anyway

view this post on Zulip Mario Carneiro (Nov 30 2020 at 16:26):

diverge_result looks like a nested if-then to me

view this post on Zulip Henning Dieterichs (Nov 30 2020 at 16:26):

and merge_result?

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

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