Zulip Chat Archive

What's the easiest tactic to turn something of type succ (n-1) into n where n is a natural number and the hypothesis n>0 is in the proof environment? I would prefer just a single tactic rather that some sequence of cancellations etc.

Ruben Van de Velde (Dec 23 2023 at 07:17):

Maybe simp [n_ne_zero] will do it? It seems pretty specific to get its own tactic

Andy Jiang (Dec 23 2023 at 07:27):

Hmmm, I guess I have a more generic question actually. do these tactics only work inside like a by ... clause? Like if I am applying some function inline, and the second argument of the function has some type, can I use simp to get that object? In other words is it possible to apply a function f to x and specify x with a tactic? or do I have to have some different environment like a by clause to use tactics. Hope this question makes sense. Like I would like a way to conjure an element of some type by saying the type and saying by some tactic we should have this element but inline if possible.

Mario Carneiro (Dec 23 2023 at 07:35):

by tac is a term, you can put it anywhere a term is expected

Andy Jiang (Dec 23 2023 at 07:43):

Thank you guys. I think now I understand it conceptually better. Although I am still struggling at something very basic I think. I tried using simp but it has failed. The precise situation I'm in is described by the error message below. Sorry for the troubles but I can't seem to find a tactic that can resolve this situation easily. simp was not really working for some reason. Can you guys confirm that simp is supposed to be able to work in this situation?

unsolved goals
n : ℕ
h✝ : length (sorted_divisors n) > 0
divs : List ℕ := sorted_divisors n
i : Fin (length divs - 1)
h : ↑i < length divs - 1 := sorryAx (↑i < length divs - 1) true
⊢ ↑i + 1 < length (sorted_divisors n)Lean 4

Mario Carneiro (Dec 23 2023 at 07:51):

no, that's not a goal for simp

Mario Carneiro (Dec 23 2023 at 07:53):

the recently landed omega should be able to handle it, maybe linarith if it's not available yet, and if that doesn't work you just have to use the theorem which will be named something like docs#Nat.add_lt_of_lt_sub

Andy Jiang (Dec 23 2023 at 07:57):

aha so simp is used to simplify like each side of an inequality but never across the inequality sign i'm taking as the takeaway?

Mario Carneiro (Dec 23 2023 at 07:58):

no it can simplify inequalities but it mostly only applies eq and iff statements. If you use the iff version of add_lt_of_lt_sub then simp will be able to rewrite the goal

Mario Carneiro (Dec 23 2023 at 07:59):

but it won't be a simp lemma by default because the result isn't really simpler

Andy Jiang (Dec 23 2023 at 08:02):

ah ok thanks! And omega worked!

Terence Tao (Dec 23 2023 at 23:24):

Andy Jiang said:

ah ok thanks! And omega worked!

Perhaps moot now that omega exists, but zify followed by ring (or abel) tends to work pretty well also, e.g.,

import Mathlib

example (n: ℕ) (hn: n > 0) : Nat.succ (n-1) = n := by
  zify [hn]; ring

Matt Diamond (Dec 23 2023 at 23:32):

FYI, for the specific case of Nat.succ (n - 1) = n, you can also just do this:

import Mathlib

example (n: ℕ) (hn: n > 0) : Nat.succ (n-1) = n := Nat.succ_pred hn.ne'

(sorry if this is obvious)

Last updated: May 02 2025 at 03:31 UTC

leanprover-community / mathlib