Zulip Chat Archive
Stream: general
Topic: example (x : ℕ) : ¬ (2 + x = 0) := sorry
Kevin Buzzard (Apr 04 2018 at 21:15):
It is forever taking me 3 lines to prove stuff like this. What's a slick way of doing this quickly?
Mario Carneiro (Apr 04 2018 at 21:17):
rw add_comm; apply succ_ne_zero
Kenny Lau (Apr 04 2018 at 22:19):
example (x : ℕ) : ¬ (2 + x = 0) := by cases x; apply nat.no_confusion
Kevin Buzzard (Apr 04 2018 at 22:19):
So you (Mario) decided to do it in tactic mode. Looking at this example I realise I didn't really understand what apply actually does.
Kenny Lau (Apr 04 2018 at 22:20):
oh hey our solutions have exactly the same length
Kevin Buzzard (Apr 04 2018 at 22:20):
he opened nat!
Kenny Lau (Apr 04 2018 at 22:20):
oh right
Kenny Lau (Apr 04 2018 at 22:20):
so i win
Kevin Buzzard (Apr 04 2018 at 22:20):
in some sense
Kevin Buzzard (Apr 04 2018 at 22:20):
He answered first
Kenny Lau (Apr 04 2018 at 22:20):
well i was sleeping
Kevin Buzzard (Apr 04 2018 at 22:20):
solutions aren't totally ordered
Kevin Buzzard (Apr 04 2018 at 22:20):
you always win if you get to choose the ordering
Kevin Buzzard (Apr 04 2018 at 22:21):
Let me think about Mario's solution.
Kenny Lau (Apr 04 2018 at 22:21):
apply [xxx], where [xxx] : A -> B -> C -> D attempts to match D with the goal, and set A, B, C as three new goals if necessary
Kevin Buzzard (Apr 04 2018 at 22:21):
x + 2 unfolds to x + bit0 1 which unfolds to x + (1 + 1)
Kevin Buzzard (Apr 04 2018 at 22:22):
and I can't match this with nat.succ anything
Kevin Buzzard (Apr 04 2018 at 22:22):
oh I have to unfold more
Kenny Lau (Apr 04 2018 at 22:22):
example (x : ℕ) : x + 2 = nat.succ (x + 1) := rfl
Kevin Buzzard (Apr 04 2018 at 22:22):
x + succ 1, succ (x + 1)
Kevin Buzzard (Apr 04 2018 at 22:22):
right
Kevin Buzzard (Apr 04 2018 at 22:23):
but there's still more to do
Kenny Lau (Apr 04 2018 at 22:23):
how so
Kevin Buzzard (Apr 04 2018 at 22:23):
because apply is not exact
Kevin Buzzard (Apr 04 2018 at 22:23):
and this is not exact
Kevin Buzzard (Apr 04 2018 at 22:24):
the goal is f(succ x) and we solve it with forall n, f(n)
Kenny Lau (Apr 04 2018 at 22:24):
example (x : ℕ) : ¬ (2 + x = 0) := by rw add_comm; exact nat.succ_ne_zero (x+1)
Kenny Lau (Apr 04 2018 at 22:24):
apply automatically fills out the arguments for you
Kevin Buzzard (Apr 04 2018 at 22:24):
I've seen it not automatically fill out the arguments for me
Kevin Buzzard (Apr 04 2018 at 22:24):
and I've had to use refine instead
Kenny Lau (Apr 04 2018 at 22:25):
well I can't say anything if you don't have an example
Kevin Buzzard (Apr 04 2018 at 22:25):
yeah and I can't read the definition of apply because it's in meta land
Kevin Buzzard (Apr 04 2018 at 22:26):
I guess I've sometimes tried to apply to partially close a goal and it's failed
Kevin Buzzard (Apr 04 2018 at 22:26):
I guess I just have to read the docstring more carefully.
Kenny Lau (Apr 04 2018 at 22:27):
/-- The `apply` tactic tries to match the current goal against the conclusion of the type of term. The argument term should be a term well-formed in the local context of the main goal. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones. The `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types. -/
Mario Carneiro (Apr 05 2018 at 01:26):
I used apply in that example simply as a shorthand for exact (or refine nonterminally), it saves me a few underscores at the end. It doesn't always work, but I think it works here.
Nicholas Scheel (Apr 05 2018 at 03:31):
what about rw add_comm; from dec_trivial?
Kenny Lau (Apr 05 2018 at 03:31):
does it work?
Nicholas Scheel (Apr 05 2018 at 03:32):
Kenny Lau (Apr 05 2018 at 03:33):
you win
Scott Morrison (Apr 05 2018 at 03:40):
simp; from dec_trivial
Kenny Lau (Apr 05 2018 at 03:40):
ok you win
Scott Morrison (Apr 05 2018 at 03:40):
Or import lean-tidy and: obviously.
Last updated: Dec 20 2023 at 11:08 UTC