## Stream: general

### Topic: Linarith unexpected failure

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

#### Yury G. Kudryashov (May 08 2020 at 21:24):

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

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

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

#### Yury G. Kudryashov (May 08 2020 at 21:51):

Then you need a better expert on Lean internals.

#### Kevin Buzzard (May 08 2020 at 21:57):

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

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


which works fine

#### 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, 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 (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

#### Bhavik Mehta (May 08 2020 at 22:03):

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

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


#### Kevin Buzzard (May 08 2020 at 22:04):

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

#### 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, 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 (May 08 2020 at 22:08):

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

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


#### Kevin Buzzard (May 08 2020 at 22:10):

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

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

#### Kevin Buzzard (May 08 2020 at 22:16):

Solinarith doesn't know that it's an inequality

#### Kevin Buzzard (May 08 2020 at 22:16):

@Mario Carneiro isfrom broken??

#### Kevin Buzzard (May 08 2020 at 22:17):

The first trace starts with a metavariable

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

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

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


which works fine

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

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

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

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

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

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

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

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