# Zulip Chat Archive

## Stream: new members

### Topic: Exact same proof works in term mode but not tactic

#### Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:05):

This works:

import data.real.basic lemma DUH : abs (2 : ℝ) = (2 : ℝ) := abs_of_pos two_pos

This works:

import data.real.basic lemma DUH : abs (2 : ℝ) = (2 : ℝ) := begin apply abs_of_pos, exact two_pos end

This doesn't work:

import data.real.basic lemma DUH : abs (2 : ℝ) = (2 : ℝ) := begin apply abs_of_pos (two_pos) end

This doesn't work:

import data.real.basic lemma DUH : abs (2 : ℝ) = (2 : ℝ) := begin apply @abs_of_pos _ _ 2 (two_pos) end

This works:

lemma DUH : abs (2 : ℝ) = (2 : ℝ) := begin rw abs_of_pos, exact two_pos end

This doesn't work:

lemma DUH : abs (2 : ℝ) = (2 : ℝ) := begin rw abs_of_pos (two_pos) end

Why? What's going on?

#### Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:07):

Oh, and this works:

import data.real.basic lemma DUH : abs (2 : ℝ) = (2 : ℝ) := begin exact abs_of_pos (two_pos) end

#### Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:09):

I can understand there may be some "metavariables make things weird" explanation for `exact`

working where `apply`

doesn't, but I really don't get why the two rewrites have different results.

#### Patrick Massot (Nov 16 2018 at 19:27):

This all about elaboration

#### Patrick Massot (Nov 16 2018 at 19:28):

The elaborator needs to guess the type of 2 in 2 > 0 (which is the statement of `two_pos`

). When it tries to do that too early this fails

#### Patrick Massot (Nov 16 2018 at 19:28):

You could probably save all attempts by type ascribing this two_pos using `(two_pos : (2 : R) > 0)`

#### Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:29):

Ah yes, it seems `apply @abs_of_pos ℝ _ 2 (two_pos)`

works too.

#### Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:31):

But how does that explain `exact`

working where `apply`

doesn't?

#### Mario Carneiro (Nov 16 2018 at 19:31):

apply needs to guess how many pis the result type has

#### Mario Carneiro (Nov 16 2018 at 19:32):

`apply x`

is basically the same as `refine x _ _ _`

where the number of underscores depends on the type of `x`

#### Mario Carneiro (Nov 16 2018 at 19:33):

This means that when elaborating `x`

we don't know what type it is yet, while with `refine`

or `exact`

we know the type of `x`

is the type of the goal

#### Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:35):

That makes sense. Thanks.

Last updated: May 18 2021 at 17:44 UTC