tactic to destructure under certain conditions?

Stream: mathlib4

[Thomas Murrills]

Often, if you have a certain fact about something, you can decompose it in a certain way. For instance, if you have a hypothesis which says that a list l satisfies 0 < l.length, you can find x and xs to rewrite l as x :: xs. It'd be convenient to target some such l in the goal type and rewrite it directly to this form (without knowing the lemma name)—something like write l as x :: xs (name pending). Ideally these sorts of decomposition lemmas would be tagged as such so that this tactic could search through all lemmas that enabled such a rewrite and try to find hypotheses to apply them.

So, kind of like rw or simp, but you specify what you want to rewrite part of your expression to instead of how to rewrite it, and in a way that lets us introduce and name local decls in the process. (Not like set(m), since we want to expand something using a nontrivial fact instead of condense something.)

Does this exist already in some form? (I might be blanking.)

[Scott Morrison]

No, it doesn't.

[Scott Morrison]

Perhaps it could be obtain! x :: xs := l, as in "I want to destructure l as x :: xs, and if that's not a thing you can do, please try harder!"

[Patrick Massot]

Note that Lean Verbose does that.

[Thomas Murrills]

Hmm, interesting! Does obtain rewrite the goal? I'm imagining it'd be useful to replace l everywhere in the goal in one fell swoop! (Maybe not, though.) (obtain_rw?)

[Patrick Massot]

See here for instance. |u n - l| ≤ l / 2 is not literally an inductive type with fields -(l/2) ≤ u n - l and u n - l ≤ l / 2.

[Thomas Murrills]

Nice! How does it figure out which lemmas to use? Does it use simp or something under the hood?

[Patrick Massot]

Lemmas are registered using an attribute.

[Patrick Massot]

The tactic doing that is very simple: https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/Tactics/By.lean#L36-L44. Sorry about the total lack of documentation. I had a deadline to get a version good enough to write the examples files, so documentation wasn't a priority.

[Patrick Massot]

The tactic elaborator is at https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/English/By.lean#L6-L7 for the English version.

[Thomas Murrills]

Gotcha, nice, thanks for the links! Re: documentation, that's ok—at a glance, the code looks clear and nicely organized. :)

[Patrick Massot]

You can see that By stuff we get new stuff first tries to call rcases but if it fails then it calls lemmas that are registered as anonymous split lemmas.

[Kyle Miller]

Here's an example of using obtain for your original use case:

theorem List.ne_nil_iff_exists {α : Type*} {xs : List α} : xs ≠ [] ↔ ∃ a as, xs = a :: as := by
  cases xs <;> simp

theorem List.length_pos_iff_exists {α : Type*} {xs : List α} :
    0 < xs.length ↔ ∃ a as, xs = a :: as := by
  rw [List.length_pos, List.ne_nil_iff_exists]

example (l : List Nat) (h : 0 < l.length) : l = l.head! :: l.tail := by
  obtain ⟨x, xs, rfl⟩ := List.length_pos_iff_exists.mp h
  /-
  x : ℕ
  xs : List ℕ
  h : 0 < List.length (x :: xs)
  ⊢ x :: xs = List.head! (x :: xs) :: List.tail (x :: xs)
  -/

That's one way these lemmas could be phrased, as lemmas that conclude in a nested existential that ends in an equality. Another way could be using lemmas that are more like eliminators.

[Thomas Murrills]

Nice! (I am ofc specifically curious about tagging lemmas for automatic use and having "nice" syntax (i.e. we're destructuring l, not the ∃), but this encourages the notion that obtain can be a big part of the solution, one way or another.)

[Thomas Murrills]

The existential phrasing was the one I had in mind for these lemmas; but I'm curious, what would an eliminator-style one look like?

[Kyle Miller]

The elab_as_elim here is just to get refine to calculate the motive argument. Otherwise you tend to have to pass one in yourself explicitly.

@[elab_as_elim]
theorem List.length_pos_elim {α : Type*} {motive : List α → Sort*}
    {xs : List α} (h : 0 < xs.length) (cons : ∀ a as, motive (a :: as)) : motive xs :=
  match xs with
  | [] => by simp at h
  | x :: xs => cons x xs

example (l : List Nat) (h : 0 < l.length) {p : List Nat → Prop} (h' : p l) :
    l = l.head! :: l.tail := by
  revert h'
  refine List.length_pos_elim h ?_
  intro x xs h'
  /-
  l : List ℕ
  h : 0 < List.length l
  p : List ℕ → Prop
  x : ℕ
  xs : List ℕ
  h' : p (x :: xs)
  ⊢ x :: xs = List.head! (x :: xs) :: List.tail (x :: xs)
  -/

[Kyle Miller]

The whole "rewriting everywhere" is an illusion. The way it works (even in obtain) is you revert everything that can be rewritten, you compute a motive that cuts out the thing being "rewritten", and then you pass that motive to the eliminator.

[Kyle Miller]

The a :: as in the theorem is what gets pasted in.

[Kyle Miller]

I guess that theorem should be a def, oops.

[Kyle Miller]

I think this could be likened to a continuation passing style version of the one that returns an existential. Though doing obtain on the existential is just deferring to the Exists and Eq eliminators.