named match constructs

Stream: new members

[Henning Dieterichs]

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]

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]

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]

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

[Henning Dieterichs]

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]

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

[Mario Carneiro]

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]

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]

that will cut your 16 cases down to 3

[Henning Dieterichs]

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]

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]

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]

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

[Mario Carneiro]

yes

[Mario Carneiro]

although I think merge_result looks like a good side definition anyway

[Mario Carneiro]

diverge_result looks like a nested if-then to me

[Henning Dieterichs]

and merge_result?

[Mario Carneiro]

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]

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