divides m_1 m_2 is documented to check m_1[i] <= m_2[i] for all i, but actually computes m_2[i] <= m_1[i].
The divides function is defined as:
/-- Check if $m_1$ divides $m_2$ (true if all exponents of $m_1$ are $\le$ those of $m_2$). -/
def divides (m_1 m_2 : CMvMonomial n) : Bool :=
Vector.all (Vector.zipWith (flip Nat.ble) m_1 m_2) (· == true)
flip makes it compute m_2[i] <= m_1[i] -- opposite of the docstring.
Executed:
divides #m[1,0] #m[2,1] -> false (doc says true: x divides x^2*y)divides #m[2,1] #m[1,0] -> true (doc says false)
Not sure which side is wrong: the body looks deliberate isDivisibleBy semantics. But the Dvd instance binds it to |, whose meaning Mul already fixes: as is, X | X^2 evaluates to false while X^2 = X * X -- wrong whichever way the helper was intended.
Spread: the Decidable (m_1 | m_2) instance lets decide kernel-certify the transposed relation, and a duplicate of it sits at L126.
Git commit: 18c1613.
divides m_1 m_2is documented to checkm_1[i] <= m_2[i]for alli, but actually computesm_2[i] <= m_1[i].The divides function is defined as:
flipmakes it computem_2[i] <= m_1[i]-- opposite of the docstring.Executed:
divides #m[1,0] #m[2,1]->false(doc saystrue: x divides x^2*y)divides #m[2,1] #m[1,0]->true(doc saysfalse)Not sure which side is wrong: the body looks deliberate
isDivisibleBysemantics. But theDvdinstance binds it to|, whose meaningMulalready fixes: as is,X | X^2evaluates tofalsewhileX^2 = X * X-- wrong whichever way the helper was intended.Spread: the
Decidable (m_1 | m_2)instance letsdecidekernel-certify the transposed relation, and a duplicate of it sits at L126.Git commit:
18c1613.