Exact same proof works in term mode but not tactic

Stream: new members

[Abhimanyu Pallavi Sudhir]

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]

Oh, and this works:

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

[Abhimanyu Pallavi Sudhir]

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]

This all about elaboration

[Patrick Massot]

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]

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

[Abhimanyu Pallavi Sudhir]

Ah yes, it seems apply @abs_of_pos ℝ _ 2 (two_pos) works too.

[Abhimanyu Pallavi Sudhir]

But how does that explain exact working where apply doesn't?

[Mario Carneiro]

apply needs to guess how many pis the result type has

[Mario Carneiro]

apply x is basically the same as refine x _ _ _ where the number of underscores depends on the type of x

[Mario Carneiro]

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]

That makes sense. Thanks.