Linarith unexpected failure

Stream: general

[Frédéric Le Roux]

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!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Frédéric Le Roux]

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))

[Yury G. Kudryashov]

Then you need a better expert on Lean internals.

[Kevin Buzzard]

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

[Bhavik Mehta]

You can by the way change the linarith to:

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

which works fine

[Kevin Buzzard]

...
    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, hε], -- 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)

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Bhavik Mehta]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

    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, hε],

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Solinarith doesn't know that it's an inequality

[Kevin Buzzard]

@Mario Carneiro isfrom broken??

[Kevin Buzzard]

The first trace starts with a metavariable

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Jalex Stark]

Bhavik Mehta said:

You can by the way change the linarith to:

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

which works fine

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

[Reid Barton]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Frédéric Le Roux]

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!

[Reid Barton]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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