1
$\begingroup$

The theorem pred_le_pred is proven in prelude.lean using pattern matching:

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m)
  | _,           _, Nat.le.refl   => Nat.le.refl
  | 0,      succ _, Nat.le.step h => h
  | succ _, succ _, Nat.le.step h => Nat.le_trans (le_succ _) h

I was wondering if there is a way to also prove it using tactics?

Note: this question is about Lean4 and not Lean3

$\endgroup$
3
  • 1
    $\begingroup$ It's not necessary to include the prover in the title, because people can see it in the tags, and this saves up more space to display more important parts of your title :) $\endgroup$
    – Trebor
    Mar 7, 2023 at 9:15
  • $\begingroup$ It's always possible to prove term-mode things using tactics; exact <the_term> for one example. You should look into the cases tactic, which may be closer to what you want. $\endgroup$ Mar 7, 2023 at 10:56
  • $\begingroup$ Yes I can use exact, but I would like to know how to try different tactics as I am trying to reason and figure out how to prove this theorem. I have tried cases and induction without success. $\endgroup$ Mar 7, 2023 at 15:29

1 Answer 1

3
$\begingroup$

You can use the intro tactic and a match expression to prove the theorem:

namespace Hidden
open Nat

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m) := by
  intro n m h
  match n, m, h with
  | _,           _, Nat.le.refl   => exact Nat.le.refl
  | 0,      succ _, Nat.le.step h => exact h
  | succ _, succ _, Nat.le.step h => exact Nat.le_trans (le_succ _) h

end Hidden

Edit: I've come up with another proof:

namespace Hidden
open Nat

theorem Nat.pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m) := by
  intro n m h
  cases h
  . exact le.refl
  . rename_i m₁ h₁
    cases n
    . exact h₁
    . rename_i n₁
      exact Nat.le_trans (le_succ n₁) h₁

end Hidden
$\endgroup$
3
  • $\begingroup$ What I want to know is how to do with without any expressions and only using tactics, since it is hard to partially prove things using expressions. $\endgroup$ Mar 7, 2023 at 15:28
  • 1
    $\begingroup$ @WalterSchulze I've just added another proof to my answer. $\endgroup$
    – Bulhwi Cha
    Mar 8, 2023 at 5:28
  • $\begingroup$ Amazing yes thank you. The key was to do cases on n ≤ m $\endgroup$ Mar 8, 2023 at 11:28

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.