Multiple case

Stream: general

[Sorawee Porncharoenwase]

I have a custom tactic named muti_case that I find myself using a lot. Today I just found out about https://github.com/leanprover-community/lean/commit/042d7e592f6e9356c3324beca1908419a423966e by @Eric Wieser which seems to be doing the same thing. I would love if this is a part of the core tactic. What's the status of this feature?

Moreover, I think it would be useful to allow * as a case name too. It would for example allow us to write something like:

inductive val : Type
| a : val
| b : val
| c : val
| d : val

open val

def test : val → val → bool
| a c := tt
| a d := tt
| b a := ff
| b b := ff
| c a := tt
| c c := tt
| d d := ff
| _ _ := ff

example {x y} (h : test x y = tt) : x = a ∨ x = c :=
begin
  cases x; cases y,
  case [a *, c *] { simp },
  case [b *, d *] { contradiction },
end

[Eric Wieser]

(leanprover-community/lean#508 for the PR)

[Eric Wieser]

There's some existing discussion about this in #metaprogramming / tactics

[Mario Carneiro]

the pr link is incorrect

[Mario Carneiro]

What's the actual tactic being proposed here?

[Eric Wieser]

Improvements to case

[Mario Carneiro]

I mean what does multi_case do

[Eric Wieser]

Runs the tactic block on all matching cases

[Eric Wieser]

Fixed the link, and attempted to guess what the broken lines of the PR were meant to me - I got this working locally in a now discarded buffer, then must have failed at copying things piecewise into lean core

[Sorawee Porncharoenwase]

Here's my current definition of muti_case:

@[interactive]
meta def multi_case
  (ns : parse (list_of ident_*))
  (ids : parse $ (tk ":" *> ident_*)?)
  (tac : itactic) : tactic unit :=
ns.mmap' (λ ns, tactic.interactive.case ns ids tac)

Pretty much, it allows you to write:

multi_case [case1a case1b, case2a case2b] : v1 v2 {
  tacs
}

Instead of:

case case1a case1b : v1 v2 {
  tacs
},
case case2a case2b : v1 v2 {
  tacs
},

The reason why I don't use any_goals or any_goals + solve1 is that it often causes deterministic timeout for me.

The PR by @Eric Wieser is better because it doesn't force variable naming in each subcase to be the same.

[Eric Wieser]

Another difference is that in my version, within the {} you can see all the matching goals, rather than just the first one

[Sorawee Porncharoenwase]

Ooh, that's very nice :)

[Eric Wieser]

So your

multi_case [case1a case1b, case2a case2b] : v1 v2 {
  tacs
}

is the linked PR's

case [case1a case1b : v1 v2, case2a case2b: v1 v2] {
  all_goals { tacs }
}

[Mario Carneiro]

If you can see all the matching goals, then does that mean there is an additional all_goals wrapper before you can do things?

[Mario Carneiro]

oh you said this

[Sorawee Porncharoenwase]

Ah, I seem to misunderstand your PR then. I thought it's exactly the same as mine, but apparently that's not the case.

It's still a good improvement, IMO, and would be a better building block for my custom tactic.

[Eric Wieser]

The motivation for my design was:

• To make the goal view helpful
• To make something like this work:

case [case1a case1b : v1 v2, case2a case2b: v1 v2] {
  all_goals { simp only [some_lemma] },
  { exact some_closing_lemma_1, }
  { exact some_closing_lemma_2, }
}

[Mario Carneiro]

I think that it makes sense to bind the variables differently for different cases, as in the PR, but the names should be "approximately the same" and the tactic script run in each case should be the same, suggesting that the all_goals wrapper be built in

[Eric Wieser]

If the all goals wrapper is built in, there's no nice way to say "the proof for these two cases is almost but not quite identical".

[Eric Wieser]

I mean sure, you can use <|>, but that obfuscates which goal you're actually trying to work on

[Mario Carneiro]

I think of this multi-case more like a match branch with an or pattern

[Eric Wieser]

I had a nasty time refactoring proofs a while back that used something like simp [foo] <|> simp [bar], as I removed a simp lemma the first branch was relying on, but all I got was errors about the second branch not matching

[Eric Wieser]

Mario Carneiro said:

I think of this multi-case more like a match branch with an or pattern

match branches with or are not a thing that exists today, right?

[Mario Carneiro]

They are in some languages, e,g:

enum Num { Neg(u32), Zero, Pos(u32) }
use Num::*;

fn abs(n: Num) -> u32 {
  match n {
    Neg(i) | Pos(i) => i,
    Zero => 0,
  }
}

[Mario Carneiro]

You can also kind of do or-patterns in lean using wildcard matches

[Sorawee Porncharoenwase]

Speaking of this, I have another tactic named soft_case. It's exactly like the current case, except that it is not wrapped with solve1. This allows us to dive into a case, cases on a variable in that case, go back up, and then all_goals at the parent level. E.g.,

inductive val : Type
| a (x : bool) : val
| b : val
| c : val
| d : val

open val

def test : val → bool
| (a ff) := tt
| (a tt) := ff
| b := ff
| c := tt
| d := ff

example {x} (h : test x = tt) : x = (a ff) ∨ x = c :=
begin
  cases x,
  soft_case a : x { cases x },
  all_goals { finish },
end

Would this be something useful to people?

[Eric Wieser]

focus_case is probably a better name, for consistency with tactic#focus

[Eric Wieser]

The question is, what semantics would focus_case with multiple cases have?

-- goals: A, B, C, D
focus_case [A, C] {
    work_on_goal 0 {split},
    work_on_goal 1 {split},
    -- goals: A1, A2, C1, C2
}
-- what should the goal list be here?

Ideally you'd reconstruct A1, A2, B, C1, C2, D, but I think the information to recover that simply doesn't exist

[Mario Carneiro]

I was also going to suggest something like soft_case to address @Eric Wieser 's comment about cases that are almost but not quite the same. I think it could be implemented with an option on case

[Mario Carneiro]

I also have a slight preference for focus_case being an option on case instead of a separate tactic, although I don't have a good suggestion for what sigil is appropriate. case...?

[Eric Wieser]

Also, what would be the semantics of:

focus_case succ : n {
   let m := n,
},
focus_case succ : o {
   -- wait, we already intro'd the variable as `n`?
},

[Eric Wieser]

Renaming all the ns to os would be fine, but it's not obvious to me that that would just work out of the box

[Mario Carneiro]

If focus_case works as I suggested, where the focus part is built in, then in your example

-- goals: A, B, C, D
focus_case [A, C] {
  split,
  -- goals: A -> A1, A2, also C -> C1, C2
}
-- goals: A1, A2, B, C1, C2, D

is doable

[Eric Wieser]

How does focus_case know where to reinsert the new goals into the goal list?

[Mario Carneiro]

it is the one that deconstructed the list

[Eric Wieser]

That would require some way to inspect the A1 goal and ask "did you come from A or C", right?

[Mario Carneiro]

No, it is essentially list.bind

[Mario Carneiro]

where goals that aren't being focused are just inserted as is into the new goal list

[Eric Wieser]

Oh, I see your point - you're ok because your proposed focus_case executes the tactic block on each goal

[Eric Wieser]

As opposed to executing it once against all goals

[Mario Carneiro]

right, that way of working is annoying anyway; most tactics want to work on a single goal

[Mario Carneiro]

especially with focus_case you can just chain several of them if you want to do different things in each case

[Mario Carneiro]

The semantics of the double focus_case is the same as case: the variables get renamed on entry to the block

[Mario Carneiro]

-- a_1 : nat
focus_case succ : n {
   -- n : nat
   let m := n,
   -- n : nat, m := n
},
focus_case succ : o {
   -- o : nat, m := o
},

[Eric Wieser]

So, my current code is something like

case [A, B] {
   all_goals { foo },
   all_goals { bar },
   work_on_goal 0 { bar0 },
   work_on_goal 1 { bar1 },
   all_goals { baz }, --done
}

I guess you're proposing I instead write that as

focus_case [A, B] { foo },
focus_case [A, B] { bar },
focus_case A { bar0 },
focus_case B { bar1 },
case [A, B] { baz },

[Eric Wieser]

The nice bit about my structure is that I can inspect the proof state without seeing goals C and D I don't care about

[Eric Wieser]

Whereas in your proposal, I either only see the proof state for A, or I see it for all goals

[Mario Carneiro]

I think that should be fixed generally though

[Eric Wieser]

You'd consider that a flaw in the infoview?

[Mario Carneiro]

that's a server goal reporting issue

[Mario Carneiro]

if an interactive tactic block is called multiple times the goal view should show all of the incoming states

[Eric Wieser]

There's still a structuring argument that I'd like to wrap the A B part of the proof in braces to separate it from the C D part

[Eric Wieser]

Maybe there are other ways to achieve that

[Mario Carneiro]

maybe that needs its own tactic

[Mario Carneiro]

subcase?

[Eric Wieser]

case_group?

[Mario Carneiro]

cases? :upside_down:

[Eric Wieser]

subcases / case_group would have to be a solve-style tactic though, unless you're ok with it inserting remaining goals in a random place

[Mario Carneiro]

probably it would put all the new goals at the front

[Mario Carneiro]

in particular, that means that case_group [B, C] {} can be used to reorder A, B, C, D to B, C, A, D

[Eric Wieser]

I thought about this a bit for work_on_goals, where it was particularly nasty because if you want to work on goals 0 and 2, then 1 and 3, you have to use work_on_goals [0, 2] { }, work_on_goals [2, 3] { } as after the first work_on_goals the goals have re-ordered!

[Eric Wieser]

But I guess for named goals that problem goes away