Zulip Chat Archive

Stream: general

Topic: example (x : ℕ) : ¬ (2 + x = 0) := sorry


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

view this post on Zulip Mario Carneiro (Apr 04 2018 at 21:17):

rw add_comm; apply succ_ne_zero

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:19):

example (x : ℕ) : ¬ (2 + x = 0) :=
by cases x; apply nat.no_confusion

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

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:20):

oh hey our solutions have exactly the same length

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:20):

he opened nat!

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:20):

oh right

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:20):

so i win

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:20):

in some sense

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:20):

He answered first

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:20):

well i was sleeping

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:20):

solutions aren't totally ordered

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:20):

you always win if you get to choose the ordering

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:21):

Let me think about Mario's solution.

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:21):

x + 2 unfolds to x + bit0 1 which unfolds to x + (1 + 1)

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:22):

and I can't match this with nat.succ anything

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:22):

oh I have to unfold more

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:22):

example (x : ℕ) : x + 2 = nat.succ (x + 1) := rfl

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:22):

x + succ 1, succ (x + 1)

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:22):

right

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:23):

but there's still more to do

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:23):

how so

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:23):

because apply is not exact

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:23):

and this is not exact

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:24):

the goal is f(succ x) and we solve it with forall n, f(n)

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:24):

example (x : ℕ) : ¬ (2 + x = 0) :=
by rw add_comm; exact nat.succ_ne_zero (x+1)

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:24):

apply automatically fills out the arguments for you

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:24):

I've seen it not automatically fill out the arguments for me

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:24):

and I've had to use refine instead

view this post on Zulip Kenny Lau (Apr 04 2018 at 22:25):

well I can't say anything if you don't have an example

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:25):

yeah and I can't read the definition of apply because it's in meta land

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 22:26):

I guess I just have to read the docstring more carefully.

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

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

view this post on Zulip Nicholas Scheel (Apr 05 2018 at 03:31):

what about rw add_comm; from dec_trivial?

view this post on Zulip Kenny Lau (Apr 05 2018 at 03:31):

does it work?

view this post on Zulip Nicholas Scheel (Apr 05 2018 at 03:32):

https://leanprover.github.io/live/latest/#code=variable%20x%20:%20nat%0A%0Aexample%20:%20%C2%AC%20(2%20+%20x%20=%200)%20:=%20by%20rw%20add_comm;%20from%20dec_trivial

view this post on Zulip Kenny Lau (Apr 05 2018 at 03:33):

you win

view this post on Zulip Scott Morrison (Apr 05 2018 at 03:40):

simp; from dec_trivial

view this post on Zulip Kenny Lau (Apr 05 2018 at 03:40):

ok you win

view this post on Zulip Scott Morrison (Apr 05 2018 at 03:40):

Or import lean-tidy and: obviously.


Last updated: May 18 2021 at 15:14 UTC