1
$\begingroup$

I am trying to prove the following theorem:

theorem list_take_take (n n: Nat) (xs: List α):
  take n (take m xs) = take (min n m) xs := by
  revert m xs
  induction n with
  | zero =>
    intro m xs
    rw [nat_min_zero]
    repeat rw [take]
  | succ n ihn =>
    intro m xs
    cases m with
    | zero =>
      rw [take, min]
      simp
      rw [take]
      apply list_take_nil
    | succ m =>
      unfold min
      split
      · -- case: succ n ≤ succ m
        -- how do I rewrite succ n ≤ succ m to n ≤ m
        -- using Nat.succ_le_succ or Nat.le_of_succ_le_succ?
        sorry
      · sorry

When I get to the split tactic, it splits the if statement that resulted from unfolding the min function, but the new hypothesis succ n ≤ succ m has no name, so I can't rewrite it to n ≤ m. Is there a way to name the hypothesis that will result from using the split tactic or is there another way to do cases on the comparison?

Note: this question is about Lean4 and not Lean3

$\endgroup$

1 Answer 1

1
$\begingroup$

In the tactic state you can see which case you are looking at

Tactic state
case succ.succ.inl
α: Type u_1
n✝n: Nat
ihn: ∀ {m : Nat} (xs : List α), take n (take m xs) = take (min n m) xs
xs: List α
m: Nat
: succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs

You can use this to add a case clause after the split

unfold min
split
· case succ.succ.inl h =>

This will result in the comparison hypothesis being named as h:

α: Type u_1
n✝n: Nat
ihn: ∀ {m : Nat} (xs : List α), take n (take m xs) = take (min n m) xs
xs: List α
m: Nat
h: succ n ≤ succ m
⊢ take (succ n) (take (succ m) xs) = take (succ n) xs
$\endgroup$
2
  • 1
    $\begingroup$ · is an anonymous case, you don't need both $\endgroup$ Mar 7, 2023 at 10:50
  • $\begingroup$ Even better, thank you :) ``` unfold min split case succ.succ.inl h => rw [nat_succ_le_succ_iff] at h ``` $\endgroup$ Mar 7, 2023 at 15:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.