# Zulip Chat Archive

## Stream: new members

### Topic: Simp not working inside a predicate

#### ROCKY KAMEN-RUBIO (Apr 18 2020 at 19:28):

(From Kevin's first logic sheet). We're given that for some function P, P(n) implies P(n+8) and P(n-3). I am trying to show P(n) implies P(n+1) and P(n-1), which I call subgoals `h1`

and `h2`

respectively, so I can do integer induction. My problem is after applying +8 twice, and -3 five times, I'm left with `h : P (n + (8 + 8) - 3 - 3 - 3 - 3 - 3)`

instead of just `h : P(n+1)`

. This doesn't reduce even after applying `simp at h,`

. Am I misunderstanding how `simp`

works? Is there another tactic I should be using?

I'm also guessing there's an easier way to apply `h8`

and `h3 `

than my monstrocity. I was trying to get a rough working solution first. Don't judge me...

lemma question_5 (P : ℤ → Prop) (h8 : ∀ n, P n → P (n + 8)) (h3 : ∀ n, P n → P (n - 3)) : (∀ n, P n) ∨ (∀ n, ¬ (P n)) := begin have h1 : ∀ n : ℤ, (P n) → (P (n+1)), intro n, intro hPn, have h := h3 (n+8+8-3-3-3-3) (h3 (n+8+8-3-3-3) (h3 (n+8+8-3-3) (h3 (n+8+8-3) (h3 (n+8+8) (h8 (n + 8) (h8 n hPn)))))), simp at h, have h2 : ∀ n : ℤ, (P n) → (P (n-1)), --intro n, intro hPn, end

#### Reid Barton (Apr 18 2020 at 19:33):

You can simplify your problem for yourself. Does `simp`

prove `n + (8 + 8) - 3 - 3 - 3 - 3 - 3 = n + 1`

? If so then you can use this as a first step. If not then the issue has nothing to do with `P`

, right?

#### Kevin Buzzard (Apr 18 2020 at 20:25):

If you just think that simp is a magic tactic that solves all simple goals then yes you're very much misunderstanding how it works. I should note that I spent about the first year of my Lean life also thinking this.

#### ROCKY KAMEN-RUBIO (Apr 18 2020 at 20:29):

I'm seeing now that it looks like integer tactics don't behave the same as nat tactics (unless I'm doing something wrong). For example, `Simp`

would be able to do this for `n : \N `

but it won't for `n:\Z`

. Going through the mathlib documentation for `int`

I'm not seeing anything like `add_left_cancel`

. Any advice for how to get up to speed on integers? A lot of the documentation is going over my head and seems unnecessary for what I'm trying to do.

theorem test (n : ℕ) : n + (8 + 8) - 3 - 3 - 3 - 3 - 3 = n + 1 := begin simp, end theorem test' (n : ℤ) : n + (8 + 8) - 3 - 3 - 3 - 3 - 3 = n + 1 := begin simp, end

#### Kenny Lau (Apr 18 2020 at 20:35):

`ring`

#### ROCKY KAMEN-RUBIO (Apr 18 2020 at 22:47):

Kenny Lau said:

`ring`

This worked (after I stared at an error for 10 minutes and then realized I forgot to `import tactic`

). Thanks!

#### Kevin Buzzard (Apr 18 2020 at 23:17):

Ha ha the error when you type ring without the import is spectacular, because ring also means something else.

#### Kevin Buzzard (Apr 18 2020 at 23:17):

It's like "what is a ring? You're not a tactic"

Last updated: Dec 20 2023 at 11:08 UTC