linarith Preprocessor

Stream: mathlib4

[Patrick Massot]

Mario, while you're here, I have another question. In Lean3, the linarith preprocessors used the tactic monad (what else?). In Lean 4 they use MetaM. Isn't it a problem for rewriting?

[Patrick Massot]

I mean specifically https://github.com/leanprover-community/mathlib/blob/36b8aa61ea7c05727161f96a0532897bd72aedab/src/tactic/linarith/preprocessing.lean#L202-L207

[Mario Carneiro]

what do you mean by "problem for rewriting"?

[Patrick Massot]

I must confess I didn't try too hard to think about what this function is doing, but a very naive port is at https://github.com/leanprover-community/mathlib4/blob/linarithRat/Mathlib/Tactic/Linarith/Preprocessing.lean#L283-L290 which is in TacticM

[Patrick Massot]

The secret goal of this message is to make you panic and port this yourself to prevent me from writing non-sense.

[Mario Carneiro]

Generally, things should be in TacticM if they actually use / manipulate the goal state, TermElabM if they need to elaborate syntax, and MetaM if they just need to be able to unify metavariables and know the local context

[Mario Carneiro]

the description of the function doesn't sound like it needs anything more than MetaM but I'm not sure about how the implementation is supposed to work

[Mario Carneiro]

MVarId.rewrite is in MetaM, what requires more?

[Patrick Massot]

But where would the MVarId come from?

[Mario Carneiro]

a parameter

[Patrick Massot]

This is what was puzzling to me. So I simply assumed it was meant to be the main goal.

[Mario Carneiro]

"tactics" in MetaM just pass MVarIds in and out

[Mario Carneiro]

like MVarId.rewrite

[Mario Carneiro]

for that you don't really need the goal state

[Patrick Massot]

I understand this. I'm talking about my specific case.

[Mario Carneiro]

/-- `normalizeDenominatorsInLHS h lhs` assumes that `h` is a proof of `lhs R 0`.
 It creates a proof of `lhs' R 0`, where all numeric division in `lhs` has been cancelled. -/

sounds like it's getting the argument in a parameter

[Mario Carneiro]

I mean this doesn't even care about the goal

[Mario Carneiro]

it's just building a proof of one thing from another

[Patrick Massot]

I agree it sounds like it doesn't care about the goal, but I'm confused about what it is rewriting.

[Mario Carneiro]

I'm confused about your confusion

[Mario Carneiro]

what is "it"?

[Patrick Massot]

I think you would waste a lot less time by actually looking at the Lean 3 code and telling me what the Lean 4 code should be.

[Mario Carneiro]

MVarId.rewrite rewrites the type of the goal it is passed, by assigning it and returning a new mvar with a different type

[Patrick Massot]

I mean wasting your time

[Mario Carneiro]

I'm working based on github because I will be leaving in a few minutes

[Patrick Massot]

I think the core problem is I couldn't find the actual analogue of docs#tactic.rewrite_core

[Mario Carneiro]

oh I see you are confused by this docstring

/--
Rewrite goal `mvarId`
-/
def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
    (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult :=

[Mario Carneiro]

it appears that e is the expression to rewrite (e.g. the type of the goal or of a hypothesis), and heq is an equality that you are using to rewrite with

[Patrick Massot]

But what is mvarId?

[Patrick Massot]

That mvarId argument is the reason why I went to TacticM where I can get something which at least has the correct type.

[Mario Carneiro]

it appears to be essentially unused, except that it is used for deriving the names of subgoals and for the local context

[Mario Carneiro]

I think you could just pass mkFreshExprMVar to it

[Patrick Massot]

Ok, I'll try that, thanks.

[Patrick Massot]

I'll stop for today because I need some sleep, but everybody should feel free to hack on https://github.com/leanprover-community/mathlib4/tree/linarithRat. The current state is everything type-checks but nothing works (see the test file for linarith).

[Scott Morrison]

I'm looking at this now. (Actually I started fresh after looking at the PR, I'll report what I find soon!)

[Scott Morrison]

!4#3801. That took longer than it should have, because I kept mixing up the arguments of MVarId.rewrite (order of arguments, and expressions vs types :woman_facepalming:). I added Expr.rewrite and Expr.rewriteType as helper functions to be less confusing next time around!

[Patrick Massot]

Amazing! Do you understand why my version wasn't working (apart from the fact that I wrote it at least one hour too late instead of sleeping)?

[Scott Morrison]

At least one thing wrong with your code:

lhs.containsConst (λ n => n = `has_div.div)

is looking for a mathlib3 name that doesn't exist anymore, so your code never fired.

[Patrick Massot]

That's indeed a very good reason, and very consistent with the time of the day when this was written.

[Scott Morrison]

Don't worry, I made exactly the same mistake on the first pass. :-)

[Alex J. Best]

Using

``has_div.div

is a way to prevent this btw, it checks that the name actually refers to a declaration at compile time.