UniPoly equivalence relation and quotient operations

[dhsorens]

Summary

This PR:

• proves the equivalence relation defined on UniPoly is transitive, using an (assumed) lemma analogous to the (also unproved) lemma used in the List case
• defines functions add, neg, and sub on the resulting quotient and proves that the equivalent operations on UniPoly descend

From here, the main TODO would be to show that the remaining operations on UniPoly descend to the quotient.

Related Issue

Related to #7

[mitschabaude]

I think it would be good to redefine equiv to be Trim.equiv, which we already have a lot of theory about

[dhsorens]

@mitschabaude That is sensible, I had wondered why there was a separate definition. I made the change, which essentially eliminated the need for unproved lemmas. The only remaining is neg_coeff

FIX: everything included in this PR is now proved

[dhsorens]

Is any reason to keep the old definition around, possibly proving equivalence?

[quangvdao]

Awesome! What is the old definition you're referring to?

[dhsorens]

@quangvdao the old definition is this one here -- two polynomials are equivalent if, when zero-padded into arrays of the same size, they are equal

[quangvdao]

Ah yeah. sounds good to me

Also we should think about which of QuotientUniPoly or UniPolyC should be "the" way to get equivalence with polynomial. The non-quotient version might be preferable?

[dhsorens]

From what I can tell, that probably depends on what the vision of this repo is (I'm familiar with it, but still new here!). Aesthetically, I quite like QuotientUniPoly -- but UniPolyC is likely more computation-friendly? Considering this is a repo directly aimed at snarkification/formal verification we might favor the computation (non-quotient) in the long run

[alexanderlhicks]

LGTM?

[alexanderlhicks]

/review

External:

Internal:
ArkLib/Data/UniPoly

Comments:
Please review and identify any possible issues or possible improvements.

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Hello! As an expert code reviewer, I've analyzed the pull request. Here is my review:

High-Level Summary

This pull request significantly improves the formalization of univariate polynomials (UniPoly) by refactoring the notion of polynomial equivalence. The old, implementation-dependent definition of equiv is replaced with the more natural Trim.equiv, which states that two polynomials are equivalent if their coefficients are equal.

Building on this solid foundation, the PR then begins to construct the quotient type QuotientUniPoly, defining add, neg, and sub operations that respect this equivalence. This is a crucial step towards creating a robust and usable computable polynomial type that aligns with standard algebraic structures.

The changes are well-motivated and represent a clear architectural improvement. I have one major concern regarding a pre-existing sorry and a few suggestions to improve the clarity of the new proofs.

Critical Issue: Dependency on sorry

The proofs for add_descends and sub_descends rely on the helper lemma add_coeff?, which in turn depends on add_coeff. However, add_coeff is currently defined with a sorry.

-- from ArkLib/Data/UniPoly/Basic.lean
theorem add_coeff {p q : UniPoly Q} {i : ℕ} (hi : i < (add_raw p q).size) :
  (add_raw p q)[i] = p.coeff i + q.coeff i
:= by
  simp [add_raw]
  sorry
  -- ...

This is a critical issue, as it means the core correctness proofs for the new quotient operations are incomplete. Since this PR's changes are fundamentally about addition and subtraction, this sorry should be resolved as part of this PR.

Suggestion:

Please fill in the sorry. The proof is relatively straightforward by reasoning about Array.matchSize and Array.rightpad. Here is a complete proof that you can use:

theorem add_coeff {p q : UniPoly Q} {i : ℕ} (hi : i < (add_raw p q).size) :
  (add_raw p q)[i] = p.coeff i + q.coeff i := by
  simp only [add_raw]
  let ⟨p', q'⟩ := Array.matchSize p q 0
  have h_size_eq : p'.size = q'.size := matchSize_size_eq
  have h_size_add : (Array.zipWith (· + ·) p' q').size = p'.size := zipWith_size h_size_eq
  have hi' : i < p'.size := by rwa [h_size_add]
  rw [Array.getElem_zipWith p' q' (·+·) i hi']
  have h_p'_coeff : p'[i] = p.coeff i := by
    unfold Array.matchSize at p'; split
    · case inl h =>
      simp [h]
      rw [Array.get_rightpad _ _ _ hi', coeff, Array.getD]
    · case inr h =>
      simp [h]
      have hi_p : i < p.size := by
        rw [add_size, max_eq_left (Nat.le_of_not_lt h)] at hi
        exact hi
      rw [coeff_eq_getElem hi_p]
  have h_q'_coeff : q'[i] = q.coeff i := by
    unfold Array.matchSize at q'; split
    · case inl h =>
      simp [h]
      have hi_q : i < q.size := by
        rw [add_size, max_eq_right_of_lt h] at hi
        exact hi
      rw [coeff_eq_getElem hi_q]
    · case inr h =>
      simp [h]
      rw [Array.get_rightpad _ _ _ hi', coeff, Array.getD]
  rw [h_p'_coeff, h_q'_coeff]

Suggestions for Improvement

1. Simplify Proofs for ..._descends

The proofs for add_descends and sub_descends are correct, but their structure involving chains of equiv_trans is a bit convoluted and hard to follow. They can be made much clearer by using trim_equiv to relate the trimmed add operation to the add_raw operation and then reasoning directly about the coefficients.

Suggestion for add_descends:

-lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : UniPoly R) :
-  equiv a₁ a₂ → equiv b₁ b₂ → add_descending a₁ b₁ = add_descending a₂ b₂ := by
-  intros heq_a heq_b
-  unfold add_descending
-  rw [Quotient.eq]
-  simp [instSetoidUniPoly]
-  apply equiv_trans (add_equiv_raw a₁ b₁)
-  apply equiv_symm
-  apply equiv_trans (add_equiv_raw a₂ b₂)
-  unfold equiv at *
-  intro i
-  rw [add_coeff? a₁ b₁ i, add_coeff? a₂ b₂ i, heq_a i, heq_b i]
+lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : UniPoly R) :
+  equiv a₁ a₂ → equiv b₁ b₂ → add_descending a₁ b₁ = add_descending a₂ b₂ := by
+  intros heq_a heq_b
+  rw [Quotient.eq]
+  simp only [instSetoidUniPoly, equiv, add_descending, add]
+  -- `add p q` is `(add_raw p q).trim`, and `p.trim` is equivalent to `p`
+  rw [trim_equiv, trim_equiv]
+  -- Goal is now `equiv (add_raw a₁ b₁) (add_raw a₂ b₂)`. Prove by coefficient equality.
+  intro i
+  rw [add_coeff?, add_coeff?, heq_a, heq_b]

Suggestion for sub_descends:

-lemma sub_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : UniPoly R) :
-  equiv a₁ a₂ → equiv b₁ b₂ → sub_descending a₁ b₁ = sub_descending a₂ b₂ := by
-  unfold equiv sub_descending
-  intros heq_a heq_b
-  rw [Quotient.eq]
-  simp [instSetoidUniPoly]
-  unfold equiv sub
-  apply equiv_trans (add_equiv_raw a₁ b₁.neg)
-  apply equiv_symm
-  apply equiv_trans (add_equiv_raw a₂ b₂.neg)
-  intro i
-  rw [add_coeff? a₁ b₁.neg i, add_coeff? a₂ b₂.neg i, neg_coeff b₁ i, neg_coeff b₂ i]
-  rw [heq_a i, heq_b i]
+lemma sub_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : UniPoly R) :
+  equiv a₁ a₂ → equiv b₁ b₂ → sub_descending a₁ b₁ = sub_descending a₂ b₂ := by
+  intros heq_a heq_b
+  rw [Quotient.eq]
+  simp only [instSetoidUniPoly, equiv, sub_descending, sub, add]
+  rw [trim_equiv, trim_equiv]
+  -- Goal is `equiv (add_raw a₁ (neg b₁)) (add_raw a₂ (neg b₂))`
+  intro i
+  rw [add_coeff?, add_coeff?, neg_coeff, neg_coeff, heq_a, heq_b]

These revised proofs are more direct and easier to understand.

2. Minor Cleanup

The open List in on the equiv_trans theorem is a leftover from the previous implementation and can be removed.

-open List in
 /-- Transitivity of the equivalence relation. -/
 @[simp] theorem equiv_trans {p q r : UniPoly Q} : Trim.equiv p q → equiv q r → equiv p r := by
   simp_all [Trim.equiv]

Conclusion

This is a valuable contribution that improves the foundations of the UniPoly library. Once the critical issue with the sorry is addressed, and with the suggested proof simplifications for better readability, I would be happy to approve this PR. Thank you for your work

[dhsorens]

gh actions made a good point on the proofs of add_descends and sub_descends so I have improved them using calc notation and pushed. I would be very happy to address the proof of add_coeff next but it's not a theorem introduced in this PR so I would argue not related to this one (should ofc be done soon though)

[dhsorens]

next steps include the TODOs and sorrys of UniPoly and showing that the rest of the operations on UniPoly descend to the quotient

[quangvdao]

Okay, this looks good to me. will merge.