## 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: May 08 2021 at 19:11 UTC