Lean4
/-- Negates a monomial `va` to get another monomial.
* `-c = (-c)` (for `c` coefficient)
* `-(a₁ * a₂) = a₁ * -a₂`
-/
def evalNegProd {a : Q($α)} (rα : Q(Ring $α)) (va : ExProd sα a) : MetaM <| Result (ExProd sα) q(-$a) := do
Lean.Core.checkSystem decl_name%.toString
match va with
| .const za ha =>
let ⟨m1, _⟩ := ExProd.mkNegNat sα rα 1
let rm := Result.isNegNat rα q(nat_lit 1) q(IsInt.of_raw $α (.negOfNat (nat_lit 1)))
let ra := Result.ofRawRat za a ha
let rb ← rm.mul ra
let ⟨zb, hb⟩ := rb.toRatNZ.get!
let ⟨b, pb⟩ := rb.toRawEq
have pb : Q(((Int.negOfNat (nat_lit 1)).rawCast : $α) * $a = $b) := pb
return ⟨b, .const zb hb, q(neg_one_mul (R := $α) $pb)⟩
| .mul (x := a₁) (e := a₂) va₁ va₂ va₃ =>
let ⟨_, vb, pb⟩ ← evalNegProd rα va₃
return ⟨_, .mul va₁ va₂ vb, (q(neg_mul $a₁ $a₂ $pb) : Expr)⟩
