Collapse cases

Stream: lean4

[Marcus Rossel]

In the following (non-mwe) example, both subgoals of a cases do pretty much the same thing. The only difference is where one of the assumptions (hi) comes from:

    cases hs.exec
    case single hi =>
      cases hi <;> (
        have := mt (Finset.ext_iff.mp hr _).mpr <| (by assumption)
        have := Finmap.ids_def'.mpr ⟨_, Eq.symm (by assumption)⟩
        contradiction
      )
    case trans _ hi _ =>
      cases hi <;> (
        have := mt (Finset.ext_iff.mp hr _).mpr <| (by assumption)
        have := Finmap.ids_def'.mpr ⟨_, Eq.symm (by assumption)⟩
        contradiction
      )

Is it possible to collapse these cases somehow, by telling the cases tactic what hi is supposed to be in each case (without doing the actual case distinction)?

[Trebor Huang]

That's called the Or pattern in some languages I suppose.

[Mario Carneiro]

The recently discussed on_goal tactic would support this, using the syntax on_goal single hi, trans _ hi _ => ..., and it would be a natural extension to use the same grammar for case as well

[Marcus Rossel]

Mario Carneiro said:

The recently discussed on_goal tactic would support this, using the syntax on_goal single hi, trans _ hi _ => ..., and it would be a natural extension to use the same grammar for case as well

But this isn't implemented yet, right?

[Mario Carneiro]

no, but API design is the hard part with tactics such as this. If you want a tactic you can use right now it's pretty easy:

syntax "case' " (ident*),* " => " tacticSeq : tactic
macro_rules
  | `(tactic| case' $[$xs:ident*],* => $tac) => do
    let tacs ← xs.mapM fun xs => `(tactic| case $(xs[0]) $(xs[1:])* => $tac)
    `(tactic| ($[$tacs]*))

example : (True → True) ∧ (True → True) := by
  constructor <;> intro
  case' left h, right h => apply h

[Marcus Rossel]

Mario Carneiro said:

If you want a tactic you can use right now it's pretty easy:

syntax "case' " (ident*),* " => " tacticSeq : tactic
macro_rules
  | `(tactic| case' $[$xs:ident*],* => $tac) => do
    let tacs ← xs.mapM fun xs => `(tactic| case $(xs[0]) $(xs[1:])* => $tac)
    `(tactic| ($[$tacs]*))

It seems I've grown pretty dependent on this tactic over the past couple of months. And now the new TSyntax has broken it :sweat_smile: Do there happen to be "proper" alternatives for this tactic now?

[Henrik Böving]

So first things first we want to use xs[0]! here in the latest nightly, then the error becomes

type mismatch
  Array.getOp! xs 0
has type
  Lean.TSyntax `ident : Type
but is expected to have type
  Lean.TSyntax `Lean.binderIdent : Type

Where binderIdent is defined as:

syntax binderIdent := ident <|> "_"

So I'd say a Coe (TSyntax `ident) (TSyntax `binderIdent) is in order here right? CC @Sebastian Ullrich

[Sébastien Michelland]

I believe you can simply use the appropriate syntax category:

syntax "case' " (Lean.binderIdent*),* " => " tacticSeq : tactic
macro_rules
  | `(tactic| case' $[$xs*],* => $tac) => do
    let tacs ← xs.mapM fun xs => `(tactic| case $(xs[0]) $(xs[1:])* => $tac)
    `(tactic| ($[$tacs]*))

[Henrik Böving]

That works as well yeah. But In general this coercion makes sense to have in the compiler I think

[Mac]

Henrik Böving said:

That works as well yeah. But In general this coercion makes sense to have in the compiler I think

Yeah... there are a LOT of missing TSyntax coercions. :stuck_out_tongue_wink: I think it is mostly going to be a manually defined thing for now. Unless @Sebastian Ullrich wants PRs that fill in gaps.

[Sebastian Ullrich]

We should probably be conservative and add coercions only where they save a lot of $(xs[0]):ident $(xs[1:]):ident* typing. And in this case the error even points to a probably better design as mentioned.