Simp not working inside a predicate

Stream: new members

[ROCKY KAMEN-RUBIO]

(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]

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]

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]

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]

ring

[ROCKY KAMEN-RUBIO]

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]

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

[Kevin Buzzard]

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