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