Zulip Chat Archive

Stream: new members

Topic: Simp not working inside a predicate


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 18 2020 at 20:35):

ring

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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