Zulip Chat Archive

I'm now trying to prove example {r n : ℕ} {h1 : 1 ≤ r} {h2 : r ≤ n} : n - r + 1 = n - (r - 1). The tactics I know of and the things I can find in data.nat don't seem to be helping - what am I missing?

Chris Hughes (Nov 16 2019 at 23:51):

does the omega tactic work?

Chris Hughes (Nov 16 2019 at 23:51):

You need import tactic.omega

Chris Hughes (Nov 16 2019 at 23:52):

nat.sub_sub is the lemma you want. But in general omega should work.

Bhavik Mehta (Nov 16 2019 at 23:54):

nat.sub_sub doesn't do it - the parens don't match up correctly

Bhavik Mehta (Nov 16 2019 at 23:54):

But omega does it, thanks!

Mario Carneiro (Nov 16 2019 at 23:54):

This lemma seems to have escaped detection, even in algebra.group

Bhavik Mehta (Nov 16 2019 at 23:57):

omega does it in this example, but not in my actual proof - I've got a line of calc which looks like (a more complicated version of)

example {s : finset ℕ} {r n : ℕ} {h1 : 1 ≤ r} {h2 : r ≤ n} : finset.card s * nat.fact (n - r + 1) = finset.card s * nat.fact (n - (r - 1)) :=
by omega

and omega can't handle it

Mario Carneiro (Nov 16 2019 at 23:58):

theorem sub_sub_assoc_swap {α} [add_group α] (a b c : α) : a - (b - c) = a + c - b :=
by simp

theorem sub_sub_assoc {α} [add_comm_group α] (a b c : α) : a - (b - c) = a - b + c :=
by simp

theorem nat.sub_sub_assoc {a b c : ℕ} (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c :=
(nat.sub_eq_iff_eq_add (le_trans (nat.sub_le _ _) h₁)).2 $
by rw [add_right_comm, add_assoc, nat.sub_add_cancel h₂, nat.sub_add_cancel h₁]