Zulip Chat Archive

Stream: new members

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


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

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

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

view this post on Zulip Patrick Massot (Nov 16 2018 at 19:27):

This all about elaboration

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:29):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:31):

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

view this post on Zulip Mario Carneiro (Nov 16 2018 at 19:31):

apply needs to guess how many pis the result type has

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 16 2018 at 19:35):

That makes sense. Thanks.


Last updated: May 18 2021 at 17:44 UTC