## 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

he opened nat!

oh right

so i win

in some sense

#### 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)

right

#### Kevin Buzzard (Apr 04 2018 at 22:23):

but there's still more to do

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

#### 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?

does it work?

you win

#### Scott Morrison (Apr 05 2018 at 03:40):

simp; from dec_trivial

ok you win

#### Scott Morrison (Apr 05 2018 at 03:40):

Or import lean-tidy and: obviously.

Last updated: May 18 2021 at 15:14 UTC