Hypothesis names with `split`

Stream: new members

[Josh Cohen]

I have a proof that looks something like the following (of course with a less trivial goal).

def optVal (l: List Nat) : Option Nat := sorry

theorem foo (l: List Nat) (x: Nat)
(H: (match (optVal l) with
| none => none
| some v => some v)
= some x):
true := by
  cases l <;> split at H <;> try contradiction
-- Rest of goals

Basically, I first want to do case analysis on an inductive datatype, then split on a (large) term being matched on in a hypothesis and rule out some trivial cases. The problem is that split clobbers the goal name. In the above example I am left with two goals with the same name h_2. Is there a way to choose hypothesis names for split or have it append to the current goal name (like repeated cases does)? I do not want to go through the resulting goals in order, so I need to be able to refer to the goal names, but this does not seem possible if they are all the same.

[Aaron Liu]

def optVal (l : List Nat) : Option Nat := sorry

theorem foo (l : List Nat) (x : Nat) (H :
    (match (optVal l) with
      | none => none
      | some v => some v) = some x) : true := by
  cases l with (split at H; try contradiction)
  | nil => sorry
  | cons x xs => sorry

[Jakub Nowak]

It's kinda weird, that this syntax is not documented when hovering over cases. I wouldn't even expect to see different documentation when hovering over with.

[Aaron Liu]

whaat

[Aaron Liu]

oh it's documented on the with

[Jakub Nowak]

Yes, it's a bit unintuitive to have separate documentation for with. It's not even a thing by itself, it's just part of the syntax for cases.

[Aaron Liu]

I remember it being documented on either cases or induction, maybe the documentation was changed?

[Jakub Nowak]

It's the same with induction.

[Jakub Nowak]

I think it was like that from the beginning: https://github.com/leanprover/lean4/commit/8182f83929df4bcafe0558f69eb2d96dab2b79cc
Line 534 on the right in src/Init/Tactics.lean (seems like github's link to line doesn't work for "Large diffs")

[Josh Cohen]

Thanks everyone, yes I had no idea about this with behavior.

[Josh Cohen]

Further question about this with behavior: suppose I have the following:

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) : p1 l ∧ p2 l := by
  cases l with (constructor; try assumption)
  | nil => sorry
  | cons x h =>
    case cons.left =>
      sorry
    case cons.right =>
      sorry

That is, my tactic in the with clause produces multiple subgoals per case, some of which are solved and others are left for me to solve. How can I select the resulting goals? The above code snippet does not work, it does not let me select case cons.left. The weird part is the error message: it says that the only valid label is case cons.right but changing to this just reverses the error.

[Aaron Liu]

I think it's running the tactics in that branch on both goals simultaneously. That's probably not what we usually want I think?

[Josh Cohen]

The strange thing is that the case cons.left statements give errors but seem to be "working". The following only gives the errors on the case statements (and not on apply H1):

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) (H1: forall x h, p1 (x :: h)) : p1 l ∧ p2 l := by
  cases l with (constructor; try apply H)
  | nil => sorry
  | cons x h =>
    case cons.left =>
      apply H1
    case cons.right =>
      sorry

While the following fails because, as you say, it does try and apply H1 to all goals:

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) (H1: forall x h, p1 (x :: h)) : p1 l ∧ p2 l := by
  cases l with (constructor; try apply H)
  | nil => sorry
  | cons x h =>
    apply H1

[Aaron Liu]

what if I write it like this, does it make more sense then?

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) : p1 l ∧ p2 l := by
  cases l with
  | nil =>
    (constructor; try assumption)
    all_goals sorry
  | cons x h =>
    (constructor; try assumption)
    all_goals
      case cons.left =>
        sorry
      case cons.right =>
        sorry

[Aaron Liu]

you can do something like this as a workaround to select the individual goals

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) : p1 l ∧ p2 l := by
  cases l with (constructor; try assumption)
  | nil => sorry
  | cons x h =>
    first
    | case cons.left =>
      sorry
    | case cons.right =>
      sorry

[Josh Cohen]

Aaron Liu said:

what if I write it like this, does it make more sense then?

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) : p1 l ∧ p2 l := by
  cases l with
  | nil =>
    (constructor; try assumption)
    all_goals sorry
  | cons x h =>
    (constructor; try assumption)
    all_goals
      case cons.left =>
        sorry
      case cons.right =>
        sorry

Yes, I am trying to figure out a way to avoid having to repeat the (constructor; try assumption) tactic in each case (but without losing name information)

[Josh Cohen]

Aaron Liu said:

you can do something like this as a workaround to select the individual goals

theorem foo {p1 p2: List Nat → Prop} (l: List Nat) (H: p1 []) : p1 l ∧ p2 l := by
  cases l with (constructor; try assumption)
  | nil => sorry
  | cons x h =>
    first
    | case cons.left =>
      sorry
    | case cons.right =>
      sorry

Thanks, this does work, although it seems like there should be a nicer way that does not require such workarounds.

[Aaron Liu]

I found the part of the code where it runs the tactic on each of the goals in a branch https://github.com/leanprover/lean4/blob/974fdd85c45cbb7c1a37fc79a98927bed92edc14/src/Lean/Elab/Tactic/Induction.lean#L544-L545