Zulip Chat Archive

Stream: general

Topic: Linarith unexpected failure


view this post on Zulip Frédéric Le Roux (May 08 2020 at 21:14):

A very strange thing is happening here:

https://github.com/FredericLeRoux/LEAN_ESPACES_METRIQUES/blob/master/esp_metrique.lean#L96

The current proof ends with linarith, and it works. But then let's replace line 96,
have clef : d x z ≤ d x y + d y z, from triangle x y z
with the less explicit
have clef, from triangle x y z
Lean's answer to this line does not change, as expected. So the context at line 96, after this change, seems to be as before.
But now the linarith tactic at the next line fails!

view this post on Zulip Yury G. Kudryashov (May 08 2020 at 21:24):

Did you try looking at this with set_option pp.all true?

view this post on Zulip Yury G. Kudryashov (May 08 2020 at 21:25):

Probably it adds dist x z ≤ dist x y + dist y z with a metavariable instead of an instance for metric_space.

view this post on Zulip Frédéric Le Roux (May 08 2020 at 21:49):

So I tried pp.all. Both lines give exactly the same result:
clef : @has_le.le.{0} real real.has_le (@espace_metrique.dist X _inst_1 x z) (@has_add.add.{0} real (@distrib.to_has_add.{0} real (@ring.to_distrib.{0} real real.ring)) (@espace_metrique.dist X _inst_1 x y) (@espace_metrique.dist X _inst_1 y z))
clef2 : @has_le.le.{0} real real.has_le (@espace_metrique.dist X _inst_1 x z) (@has_add.add.{0} real (@distrib.to_has_add.{0} real (@ring.to_distrib.{0} real real.ring)) (@espace_metrique.dist X _inst_1 x y) (@espace_metrique.dist X _inst_1 y z))

view this post on Zulip Yury G. Kudryashov (May 08 2020 at 21:51):

Then you need a better expert on Lean internals.

view this post on Zulip Kevin Buzzard (May 08 2020 at 21:57):

have clef := triangle x y z, works, but have clef, from triangle x y z, fails

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:00):

You can by the way change the linarith to:

    linarith only [triangle x y z, z_in, y_in, ] }

which works fine

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:00):

...
    have clef, from triangle x y z,
    have clef2 := triangle x y z,
    have h : clef = clef2 := rfl,
--    linarith only [clef, z_in, y_in, hε], -- fails!
    linarith only [clef2, z_in, y_in, ], -- works
...

This is surprising (to me). With pp.all on true, clef and clef2 are identical (indeed the prettyprinter is telling me they have the same type)

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:02):

I think the rfl is doing some simplifications/unfolding to prove the equality, but linarith doesn't perform these; and the clef (in Kevin's code) has something folded differently to what the linarith wants

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:03):

And this also explains why pp.all thinks the terms are the same

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:03):

clef clef2 : d x z ≤ d x y + d y z,
h : clef = clef2
⊢ d x z < r

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:04):

Where's that Mario super-pp-all code?

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:05):

...
    have clef, from triangle x y z,
    simp only [] at clef,
    linarith only [clef, z_in, y_in, ]}
...

works as well, showing that there is something to simplify in the term, and it's this simplification that makes it work

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:08):

ha ha! I think it's the same issue as the one I found a few days ago!

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:09):

    have clef, from triangle x y z,
    have clef2 := triangle x y z,
    have h : clef = clef2 := rfl,
    (do t  tactic.to_expr```(clef) >>= tactic.infer_type,
      tactic.trace (expr.to_raw_fmt t)),
    (do t  tactic.to_expr```(clef2) >>= tactic.infer_type,
      tactic.trace (expr.to_raw_fmt t)),
--    linarith only [clef, z_in, y_in, hε],
    linarith only [clef2, z_in, y_in, ],

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:10):

clef has some metavariable in it which pp.all can't see

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:13):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/rw.3A.20equality.20is.20not.20an.20equality/near/196693213

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:16):

Solinarith doesn't know that it's an inequality

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:16):

@Mario Carneiro isfrom broken??

view this post on Zulip Kevin Buzzard (May 08 2020 at 22:17):

The first trace starts with a metavariable

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:17):

I think the have clef, from pattern might just be a bad idea: we're naming something without giving its type at all

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:18):

which I'm distinguishing from have clef := triangle x y z since in this one the type can be inferred

view this post on Zulip Jalex Stark (May 08 2020 at 22:38):

Bhavik Mehta said:

You can by the way change the linarith to:

    linarith only [triangle x y z, z_in, y_in, ] }

which works fine

did you guess this or did it come from something like linarith? ?

view this post on Zulip Reid Barton (May 08 2020 at 22:39):

Is it possible to write a zonk tactic which instantiates all metavariables that have been assigned everywhere?

view this post on Zulip Reid Barton (May 08 2020 at 22:40):

I'm glad to finally understand this situation where pp.all prints two identical types but they behave differently for some tactics

view this post on Zulip Bhavik Mehta (May 08 2020 at 22:40):

have clef := triangle x y z, linarith [clef, ...] worked so I presumed linarith [triangle x y z, ...] should work too

view this post on Zulip Frédéric Le Roux (May 09 2020 at 13:46):

Indeed, expr.to_raw_fmt tgives (mvar _mlocal._fresh.880.289587 _mlocal._fresh.880.289587 (const 2 []))when applied on the bad version of clef. I am happy with have clef := triangle x y z, but that's frightening!

view this post on Zulip Reid Barton (May 09 2020 at 13:48):

I guess I'm also a bit confused because in GHC I thought zonking was a performance optimization--suggesting that the difference between an assigned metavariable and its definition should somehow be invisible to everything.

view this post on Zulip Mario Carneiro (May 09 2020 at 14:04):

it is definitely supposed to be invisible to everything, but expr is a type in lean, with distinct constructors for mvar and other things, so it's tough to make it actually invisible to pure code

view this post on Zulip Mario Carneiro (May 09 2020 at 14:06):

e.g. if I have an unassigned mvar, store it somewhere, then the mvar gets assigned, and I recheck my store, it had better still be an mvar because otherwise it wouldn't be a pure function, yet it is nevertheless an assigned mvar


Last updated: May 14 2021 at 06:16 UTC