rw tactic introduces cases?

Stream: new members

[Preeyan Parmar]

When using the rw tactic with an inductively-defined function, it seems to introduce a case split that I don't understand at all.

inductive Tree where
| Leaf : Tree
| Pair : Tree → Tree → Tree

-- This isn't a sensible definition of anything real, it's just for an example
-- The key point is that I want a special definition for Pair Leaf _, and a fallback definition for when the first argument of Pair is not a Leaf
def Prune : Tree → Tree
| .Leaf => .Leaf
| .Pair .Leaf _ => .Leaf
| .Pair x y => .Pair (Prune x) y

-- This isn't a true theorem, it's just to illustrate the tactic state after using rw
theorem Foo : Prune t = .Leaf := by
  induction t with
  | Leaf => sorry
  | Pair x y ih ih' => rw [Prune]

What I want to do is treat the two cases Pair Leaf _ and Pair (not leaf) _ separately. The rw tactic has introduced two cases here, but the two subgoals are

case Pair
xy: Tree
ih: Prune x = Tree.Leaf
ih': Prune y = Tree.Leaf
⊢ Tree.Pair (Prune x) y = Tree.Leaf

case Pair.x_2
xy: Tree
ih: Prune x = Tree.Leaf
ih': Prune y = Tree.Leaf
⊢ x = Tree.Leaf → False

which I can't make sense of. What's going on here?

[Paul Rowe]

I think rw is doing a lot of work behind the scenes to already solve the case when x = Leaf. What you are seeing in the first goal is the result of rewriting Prune when x \ne Leaf. The second goal is asking you to prove that x \ne Leaf.

A more verbose, but also more transparent strategy is to take cases on x before continuing.

theorem Foo : Prune t = .Leaf := by
  induction t with
  | Leaf => sorry
  | Pair x y ih ih' =>
    cases x with
    | Leaf => sorry
    | Pair x' y' => sorry

[Preeyan Parmar]

The second goal is asking you to prove that x \ne Leaf

Why does it introduce this goal? It's possible for x to be a Leaf.

[Paul Rowe]

I should caveat everything below by saying that I don't really know how rw works, so I'm making some educated guesses. If anybody else has a better explanation, I'd love to see it.

At the place you are trying to perform a rw, Lean only knows that the argument to Prune is Tree.Pair x y. This means that two of your patterns might be viable here. I believe rw tries to work with each of them in turn. The first pattern match replaces x with Leaf and the rewrite easily takes care of that case behind the scenes (i.e. you never see it). Because patterns are matched in order, the third pattern for Prune only applies when x \ne Leaf. That is, in order to use this case, you have an obligation to prove that x \ne leaf. But the pattern itself is not strong enough to impose any particular structure on x in this case and rw isn't smart enough to fill in the blanks.

To see a contrast, you could write your Prune function as follows:

def Prune : Tree → Tree
| .Leaf => .Leaf
| .Pair .Leaf _ => .Leaf
| .Pair (.Pair x' y') y => .Pair (Prune (.Pair x' y')) y

If you do that, and keep your proof attempt at Foo unchanged, the stronger pattern now replaces x with Tree.Pair x' y' and Lean is smart enough to figure out that this can't be equal to Leaf. The result is that you only get one goal as expected. However, behind the scenes, it still creates an obligation to prove that x \ne Leaf, but since the pattern match replaces x with Tree.Pair x' y', rw is smart enough to discharge that goal on its own.

[Timo Carlin-Burns]

If this was an intentional feature of rw, I would expect that x ≠ Tree.leaf would be a hypothesis in goal state after rewriting by the third equation (Prune x y to .Pair (Prune x) y), not a new goal.

[Timo Carlin-Burns]

I also don't know exactly how rw works. My best guess for what's happening is that when Prune is defined, a lemma is generated for each of its equations. Then rw [Prune] ends up rewriting by the third equation lemma because that's the only one which is applicable.

theorem prune_case1 : Prune .Leaf = .Leaf := rfl
theorem prune_case2 (x : Tree): Prune (.Pair .Leaf y) = .Leaf := rfl
theorem prune_case3 (x y : Tree) (h : x ≠ .Leaf) : Prune (.Pair x y) = .Pair (Prune x) y := sorry

theorem Foo : Prune t = .Leaf := by
  induction t with
  | Leaf => sorry
  | Pair x y ih ih' => rw [prune_case3] -- case 3 is the only lemma which is applicable

[Timo Carlin-Burns]

Here is another example with similar behavior

def myFun : Nat → String
  | 5 => "five"
  | (n + 2) => myFun n
  | n => "n"

example (n : Nat) : myFun n = "foo" := by
  rw [myFun] -- seems to be rewriting by the third equation, even though the first or second could theoretically apply.
/- unsolved goals

  n: Nat
  ⊢ "n" = "foo"

  n: Nat
  ⊢ n = 5 → False

  n: Nat
  ⊢ ∀ (n_1 : Nat), n = Nat.succ (Nat.succ n_1) → False

-/

[Damiano Testa]

In fact, you can find out what are the auto-generated lemmas:

import Mathlib.Util.WhatsNew

inductive Tree where
| Leaf : Tree
| Pair : Tree → Tree → Tree

whatsnew in
def Prune : Tree → Tree
| .Leaf => .Leaf
| .Pair .Leaf _ => .Leaf
| .Pair x y => .Pair (Prune x) y

[Timo Carlin-Burns]

I tried that but I don't see any equation lemmas listed in the output of whatsnew...

[Patrick Massot]

They are not generated immediately but on demand.

[Preeyan Parmar]

So how can I actually prove something about a function that is inductively defined with fallback cases? I like Timo's example:

def myFun : Nat → Nat
  | 5 => 0
  | n + 2 => myFun n
  | n => 0

theorem Foo (n : Nat) : myFun n = 0 := match n with
  | 5 => by rw [myFun]
  | n + 2 => by rw [myFun]; exact Foo n; sorry
  | n => by rw [myFun]; sorry; sorry

The theorem here is actually true, so it ought to have a proof. But I haven't managed to find a proof yet. In my attempt above, the sorrys are goals like n \neq 3 which are true because that case would have already been matched, but I don't know how to fill in the proof.

[Preeyan Parmar]

I can fold the proof into the definition like this:

def myFun : Nat → {n : Nat // n = 0}
  | 5 => ⟨ 0, rfl ⟩
  | n + 2 => myFun n
  | n => ⟨ 0, rfl ⟩

but folding everything you need to know about the function into the definition might be unwieldy in general?

[Joachim Breitner]

In the future (once https://github.com/leanprover/lean4/pull/3432 reaches you) you'll get a custom induction principle for your (recursive) function that takes care of this.

Until then , does unfold followed by split help?

[Preeyan Parmar]

unfold then split does work for this:

theorem Foo (n : Nat) : myFun n = 0 := by
  unfold myFun; split; rfl; apply Foo; rfl