non-structured, non-anonymous cases

Stream: lean4

[Jakob von Raumer]

In some situations, one wants to destruct a pair or other structure instance in the tactic goal, without wanting to indent. have or let don't do this, because they don't change the goal. Can we have a cases syntax that somehow allows for something like Lean 3's cases x with (mk a b)?

[Leonardo de Moura]

@Jakob von Raumer
We can add this feature. In the meantime, consider using the renameI tactic for renaming inaccessible names.
If the cases creates a single goal, you can even have a macro that applies cases and renameI.

[Leonardo de Moura]

The next tactic is based on renameI. Here is an example:

def f (xs : List Nat) : Nat :=
  match xs with
  | [] => 1
  | [a, b] => (a + b).succ
  | _ => 2

theorem ex1 (xs : List Nat) (hr : xs.reverse = xs) (ys : Nat) : ys > 0 → f xs > 0 := by
  simp [f]
  split
  next => intro hys; decide
  next => intro hys; apply Nat.zero_lt_succ
  next zs n₁ n₂ => intro hys; decide

[Leonardo de Moura]

Here is a renameI example

example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by
  intros
  renameI h1 _ h2
  apply Eq.trans
  apply Eq.symm
  exact h2
  exact h1

[Jakob von Raumer]

Ah, I see, that should make it simple to combine the two. Though at some point this will probably be covered by the port of rcases anyway. /cc @Mario Carneiro

[Mario Carneiro]

You can also use cases x with | mk a b => ?_, although it doesn't read very nicely

[Jakob von Raumer]

This is a an okay solution in principle, unfortunately the Infoview doesn't update correctly in the line after? /cc @Sebastian Ullrich I thought that was one of the things you had fixed during TBA?

[Sebastian Ullrich]

That doesn't look like code we would expect students to write, haha

[Sebastian Ullrich]

Not sure yet if this needs some special case