Bug in `polyrith`?

Stream: mathlib4

[Heather Macbeth]

On the following test polyrith gives the output

polyrith found the following certificate, but it failed to close the goal:
↑s * ↑y * h₁ + ↑r * ↑x * h₂ - 1 * h₃ + (↑b + 1) * h₄ + (↑a + 1) * h₅ + h₆

as well as quite a number of other complaints ("ring failed, ring expressions not equal", "ring failed: not an equality", "failed to synthesize instance HMul ℕ ℕ ℤ"):

import Mathlib.Tactic.Polyrith

example {r a p s b q t u x y z : ℕ}
    (h₁ : (r:ℤ) = (a + 1) * p)
    (h₂ : (s:ℤ) = (b + 1) * q)
    (h₃ : (t:ℤ) = ((1 + a + b) + 1) * u)
    (h₄ : (x:ℤ) * (r:ℤ) * q = u)
    (h₅ : (y:ℤ) * p * (s:ℤ) = u)
    (h₆ : (z:ℤ) * (r:ℤ) * (s:ℤ) = ((x:ℤ) + (y:ℤ)) * (r:ℤ) * (s:ℤ)) :
    (z:ℤ) * (r:ℤ) * (s:ℤ) = (t:ℤ) := by
  polyrith

[Heather Macbeth]

Any ideas? I think it's something to do with the interaction with casting, because the same test works fine when the variables are integers.

[Mario Carneiro]

polyrith actually has to go through an Expr -> Syntax -> Expr roundtrip because it is trying to produce something that can be fed to linear_combination. So things like lossy pretty printing do affect it

[Mario Carneiro]

there are some tricks it could pull to make the roundtrip lossless even though users can't write it, but I think that would weaken the claim of a Try this: <stuff that doesn't work> prompt

[Heather Macbeth]

It works in mathlib3! Is there a different mechanism there?

[Thomas Murrills]

Maybe coercions could be rendered in an "input form", though; if you replace up-arrows with type annotations the following call to linear_combination works:

linear_combination (s : ℤ) * (y : ℤ) * h₁ + (r : ℤ) * (x : ℤ) * h₂ - 1 * h₃ + ((b : ℤ) + 1) * h₄ + ((a : ℤ) + 1) * h₅ + h₆

[Mario Carneiro]

Oh, I just noticed that the "failed to synthesize instance" error occurs at position 0:0 which makes it look like the import line didn't work

[Mario Carneiro]

Thomas Murrills said:

Maybe coercions could be rendered in an "input form", though; if you replace up-arrows with type annotations the following call to linear_combination works:

linear_combination (s : ℤ) * (y : ℤ) * h₁ + (r : ℤ) * (x : ℤ) * h₂ - 1 * h₃ + ((b : ℤ) + 1) * h₄ + ((a : ℤ) + 1) * h₅ + h₆

Sure, but lossless pretty printing has been a dream for ages and it's a huge project

[Thomas Murrills]

I see, so not worth doing piecemeal?

[Mario Carneiro]

Heather Macbeth said:

It works in mathlib3! Is there a different mechanism there?

Yes, linear_combination works differently in mathlib4, being primarily a macro now which manipulates syntax directly instead of working on exprs

[Mario Carneiro]

It is pretty funny (but expected) that this works:

example {r a p s b q t u x y z : ℕ}
    (h₁ : (r:ℤ) = (a + 1) * p)
    (h₂ : (s:ℤ) = (b + 1) * q)
    (h₃ : (t:ℤ) = ((1 + a + b) + 1) * u)
    (h₄ : (x:ℤ) * (r:ℤ) * q = u)
    (h₅ : (y:ℤ) * p * (s:ℤ) = u)
    (h₆ : (z:ℤ) * (r:ℤ) * (s:ℤ) = ((x:ℤ) + (y:ℤ)) * (r:ℤ) * (s:ℤ)) :
    (z:ℤ) * (r:ℤ) * (s:ℤ) = (t:ℤ) := by
  set_option pp.all true in
  polyrith

[Mario Carneiro]

Also @Heather Macbeth can you elaborate on what you mean by "it works in mathlib3"? Does it actually produce something you can successfully copy-paste?

[Mario Carneiro]

I don't know whether there is an option for coercions to show the expected type like @Thomas Murrills suggests. Using set_option pp.coercions false causes it to print Nat.cast applications, which doesn't really fix the type ambiguities here

[Heather Macbeth]

@Mario Carneiro On the following Lean 3 code

import tactic.polyrith

example {r a p s b q t u x y z : ℕ}
    (h₁ : (r:ℤ) = (a + 1) * p)
    (h₂ : (s:ℤ) = (b + 1) * q)
    (h₃ : (t:ℤ) = ((1 + a + b) + 1) * u)
    (h₄ : (x:ℤ) * (r:ℤ) * q = u)
    (h₅ : (y:ℤ) * p * (s:ℤ) = u)
    (h₆ : (z:ℤ) * (r:ℤ) * (s:ℤ) = ((x:ℤ) + (y:ℤ)) * (r:ℤ) * (s:ℤ)) :
    (z:ℤ) * (r:ℤ) * (s:ℤ) = (t:ℤ) :=
begin
  polyrith,
end

I get "goals accomplished :tada:" with a blue underline "try this" for

linear_combination ↑s * ↑y * h₁ + ↑r * ↑x * h₂ - h₃ + (↑b + 1) * h₄ + (↑a + 1) * h₅ + h₆

and when you click the "try this" to insert that code, it also works.

[Heather Macbeth]

Maybe the key point is that (as you said) linear_combination is more robust in mathlib3: this (without coercions)

linear_combination s * y * h₁ + r * x * h₂ - h₃ + (b + 1) * h₄ + (a + 1) * h₅ + h₆

solves the example in mathlib3 but not in mathlib4.

[Mario Carneiro]

To give a simpler example:

example {r s a b : ℕ} (h₁ : (r : ℤ) = a + 1) (h₂ : (s : ℤ) = b + 1) :
    r * s = (a + 1 : ℤ) * (b + 1) := by
  polyrith

expands to

example {r s a b : ℕ} (h₁ : (r : ℤ) = a + 1) (h₂ : (s : ℤ) = b + 1) :
    r * s = (a + 1 : ℤ) * (b + 1) := by
  linear_combination
    (↑b + 1) * h₁ + ↑r * h₂

which expands to

open Mathlib.Tactic.LinearCombination in
example {r s a b : ℕ} (h₁ : (r : ℤ) = a + 1) (h₂ : (s : ℤ) = b + 1) :
    r * s = (a + 1 : ℤ) * (b + 1) := by
    refine eq_of_add (add_pf (c_mul_pf (↑b + 1) h₁) (c_mul_pf ↑r h₂)) ?_ <;>
    ring1

which fails due to elaboration issues in the refine line

[Heather Macbeth]

Does the mathlib3 implementation effectively do that, too?

[Mario Carneiro]

The mathlib3 version assumes everything is over a single type and elaborates everything in advance of constructing the term. In this case we are literally constructing a syntax to pass to refine

[Mario Carneiro]

one of the things the new implementation buys us is that it can be much more flexible with regard to putting h's in different places. The mathlib3 version is limited to linear combinations (as the name suggests) with the h's on the right, but the mathlib4 version can do stuff like h1 * h2 + 3 / h3 as well

[Heather Macbeth]

Perhaps we could have both. It would be nice to have a very robust version which we could even just call polyrith_with_witness, which fixes a type and doesn't need the flexibility since the syntax is provided by autogenerated output. That could follow the mathlib3 implementation. And also keep the current macro version.

[Mario Carneiro]

but at the end of the day it is more or less just a macro over refine, so the issues here can be traced back to elaborator troubles. For example, it is odd that this doesn't work:

theorem c_mul_pf [Mul α] (p : b = c) (a : α) : a * b = a * c := p ▸ rfl

example {r a b : ℕ} (h₁ : (r : ℤ) = a + 1) : True := by
    have := c_mul_pf (↑b + 1) h₁

have := c_mul_pf (α := ℤ) (↑b + 1) h₁ works

[Mario Carneiro]

In this case we know the types of the h's, so I can add more type ascriptions if that's what is needed to keep the elaborator from getting confused

[Mario Carneiro]

It seems that putting the variable second is sufficient to fix the issue:

theorem c_mul_pf' [Mul α] (p : b = c) (a : α) : a * b = a * c := p ▸ rfl

example {r a b : ℕ} (h₁ : (r : ℤ) = a + 1) : True := by
    have := c_mul_pf' h₁ (↑b + 1)

[Mario Carneiro]

!4#2678

[Heather Macbeth]

Thanks!!

[Heather Macbeth]

You give the test case

example {r s a b : ℕ} (h₁ : (r : ℤ) = a + 1) (h₂ : (s : ℤ) = b + 1) :
    r * s = (a + 1 : ℤ) * (b + 1) := by
  linear_combination (↑b + 1) * h₁ + ↑r * h₂

Does this also work on your branch?

example {r s a b : ℕ} (h₁ : (r : ℤ) = a + 1) (h₂ : (s : ℤ) = b + 1) :
    r * s = (a + 1 : ℤ) * (b + 1) := by
  linear_combination (b + 1) * h₁ + r * h₂

If I understand correctly, it would have in mathlib3.

[Mario Carneiro]

yes it does. The version with the up arrows is relevant for being the style that polyrith generates

[Kevin Buzzard]

Mario Carneiro said:

one of the things the new implementation buys us is that it can be much more flexible with regard to putting h's in different places. The mathlib3 version is limited to linear combinations (as the name suggests) with the h's on the right, but the mathlib4 version can do stuff like h1 * h2 + 3 / h3 as well

What the heck does 3 / h3 mean?

[Mario Carneiro]

if h3 : x = y then it is a proof of 3 / x = 3 / y

[Mario Carneiro]

You can basically write arbitrary expressions involving equations this way, it's just a variation on congr

[Mario Carneiro]

There was another mathlib3 tactic that was added to construct things like this with a congr like name but I can't find it now... it had syntax like apply_fun a + _1 * _2, does this ring any bells?

[Eric Wieser]

tactic#congrm?

[Eric Wieser]

I think someone is porting that to lean 4

[Mario Carneiro]

yeah, that

[Mario Carneiro]

basically linear_combination does that but specialized to +,-,*,/, and then passes the results to ring1

[Heather Macbeth]

I think the following might be another bug in polyrith (cc @Mario Carneiro):

import Mathlib.Tactic.Polyrith

-- works
example (y a : ℤ) (k : ℕ) (h : a ^ k = 0) : a ^ k * y = 0 := by
  linear_combination y * h

-- works
example (y a : ℤ) (h : a = 0) : a * y = 0 := by polyrith

-- fails
example (y a : ℤ) (k : ℕ) (h : a ^ k = 0) : a ^ k * y = 0 := by
  polyrith
/-
polyrith failed to retrieve a solution from Sage! TypeError:
a is neither an integer nor a rational
-/

[Mario Carneiro]

hm, this is annoying to solve. It appears that sage doesn't like it when you give it a "polynomial expression" like a ^ k * y

[Heather Macbeth]

But here a ^ k should be sent as a single token, right? Because k is not a numeral.

[Heather Macbeth]

I guess the issue is to parse a ^ 17 differently from a ^ k.

[Heather Macbeth]

(It works in mathlib3.)

[Mario Carneiro]

...or not: !4#3224

[Mario Carneiro]

The issue is that polyrith builds on ring, which has a more permissive concept of "polynomial" due to its ring_exp heritage in lean 3

[Mario Carneiro]

so it has to explicitly not parse things the same way ring would in order to not produce non-polynomial expressions that will confuse sage

[Heather Macbeth]

Thanks!