modes

Stream: general

[Kevin Buzzard]

So what are these "modes"? Johannes talked about smt mode and conv mode. Do mathematician end users need to know about these modes yet? I have used a conv tactic -- is that related to conv mode? My understanding of these things is still very hazy. Is there any advice for making it better other than "look through the libraries and try to spot stuff"?

[Mario Carneiro]

As you may have noticed, the conv tactic isn't really a self-contained tactic; it ends with a tactic block and you have to put other tactics in it. Inside that block, proof states look a little different and there are a different set of available tactics. That is a mode

[Kevin Buzzard]

Can I hang out in conv mode like I hang out in what I call "tactic mode"? Is that the correct name for that mode? The place where I can access tactic.interactive stuff?

[Sebastian Ullrich]

Yes, in mode $m you have access to tactics from namespace $m.interactive

[Sebastian Ullrich]

It doesn't make sense to enter conv mode without using conv, but you can e.g. enter smt mode using begin [smt] ... end

[Moses Schönfinkel]

Are we getting any closer to getting something like omega in [smt]?

[Kevin Buzzard]

example : 2 + 2 = 4 := begin
  conv in (2 + 2 = 4) {
   -- wooah I'm in conv mode
   -- there is no turnstile!
   -- goal is
   -- | 2 + 2 = 4
   -- what do I do now?
  }
end

[Kevin Buzzard]

Yay! I can't unfold +! I can't do anything!

[Kevin Buzzard]

Is it init/meta/converter/interactive.lean I'm supposed to be looking at? (converter not conv)

[Gabriel Ebner]

Yes.

[Gabriel Ebner]

The idea is that the pipe shows you the current term that you rewrite.

[Gabriel Ebner]

Try to_lhs, and you get to the left side of the equation.

[Patrick Massot]

Almost each time I try conv it tells me it can't find the pattern

[Gabriel Ebner]

If you do whnf, you convert the current subterm to WHNF.

[Patrick Massot]

even if the pattern is _

[Gabriel Ebner]

I feel it's pretty buggy.

[Patrick Massot]

Usually I wish I could use it to rewrite under a lambda

[Patrick Massot]

But it very rarely succeeds

[Kevin Buzzard]

Isn't that exactly what it's for?

[Gabriel Ebner]

Something like this?

example : (λ x : ℕ, 0+x) = (λ x, x) :=
begin
  conv { to_lhs, funext, rw ← nat.zero_add x },
end

[Kevin Buzzard]

example : 2 + 2 = 4 := begin
  conv in (2 + 2) {
    whnf,
  },
  conv in (4) {
    whnf,
  },
end

[Kevin Buzzard]

When I leave conv mode it closes a goal of the form x=x?

[Gabriel Ebner]

Yes, it tries reflexivity and triv.

[Patrick Massot]

I didn't know you could enter conv mode without in pattern

[Gabriel Ebner]

in just navigates to the specified subterm. Otherwise you start at the top.

[Kevin Buzzard]

I didn't know you could enter conv mode without in pattern

You learn about these things in the "modes" topic.

[Patrick Massot]

What are the navigating commands inside conv mode? I see you wrote to_lhs

[Patrick Massot]

That converter/interactive.lean could have a bit more docstrings...

[Gabriel Ebner]

There's also congr, which opens subgoals for all* arguments of the current term.
*Well, whatever you can reach via congruence lemmas.

[Patrick Massot]

I don't understand what that means

[Patrick Massot]

What is a "goal for an argument"?

[Gabriel Ebner]

Step through this example:

example : 2 + 1 = 5 := begin
  conv {
    to_lhs,
    congr,
  },
end

After to_lhs, you have one goal | 2+2. If you then invoke congr you get two goals, | 2 for the first argument of +, and | 1 for the second argument.

[Patrick Massot]

Ok, maybe the word "goal" is misleading here

[Patrick Massot]

You mean branch the navigation to navigate to all arguments, right?

[Gabriel Ebner]

I guess you could say that.

[Gabriel Ebner]

Under the hood each of the branches is represented as a goal in the tactic state (e.g. as 2 = ?m_1), that's where I got the notation from.

[Patrick Massot]

After navigating to a subterm, what can you do besides rewrite and whnf?

[Patrick Massot]

And if I arrive using congr at two goals but I want to act only on one, how can I leave some subterm unchanged?

[Mario Carneiro]

It occurs to me that norm_num and ring should probably be available as conv tactics

[Mario Carneiro]

Maybe "target" is a better term than "goal" in the conv monad

[Patrick Massot]

Indeed target sounds less confusing to me

[Patrick Massot]

And ring and norm_num would probably be useful here

[Kevin Buzzard]

I was going to try to figure out smt now

[Kevin Buzzard]

but I just got an email from Leo via github...

[Kevin Buzzard]

https://github.com/leanprover/lean/issues/1940#issuecomment-370014241

[Patrick Massot]

Yeah the B⃫DFL says we shouldn't use that

[Patrick Massot]

This is really mysterious to me. I thought Leo came from the SMT world and wanted to bridge the gap between automated stuff and proofs assistants

[Gabriel Ebner]

I think Leo has drawn conclusions from his experience with Z3 and SMT in general. He believes that users are often encoding straightforward problems in very roundabout ways just because they want to fit it into the language of SMT. This is not the best way to solve these problems. I remember two stories that he kept telling:

[Gabriel Ebner]

1) Somebody was using Z3 to solve physics problems. They took measurements using a camera and (I think) gave equations to Z3 that constrained the position of an object. However they formulated them as a problem in real arithmetic, which is somewhat expensive to decide. Inexact numeric methods would have been a better choice here. (Ok, this story doesn't really say anything against SMT in Lean..)

[Scott Morrison]

(and of course the problem with these stories is that failures get blamed on the back-end, not the user's choice of encoding, I guess)

[Gabriel Ebner]

2) The dependently-typed language F* uses Z3 to discharge verification conditions. They have a wonderful paper on how to write an evaluator using e-matching. (see http://hatt2016.inria.fr/program/) Essentially, they output several megabytes of essentially first-order formulas just so that Z3 evaluates an expression like simp would.

[Gabriel Ebner]

This one is more my own impression: SMT solvers (and theorem provers in general) have quite a bit of heuristics built-in so that they can handle many problems. However, just going by heuristics is often brittle. For example, Z3 has its own tactics language to specify the global proof search strategy. https://link.springer.com/chapter/10.1007/978-3-642-36675-8_2 I think Leo wants to do something like this in Lean. That is, the automated theorem should not do any case-splits, other non-deterministic, or potentially expensive reasoning by default. Instead the user should explicitly specify the expensive steps using tactics. This approach could be less brittle and more performant than heuristic strategies.

[Gabriel Ebner]

This was also pretty much his answer when I asked him, "why doesn't Lean have the SAT part of SMT?" He seems to have a bit of bad experience with unreliable proofs in Z3.

[Patrick Massot]

What about all these answers like "smt will do that, so let's not try something else" when Coq people asked for omega or other automatic tactics?

[Moses Schönfinkel]

It will do that once it's in a state where users can specify the expensive steps, I guess :)?

[Moses Schönfinkel]

Either way, thank you very much for the insight @Gabriel Ebner .

[Patrick Massot]

Yes, thanks for all your explanations today

[Gabriel Ebner]

I don't know what discussion happened about omega. I think Leo wants to have omega in the long-term future, but it's not blocking anything right now and it's not scientifically interesting either. At that point, omega will probably work in SMT mode (if it still exists). BTW, you can lift any tactic to SMT, so you could use ring as omega--.

[Gabriel Ebner]

@Mario Carneiro said he wanted to do omega in summer, but I'm not sure what came of that.

[Patrick Massot]

When I'll have more time I'll try to write everything I understood about conv (from today's explanations and earlier examples) so that won't be totally lost

[Patrick Massot]

I don't really know what omega is meant to do but it seem to help with computation. And computations are really the most inconvenient part of Lean I've seen

[Gabriel Ebner]

It decides linear integer arithmetic (Presburger arithmetic), but only in one of the versions of natural numbers and integers in the Coq standard library. (They have quite a few versions...)

[Patrick Massot]

Ok, it seems less crucial than ring and field (or a version for vector space that would be really awesome)

[Moses Schönfinkel]

Not the case when you're certifying software! :)

[Patrick Massot]

I see. But remember Lean is mathematics friendly (doesn't care too much about constructivism, has documentation mentioning theorem in the title and not referring to Haskell or ML at every page etc...)

[Andrew Ashworth]

I see. But remember Lean is mathematics friendly (doesn't care too much about constructivism, has documentation mentioning theorem in the title and not referring to Haskell or ML at every page etc...)

I think you might be confusing Jeremy and his CMU group with Leo :) That Lean is useful for mathematicians is a happy side-effect of Lean being useful for certifying software.

[Sebastian Ullrich]

I believe there is a bad bug in conv that makes it fail with "failed to match pattern" if the conv tactic block fails... I never fixed it because I don't really use it

[Patrick Massot]

That explains everything I saw when trying conv! Should I open an issue then? Or it enough to :pray: here?

[Mario Carneiro]

Best stick to prayer. Gabriel and Sebastian are the only ones in a position to fix this if they wish, and they read this chat so consider them informed. Leo isn't going to do anything about "misleading error messages", so reporting it is just counterproductive these days.

[Kevin Buzzard]

That explains everything I saw when trying conv! Should I open an issue then? Or it enough to :pray: here?

I guess I have had the same experience with conv as Patrick -- it has failed for me in exactly the same way (but in contrast to Sebastian I, probably like Patrick, just assumed it was me that was at fault). It's nice to be aware of the bug but now I realise that one can use it in interactive mode I feel like I have a good workaround.

[Simon Hudon]

Are error messages something that could be fixed with patches from the community? I mean maybe we could learn to fix it ourselves and just submit those changes.

[Kevin Buzzard]

I just think he wants everyone to leave him alone.

[Kevin Buzzard]

And my impression is that we're doing that quite well recently. I've certainly sat on a couple of minor things rather than reporting trivial bugs

[Patrick Massot]

Of course I also assumed it was my fault, especially since I understood very little of what conv was meant to do. I agree that knowing existence of this bug should be enough to mostly avoid it. But it would still be much nicer if @Sebastian Ullrich could fix it.

[Patrick Massot]

Yes, it tries reflexivity and triv.

[in the above quote, "it" refers to Lean when closing a conv block]

[Patrick Massot]

Not quite

[Patrick Massot]

It tries to close the goal when it really becomes x = x, not x' = x with x' defeq x

[Patrick Massot]

example (a : ℕ) : a * a = a * a :=
begin
conv { to_lhs, whnf },
trivial
end

wouldn't work without that trivial (or refl)

[Patrick Massot]

When I'll have more time I'll try to write everything I understood about conv (from today's explanations and earlier examples) so that won't be totally lost

see https://github.com/PatrickMassot/mathlib/blob/docs-conv/docs/extras/conv.md

[Patrick Massot]

I opened a WIP PR at https://github.com/leanprover/mathlib/pull/73 so that people can add comments in a Github review

[Patrick Massot]

Of course I'd like @Gabriel Ebner to check what I wrote. But I would also like to read comments from people who don't know much about this converter mode.

[Kevin Buzzard]

That looks fine to me. Somehow conv looks much easier to use now I realise I can use it interactively.

[Patrick Massot]

Exactly: once explained, this is easy. The trap is to conclude this doesn't need documentation

[Patrick Massot]

To be fair, the documentation is the change log was already very efficient. Without the pattern matching bug (now promoted "well known documented bug") it may have been enough to figure it out without Gabriel's help.

[Patrick Massot]

Quick poll: @Sebastian Ullrich what do you think the abbreviation convstands for?

[Sebastian Ullrich]

convolution, obviously

[Patrick Massot]

:smile: Please answer seriously (unless you already saw the discussion about it on Github)

[Kevin Buzzard]

Patrick is trying to figure out if it's conversion or converter

[Kevin Buzzard]

for the docs

[Patrick Massot]

Convolution always make great jokes. When I was a third student, my algebra teacher asked the audience "do you know a commutative ring without unit?". After some silence, someone answered: "integrable functions on R with usual addition and the convolution product". The algebra teacher turned slightly green and, after a few seconds, recovered and told us: "what about even integers?".

[Kevin Buzzard]

even integers are a pathological example

[Kevin Buzzard]

the first one comes up in the real world

[Kevin Buzzard]

it works for the p-adics too

[Patrick Massot]

I think he only wanted to emphasize why ideals are not subrings (knowing that we agreed rings have a unit)

[Sebastian Ullrich]

I did see the Github thread already, unfortunately. I have no strong feelings in either direction.

[Patrick Massot]

And the teacher was http://www.mathematik.uni-stuttgart.de/~geckmf/ I don't think he sees convolution products in the real world

[Moses Schönfinkel]

You've missed an excellent bikeshedding opportunity.

[Kevin Buzzard]

Given the choice between some tedious assertion violation or the chance to weigh in on what conv actually means, I'm surprised he didn't take the bait!

[Patrick Massot]

He is a wise guy. He saw God already decided.

[Patrick Massot]

What should I do with this converter vs conversion? Follow Leo or tradition?

[Mario Carneiro]

My guess is this is a non-native speakerism

[Patrick Massot]

I can understand that

[Patrick Massot]

It does not tell what to do

[Kevin Buzzard]

Go with tradition

[Kevin Buzzard]

but put a warning that Leo can change things at any time and then the docs will be broken

[Patrick Massot]

Writing conversion instead of converter would not break any code in the documentation

[Patrick Massot]

The full name is used only in the name (which does not need to be explicitly imported since it's in init) and docstrings

[Patrick Massot]

Hum, the name is also used in the infamous error message: "find converter failed, pattern was not found"

[Patrick Massot]

Now I have a sentence containing both versions (I did not dare correcting the error message)

[Sebastian Ullrich]

Whelp, now I remember why I didn't fix the error message. conv uses tactic.ext_simplify_core, which doesn't really allow propagating errors.

[Patrick Massot]

So it would be really complicated to fix?

[Sebastian Ullrich]

It's not trivial at least