can this be proved without writing a motive explicitly?

Stream: lean4

[Ted Hwa]

The lemma below is very simple but seemingly can't be proved without writing out a motive explicity. Simpler approaches result in "motive is not type correct" or similar. It seems like the proof in head is causing the issue.

I want something that will generalize to arbitrary type for state (not just Nat) and arbitrary step function as long as we can prove that it terminates for all states.

import Mathlib.Tactic

def step (state: Nat): Option Nat :=
  if state = 0 then none else some (state - 1)

set_option linter.unusedVariables false in
def countdown (state: Nat) :=
  match h: step state with
  | none => [state]
  | some newState => state :: countdown newState
termination_by state
decreasing_by
  simp_wf
  simp [step] at h
  split_ifs at h
  simp at h
  omega

-- A very simple lemma
lemma initial_state (state: Nat): (countdown state).head (by unfold countdown; split <;> simp) = state := by
  unfold countdown
/- ⊢ (match h : step state with
      | none => [state]
      | some newState => state :: countdown newState).head
    ⋯ =
  state -/
  -- The conclusion looks very obvious at this point, but all simple tactics fail:
  -- simp       -- simp made no progress
  -- split      -- fails
  -- rcases h: step state    -- tactic 'generalize' failed, result is not type correct
  -- With a naive by_cases approach, the subsequent simp, rw, or simp_rw all fail.
  --  rw gives 'motive is not type correct'
  -- Instead, I have to write out the motive explicitly.

  let motive := fun x => (match h : x with
    | none => [state]
    | some newState => state :: countdown newState).head (by split <;> simp) = state
  by_cases h: step state = none
  · have: motive (step state) = motive none := by rw [h]
    simp [motive] at this
    exact this
  · sorry -- this case is similar after converting h to step state = some newState

[Kim Morrison]

How about

import Mathlib.Tactic

def step (state: Nat): Option Nat :=
  if state = 0 then none else some (state - 1)

set_option linter.unusedVariables false in
def countdown (state: Nat) :=
  match h: step state with
  | none => [state]
  | some newState => state :: countdown newState
termination_by state
decreasing_by sorry

lemma initial_state (state: Nat): (countdown state).head (by unfold countdown; split <;> simp) = state := by
  unfold countdown
  generalize_proofs p
  split at p <;> rfl

[Kim Morrison]

(Clue: all the incorrect motives must have been about the proof inside .head. So use generalize_proofs to get access to it directly.)

[Ted Hwa]

Thank you, that was really helpful in eliminating motives from several of my proofs. However, there are still some others which I couldn't eliminate. In the more difficult cases, the motive has to include an equality hypothesis because the statement to be proved would be false for an arbitrary x. Then I had to fall back on Eq.rec to use the motive. I don't have a minimized example yet.

[Kim Morrison]

Looking forward to seeing them! :-)

[Ted Hwa]

Ok, here's a reasonably minimized example.

import Mathlib.Tactic

def step (state: Nat): Option Nat :=
  if state = 0 then none else some (state - 1)

set_option linter.unusedVariables false in
def countdown (state: Nat) :=
  match h: step state with
  | none => [state]
  | some newState => state :: countdown newState
termination_by state
decreasing_by sorry

lemma tailLast (state: Nat):
    ∀ s ∈ countdown state,
      List.getLast (countdown state) (by sorry) =
       List.getLast (countdown s) (by sorry) := by sorry

lemma suffixEqualsCountdownOfHead {suffix: List Nat}
    (suffix_nonempty: suffix ≠ []) (state: Nat):
    suffix ∈ (countdown state).tails →
      suffix = countdown (suffix.head suffix_nonempty) := by sorry

lemma tailLastSuffix (state: Nat) (suffix: List Nat)
    (suffix_nonempty: suffix ≠ []) (suffix_in_tails: suffix ∈ (countdown state).tails):
    List.getLast (countdown state) (by sorry) =
     List.getLast suffix suffix_nonempty := by
  have foo := tailLast state (suffix.head suffix_nonempty)
  have foo2 := suffixEqualsCountdownOfHead suffix_nonempty state suffix_in_tails
  -- I want to do rw [foo2]. Here the equality hypothesis is needed in the motive
  -- because a general x could  be empty, then no proof is possible for x.getLast
  let motive := fun x (h2: countdown (suffix.head suffix_nonempty) = x) =>
    List.getLast (countdown state) (by sorry) =
      x.getLast (by rw [← h2]; unfold countdown; split <;> simp)
  have := @Eq.rec (motive := motive) (by
      simp [motive]
      apply foo
      sorry  -- rest of the proof is not relevant to this issue
    ) suffix foo2.symm
  exact this

[Ted Hwa]

Above code has been edited slightly to include the proof for x.getLast since that's important to the issue.

[Ted Hwa]

In my last example, if I do simp_rw [foo2] (on the line with the comment I want to do rw [foo2]), I get

tactic 'simp' failed, nested error:
maximum recursion depth has been reached

and after turning on diagnostics as suggested, I get the following output which I don't know how to interpret:

[simp] used theorems (max: 99, num: 1): ▼
  _uniq.680 ↦ 99
[simp] tried theorems (max: 99, num: 1): ▼
  _uniq.680 ↦ 99, succeeded: 99
[reduction] unfolded reducible declarations (max: 32, num: 1): ▼
  Ne ↦ 32

[Ted Hwa]

I found a solution. The following code replaces the code starting with the motive line. But I don't really understand why rw or simp_rw sometimes works and sometimes doesn't in these situations.

rw [← foo2] at foo
apply foo
sorry  -- rest of proof is same as the last `sorry` before

[Ted Hwa]

The initial generalize_proofs solution doesn't seem to work on the latest nightly build (mathlib nightly-testing-2024-06-05, lean nightly-2024-06-05). It works on 4.8.0.

import Mathlib.Tactic.GeneralizeProofs

def step (state: Nat): Option Nat :=
  if state = 0 then none else some (state - 1)

set_option linter.unusedVariables false in
def countdown (state: Nat) :=
  match h: step state with
  | none => [state]
  | some newState => state :: countdown newState
termination_by state
decreasing_by sorry

theorem initial_state (state: Nat): (countdown state).head (by unfold countdown; split <;> simp) = state := by
  unfold countdown
  generalize_proofs p
  split at p <;> rfl   -- works on 4.8.0 but on latest nightly, gives tactic 'splitMatch' failed, nested error: 'applyMatchSplitter' failed, failed to generalize target

[Ted Hwa]

Filed a bug at https://github.com/leanprover/lean4/issues/4390