Direct Sums for Computational Polynomials

Stream: mathlib4

[Dhruv Bhatia]

As per this link, I decided to try using direct sums to model computational polynomials. One of the examples there shows, using decide, that a certain Finset (CPolynomial Int) contains elements that are all not equal to 0.

However, when I changed Int to Rat, I get a weird instance error. Consider the following:

import Mathlib

open scoped DirectSum

abbrev CPolynomial (R) [Semiring R] := ⨁ i : ℕ, R
abbrev CPolynomial.X {R} [Semiring R] : CPolynomial R := .single 1 1

unsafe instance {R} [Semiring R] [Repr R] : Repr (CPolynomial R) where
  reprPrec x prec :=
    let l := x.support'.unquot.1.sort (· ≤ ·)
    Std.Format.joinSep (l.map fun
      | 0 => repr (x 0)
      | 1 => f!"{repr (x 1)}*X"
      | i => f!"{repr (x i)}*X^{i}") f!" + "

open CPolynomial

example : (2 * X^3 + 1 : CPolynomial ℚ) = 0 := by
  decide

#eval (2 * X^3 + 1 : CPolynomial ℚ) = 0

#synth DecidableEq (CPolynomial ℚ)

Can anyone explain why the eval and the synth commands work, but the example doesn't? Thanks!

[Yan Yablonovskiy 🇺🇦]

Opening in lean playground, it looks like the eval shows false as the result in the infoview. So thats good

[Dhruv Bhatia]

yes, false is the correct output

[Yan Yablonovskiy 🇺🇦]

Dhruv Bhatia said:

yes, false is the correct output

Yea i realised that it should still decide regardless

[Dhruv Bhatia]

are you getting the same long instance unfolding error when using decide? It seems to not be able to find an instance of Decidable for the prop 2 * X ^ 3 + 1 = 0

[Yan Yablonovskiy 🇺🇦]

Dhruv Bhatia said:

are you getting the same long instance unfolding error when using decide? It seems to not be able to find an instance of Decidable for the prop 2 * X ^ 3 + 1 = 0

Yea i get a stuck at reduction error when unfolding instances

[Yan Yablonovskiy 🇺🇦]

Note if you use native_decide you get

Tactic `native_decide` evaluated that the proposition
  2 * X ^ 3 + 1 = 0
is false

which i guess means the eval fits the goal statement at least

[Dhruv Bhatia]

makes sense, we did see that #eval was already working

[Yan Yablonovskiy 🇺🇦]

it only gets more confusing, you can use

#reduce instDecidableEqDirectSum ℕ (fun i => ℚ) (2 * X ^ 3 + 1) 0

to end up seeing isFalse . It might also be something specifically to do with the tactic, looking at the docs:

Limitation: In the default mode or +kernel mode, since decide uses reduction to evaluate the term, Decidable instances defined by well-founded recursion might not work because evaluating them requires reducing proofs. Reduction can also get stuck on Decidable instances with Eq.rec terms. These can appear in instances defined using tactics (such as rw and simp). To avoid this, create such instances using definitions such as decidable_of_iff instead.

[Yan Yablonovskiy 🇺🇦]

Looks like this works:

example : (2 * X^3 + 1 : CPolynomial ℚ)  = 0 := by
   with_unfolding_all decide