Lean4
/-- Extract a common factor `L` of two products-of-powers `l₁` and `l₂` in `M`, in the sense that
both `l₁` and `l₂` are quotients by `L` of products of *positive* powers.
The variable `cond` specifies whether we extract a *certified nonzero[/positive]* (and therefore
potentially smaller) common factor. If so, the metaprogram returns a "proof" that this common factor
is nonzero/positive, i.e. an expression `Q(NF.eval $(L.toNF) ≠ 0)` / `Q(0 < NF.eval $(L.toNF))`. -/
partial def gcd (iM : Q(CommGroupWithZero $M)) (l₁ l₂ : qNF M)
(disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type)) (cond : DenomCondition (M := M) q(inferInstance)) :
MetaM <|
Σ (L l₁' l₂' : qNF M),
Q((NF.eval $(L.toNF)) * NF.eval $(l₁'.toNF) = NF.eval $(l₁.toNF)) ×
Q((NF.eval $(L.toNF)) * NF.eval $(l₂'.toNF) = NF.eval $(l₂.toNF)) × cond.proof L :=
/- Handle the case where atom `i` is present in the first list but not the second. -/
let absent (l₁ l₂ : qNF M) (n : ℤ) (e : Q($M)) (i : ℕ) :
MetaM <|
Σ (L l₁' l₂' : qNF M),
Q((NF.eval $(L.toNF)) * NF.eval $(l₁'.toNF) = NF.eval $(qNF.toNF (((n, e), i) :: l₁))) ×
Q((NF.eval $(L.toNF)) * NF.eval $(l₂'.toNF) = NF.eval $(l₂.toNF)) × cond.proof L :=
do
let ⟨L, l₁', l₂', pf₁, pf₂, pf₀⟩ ← gcd iM l₁ l₂ disch cond
if 0 < n then
-- Don't pull anything out
return ⟨L, ((n, e), i) :: l₁', l₂', (q(NF.eval_mul_eval_cons $n $e $pf₁) :), q($pf₂), pf₀⟩
else if n = 0 then
-- Don't pull anything out, but eliminate the term if it is a cancellable zero
let ⟨l₁'', pf''⟩ ← tryClearZero disch iM 0 e i l₁'
let pf'' : Q(NF.eval ((0, $e) ::ᵣ $(l₁'.toNF)) = NF.eval $(l₁''.toNF)) := pf''
return ⟨L, l₁'', l₂', (q(NF.eval_mul_eval_cons_zero $pf₁ $pf'') :), q($pf₂), pf₀⟩
try
let (pf, b) ← mkDenomConditionProofSucc disch pf₀ e n i
return
⟨((n, e), i) :: L, l₁', ((-n, e), i) :: l₂', (q(NF.eval_cons_mul_eval $n $e $pf₁) :),
(q(NF.eval_cons_mul_eval_cons_neg $n $pf $pf₂) :), b⟩
catch _ =>
-- if we can't prove nonzeroness, don't pull out e.
return
⟨L, ((n, e), i) :: l₁', l₂', (q(NF.eval_mul_eval_cons $n $e $pf₁) :), q($pf₂), pf₀⟩
/- Handle the case where atom `i` is present in both lists. -/
let bothPresent (t₁ t₂ : qNF M) (n₁ n₂ : ℤ) (e : Q($M)) (i : ℕ) :
MetaM <|
Σ (L l₁' l₂' : qNF M),
Q((NF.eval $(L.toNF)) * NF.eval $(l₁'.toNF) = NF.eval $(qNF.toNF (((n₁, e), i) :: t₁))) ×
Q((NF.eval $(L.toNF)) * NF.eval $(l₂'.toNF) = NF.eval $(qNF.toNF (((n₂, e), i) :: t₂))) × cond.proof L :=
do
let ⟨L, l₁', l₂', pf₁, pf₂, pf₀⟩ ← gcd iM t₁ t₂ disch cond
if n₁ < n₂ then
let N : ℤ := n₂ - n₁
return
⟨((n₁, e), i) :: L, l₁', ((n₂ - n₁, e), i) :: l₂', (q(NF.eval_cons_mul_eval $n₁ $e $pf₁) :),
(q(NF.mul_eq_eval₂ $n₁ $N $e $pf₂) :), ← mkDenomConditionProofSucc' disch pf₀ e n₁ i⟩
else if n₁ = n₂ then
return
⟨((n₁, e), i) :: L, l₁', l₂', (q(NF.eval_cons_mul_eval $n₁ $e $pf₁) :),
(q(NF.eval_cons_mul_eval $n₂ $e $pf₂) :), ← mkDenomConditionProofSucc' disch pf₀ e n₁ i⟩
else
let N : ℤ := n₁ - n₂
return
⟨((n₂, e), i) :: L, ((n₁ - n₂, e), i) :: l₁', l₂', (q(NF.mul_eq_eval₂ $n₂ $N $e $pf₁) :),
(q(NF.eval_cons_mul_eval $n₂ $e $pf₂) :), ← mkDenomConditionProofSucc' disch pf₀ e n₂ i⟩
match l₁, l₂ with
| [], [] =>
pure
⟨[], [], [], (q(one_mul (NF.eval $(qNF.toNF (M := M) []))) :), (q(one_mul (NF.eval $(qNF.toNF (M := M) []))) :),
cond.proofZero⟩
| ((n, e), i) :: t, [] => do
let ⟨L, l₁', l₂', pf₁, pf₂, pf₀⟩ ← absent t [] n e i
return ⟨L, l₁', l₂', q($pf₁), q($pf₂), pf₀⟩
| [], ((n, e), i) :: t => do
let ⟨L, l₂', l₁', pf₂, pf₁, pf₀⟩ ← absent t [] n e i
return ⟨L, l₁', l₂', q($pf₁), q($pf₂), pf₀⟩
| ((n₁, e₁), i₁) :: t₁, ((n₂, e₂), i₂) :: t₂ => do
if i₁ > i₂ then
let ⟨L, l₁', l₂', pf₁, pf₂, pf₀⟩ ← absent t₁ (((n₂, e₂), i₂) :: t₂) n₁ e₁ i₁
return ⟨L, l₁', l₂', q($pf₁), q($pf₂), pf₀⟩
else if i₁ == i₂ then
try
bothPresent t₁ t₂ n₁ n₂ e₁ i₁
catch _ =>
-- if `bothPresent` fails, don't pull out `e`
-- the failure case of `bothPresent` should be:
-- * `.none` case: never
-- * `.nonzero` case: if `e` can't be proved nonzero
-- * `.positive _` case: if `e` can't be proved positive
let ⟨L, l₁', l₂', pf₁, pf₂, pf₀⟩ ← gcd iM t₁ t₂ disch cond
return
⟨L, ((n₁, e₁), i₁) :: l₁', ((n₂, e₂), i₂) :: l₂', (q(NF.eval_mul_eval_cons $n₁ $e₁ $pf₁) :),
(q(NF.eval_mul_eval_cons $n₂ $e₂ $pf₂) :), pf₀⟩
else
let ⟨L, l₂', l₁', pf₂, pf₁, pf₀⟩ ← absent t₂ (((n₁, e₁), i₁) :: t₁) n₂ e₂ i₂
return ⟨L, l₁', l₂', q($pf₁), q($pf₂), pf₀⟩
