\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Module
\import Arith.Fin.Order
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Solver
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Arith.Bool
\import Arith.Int
\import Arith.Nat
\import Algebra.Semiring
\import Arith.Rat
\import Data.Bool
\import Data.List
\import Function.Meta
\import Order.Lattice
\import Order.Lexicographical
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set \hiding (#)
\data RingTerm (C V : \Type)
| coef C
| var V
| :zro
| :ide
| :negative (RingTerm C V)
| \infixl 6 :+ (t s : RingTerm C V)
| \infixl 7 :* (t s : RingTerm C V)
\class BaseData {C : Semiring} {S : LinearOrder.Dec C} {R : Semiring} (alg : SemiringHom C R) \extends CMonoidData {
| M => AbMonoid.toCMonoid R
| alg-comm (x : C) (y : R) : alg x R.* y = y R.* alg x
\field mData : MonoidData {R} vars
\func interpretRingNF (l : List (\Sigma (List V) C)) : R \elim l
| nil => 0
| :: x nil => alg x.2 * mData.interpretNF x.1
| :: x l => alg x.2 * mData.interpretNF x.1 + interpretRingNF l
\lemma cons (x : \Sigma (List V) C) (l : List (\Sigma (List V) C)) : interpretRingNF (x :: l) = alg x.2 * mData.interpretNF x.1 + interpretRingNF l \elim l
| nil => inv zro-right
| :: a l => idp
}
\class AlgData \extends BaseData {
| pnegative : R -> R
| negate : List (\Sigma (List V) C) -> List (\Sigma (List V) C)
| interpretNF_negate (l : List (\Sigma (List V) C)) : pnegative (interpretRingNF l) = interpretRingNF (negate l)
\func interpret (t : RingTerm C V) : R \elim t
| coef c => alg c
| var x => vars x
| :zro => 0
| :ide => 1
| :negative t => pnegative (interpret t)
| :+ t s => interpret t + interpret s
| :* t s => interpret t * interpret s
\lemma interpretRingNF_++ (l1 l2 : List (\Sigma (List V) C)) : interpretRingNF (l1 ++ l2) = interpretRingNF l1 + interpretRingNF l2 \elim l1
| nil => inv zro-left
| :: a l1 => run {
repeat {2} (rewrite BaseData.cons),
rewrite interpretRingNF_++,
inv +-assoc
}
\lemma interpretNF_map (a1 : C) (a2 a3 : List V) (l : List (\Sigma (List V) C)) : interpretRingNF (map (\lam b => (a2 ++ b.1 ++ a3, a1 * b.2)) l) = alg a1 * mData.interpretNF a2 * interpretRingNF l * mData.interpretNF a3 \elim l
| nil => inv (pmap (`* _) zro_*-right *> zro_*-left)
| :: a l => run {
repeat {2} (rewrite BaseData.cons),
repeat {2} (rewrite mData.interpretNF_++),
rewrite (alg.func-*, interpretNF_map, ldistr, rdistr),
pmap (`+ _) $ equation.monoid {alg-comm a.2 (mData.interpretNF a2)}
}
\lemma interpretNF_map-left (a1 : C) (a2 : List V) (l : List (\Sigma (List V) C)) : interpretRingNF (map (\lam b => (a2 ++ b.1, a1 * b.2)) l) = alg a1 * mData.interpretNF a2 * interpretRingNF l
=> inv (path (\lam i => interpretRingNF (map (\lam b => (a2 ++ (++_nil {_} {b.1} @ i), a1 * b.2)) l))) *> interpretNF_map a1 a2 nil l *> ide-right
\lemma interpretNF_multiply (l1 l2 : List (\Sigma (List V) C)) {acc : List (\Sigma (List V) C)} : interpretRingNF (multiply l1 l2 acc) = interpretRingNF l1 * interpretRingNF l2 + interpretRingNF acc \elim l1
| nil => rewrite zro_*-left (inv zro-left)
| :: a l1 => run {
rewrite (interpretNF_multiply, interpretRingNF_++),
rewriteI +-assoc,
pmap (`+ _),
later,
rewrite (BaseData.cons, rdistr, interpretNF_map-left),
+-comm
}
\lemma interpretNF_multiply' (l1 l2 : List (\Sigma (List V) C)) : interpretRingNF (multiply' l1 l2) = interpretRingNF l1 * interpretRingNF l2 \elim l2
| nil => inv zro_*-right
| :: a l2 => interpretNF_multiply l1 (a :: l2) *> zro-right
\lemma perm-consistent {l l' : List (\Sigma (List V) C)} (p : Perm l l') : interpretRingNF l = interpretRingNF l' \elim l, l', p
| nil, nil, perm-nil => idp
| :: a1 l1, :: a2 l2, perm-:: idp p => repeat {2} (rewrite BaseData.cons) (pmap (_ +) (perm-consistent p))
| :: a1 (:: a1' l1), :: a2 (:: a2' l2), perm-swap idp idp idp => repeat {2} (rewrite BaseData.cons) (inv +-assoc *> pmap (`+ interpretRingNF l1) +-comm *> +-assoc)
| l1, l2, perm-trans p1 p2 => perm-consistent p1 *> perm-consistent p2
\protected \lemma sort-consistent (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretRingNF (sort l)
=> rewrite (sort=insert l) (perm-consistent (Insertion.sort-perm l))
\func collapse1 (m : List V) (c : C) (l : List (\Sigma (List V) C)) : List (\Sigma (List V) C) \elim l
| nil => (m,c) :: nil
| :: a' l => \case decideEq m a'.1 \with {
| yes _ => collapse1 a'.1 (c + a'.2) l
| no _ => (m,c) :: collapse1 a'.1 a'.2 l
}
\func collapse (l : List (\Sigma (List V) C)) : List (\Sigma (List V) C)
| nil => nil
| :: a l => collapse1 a.1 a.2 l
\lemma collapse1-consistent (m : List V) (c : C) (l : List (\Sigma (List V) C)) : alg c * mData.interpretNF m + interpretRingNF l = interpretRingNF (collapse1 m c l) \elim l
| nil => zro-right
| :: a l => mcases \with {
| yes p => rewrite BaseData.cons $
inv +-assoc *>
pmap (`+ interpretRingNF l) (pmap (alg c * mData.interpretNF __ + _) p *> inv (pmap (`* _) alg.func-+ *> rdistr)) *>
collapse1-consistent a.1 (c + a.2) l
| no _ => repeat {2} (rewrite BaseData.cons) (pmap (_ +) (collapse1-consistent a.1 a.2 l))
}
\lemma collapse-consistent (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretRingNF (collapse l)
| nil => idp
| :: a l => rewrite BaseData.cons (collapse1-consistent a.1 a.2 l)
\func remove0 (l : List (\Sigma (List V) C)) : List (\Sigma (List V) C)
| nil => nil
| :: a l => \case decideEq a.2 zro \with {
| yes e => remove0 l
| no n => a :: remove0 l
}
\lemma remove0-consistent (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretRingNF (remove0 l)
| nil => idp
| :: a l => rewrite BaseData.cons $ mcases \with {
| yes e => rewrite e $ pmap (__ * _ + _) alg.func-zro *> pmap (`+ _) zro_*-left *> zro-left *> remove0-consistent l
| no n => rewrite BaseData.cons $ pmap (_ +) (remove0-consistent l)
}
\func normalize' (t : RingTerm C V) : List (\Sigma (List V) C) \elim t
| coef c => (nil, c) :: nil
| var v => (v :: nil, 1) :: nil
| :zro => nil
| :ide => (nil, 1) :: nil
| :negative t => negate (normalize' t)
| :+ t s => normalize' t ++ normalize' s
| :* t s => remove0 (collapse (multiply' (normalize' t) (normalize' s)))
\lemma normalize-consistent' (t : RingTerm C V) : interpret t = interpretRingNF (normalize' t)
| coef c => inv ide-right
| var v => rewrite alg.func-ide (inv ide-left)
| :zro => idp
| :ide => inv (ide-right *> alg.func-ide)
| :negative t => rewrite normalize-consistent' (interpretNF_negate (normalize' t))
| :+ t s => repeat {2} (rewrite normalize-consistent') (inv (interpretRingNF_++ (normalize' t) (normalize' s)))
| :* t s => repeat {2} (rewrite normalize-consistent') (inv (interpretNF_multiply' (normalize' t) (normalize' s)) *> collapse-consistent _ *> remove0-consistent _)
\func normalize (t : RingTerm C V) => remove0 (collapse (sort (normalize' t)))
\lemma normalizeList-consistent (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretRingNF (remove0 (collapse (sort l)))
=> sort-consistent _ *> collapse-consistent _ *> remove0-consistent _
\lemma normalize-consistent (t : RingTerm C V) : interpret t = interpretRingNF (normalize t)
=> normalize-consistent' t *> normalizeList-consistent _
\protected \lemma terms-equality (t s : RingTerm C V) (p : interpretRingNF (normalize t) = interpretRingNF (normalize s)) : interpret t = interpret s
=> normalize-consistent t *> p *> inv (normalize-consistent s)
\protected \lemma replace-consistent (list : List (\Sigma (List V) C)) (l r : RingTerm C V) (is : List Nat) (a b : List V) (c : C)
(p : interpretRingNF (remove0 (collapse (sort (CMonoidData.indices is list)))) = interpretRingNF (remove0 (collapse (sort (map (\lam t => (a ++ t.1 ++ b, c * t.2)) (normalize' l))))))
(rule : interpret l = interpret r)
: interpretRingNF list = interpretRingNF (map (\lam t => (a ++ t.1 ++ b, c * t.2)) (normalize' r) ++ CMonoidData.removeIndices is list)
=> replace-consistent-lem is list *>
interpretRingNF_++ _ _ *>
pmap (`+ _) (normalizeList-consistent _ *> p *> inv (normalizeList-consistent _) *> interpretNF_map c a b _ *> pmap (_ * __ * _) (inv (normalize-consistent' l) *> rule *> normalize-consistent' r) *> inv (interpretNF_map c a b _)) *>
inv (interpretRingNF_++ _ _)
\protected \lemma replace-consistent-lem (is : List Nat) (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretRingNF (CMonoidData.indices is l ++ CMonoidData.removeIndices is l)
| nil, l => idp
| :: 0 is, nil => idp
| :: (suc _) is, nil => idp
| :: 0 is, :: a l => repeat {2} (rewrite BaseData.cons) (pmap (_ +) (replace-consistent-lem is l))
| :: (suc n) is, :: a l => BaseData.cons a l *> pmap (_ +) (replace-consistent-lem (n :: is) l) *> inv (BaseData.cons a _) *> perm-consistent Perm.perm-head
} \where {
\open Sort
\open Sort.RedBlack
\func multiply' {V : \Type} {C : Monoid} (l1 l2 : List (\Sigma (List V) C)) : List (\Sigma (List V) C) \elim l2
| nil => nil
| l2 => multiply l1 l2 nil
\func multiply {V : \Type} {C : Monoid} (l1 l2 acc : List (\Sigma (List V) C)) : List (\Sigma (List V) C) \elim l1
| nil => acc
| :: a l1 => multiply l1 l2 (map (\lam b => (a.1 ++ b.1, a.2 * b.2)) l2 ++ acc)
}
\class CAlgData \extends AlgData {
\override R : CSemiring
\override mData : CMonoidData vars
| mData => \new CMonoidData
| alg-comm x y => *-comm
\func normalize (t : RingTerm C V) => remove0 (collapse (sort (map (\lam p => (sort p.1, p.2)) (normalize' t))))
\lemma map_sort-consistent (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretRingNF (map (\lam p => (sort p.1, p.2)) l)
| nil => idp
| :: a l => repeat {2} (rewrite BaseData.cons) $ pmap2 (_ * __ + __) (CMonoidData.sort-consistent {mData} a.1) (map_sort-consistent l)
\protected \lemma normalize-consistent (t : RingTerm C V) : interpret t = interpretRingNF (normalize t)
=> normalize-consistent' t *> map_sort-consistent _ *> normalizeList-consistent _
\protected \lemma terms-equality (t s : RingTerm C V) (p : interpretRingNF (normalize t) = interpretRingNF (normalize s)) : interpret t = interpret s
=> normalize-consistent t *> p *> inv (normalize-consistent s)
\protected \lemma replace-consistent (list : List (\Sigma (List V) C)) (l r : RingTerm C V) (is : List Nat) (a : List V) (c : C)
(p : interpretRingNF (remove0 (collapse (sort (map (\lam p => (sort p.1, p.2)) (CMonoidData.indices is list))))) = interpretRingNF (remove0 (collapse (sort (map (\lam t => (sort (a ++ t.1), c * t.2)) (normalize' l))))))
(rule : interpret l = interpret r)
: interpretRingNF list = interpretRingNF (map (\lam t => (a ++ t.1, c * t.2)) (normalize' r) ++ CMonoidData.removeIndices is list)
=> replace-consistent-lem is list *>
interpretRingNF_++ _ _ *>
pmap (`+ _) (map_sort-consistent _ *>
normalizeList-consistent _ *>
p *>
inv (normalizeList-consistent _) *>
pmap interpretRingNF (map_comp (\lam (t : \Sigma (List V) C) => (sort t.1, t.2)) (\lam t => (a ++ t.1, c * t.2)) (normalize' l)) *>
inv (map_sort-consistent _) *>
interpretNF_map-left c a _ *>
pmap (_ *) (inv (normalize-consistent' l) *> rule *> normalize-consistent' r) *>
inv (interpretNF_map-left c a _)) *>
inv (interpretRingNF_++ _ _)
} \where {
\open Sort.RedBlack
\open AlgData
}
\class SemiringData \extends AlgData
| C => NatSemiring
| S => NatSemiring
| alg => natMap
| alg-comm => natComm
| mData {}
| pnegative x => x
| negate x => x
| interpretNF_negate l => idp
\class CSemiringData \extends CAlgData, SemiringData
\class LatticeData (L : BoundedDistributiveLattice) \extends CAlgData {
| R => L
| C => BoundedDistributiveLattice.toSemiring BoolLattice
| S => BoolPoset
| alg {
| func => \case __ \with {
| false => bottom
| true => top
}
| func-+ {x} {y} => inv \case \elim x, \elim y \with {
| true, true => <=-antisymmetric top-univ join-left
| true, false => R.zro-right
| false, true => R.zro-left
| false, false => R.zro-left
}
| func-zro => idp
| func-ide => idp
| func-* {x} {y} => inv \case \elim x, \elim y \with {
| true, true => R.ide-left
| true, false => R.ide-left
| false, true => R.ide-right
| false, false => R.zro_*-left
}
}
| pnegative x => x
| negate x => x
| interpretNF_negate l => idp
\data ComparisonResult (l l' : List V)
| lessOrEquals (mData.interpretNF l ∨ mData.interpretNF l' = mData.interpretNF l)
| greater (mData.interpretNF l ∨ mData.interpretNF l' = mData.interpretNF l')
| uncomparable
\func compare (l l' : List V) : ComparisonResult l l'
| nil, _ => lessOrEquals (<=-antisymmetric top-univ join-left)
| :: a l, nil => greater (<=-antisymmetric top-univ join-right)
| :: a l, :: a' l' => \case trichotomy a a' \with {
| less a<a' => \case compare l (a' :: l') \with {
| greater p => greater $ rewrite (MonoidData.interpretNF.cons {mData}) (lattice-lem p)
| _ => uncomparable
}
| equals a=a' => \case compare l l' \with {
| lessOrEquals p => lessOrEquals $ rewriteI a=a' $ repeat {2} (rewrite (MonoidData.interpretNF.cons {mData})) (inv ldistr *> pmap (vars a ∧) p)
| greater p => greater $ rewrite a=a' $ repeat {2} (rewrite (MonoidData.interpretNF.cons {mData})) (inv ldistr *> pmap (vars a' ∧) p)
| uncomparable => uncomparable
}
| Order.LinearOrder.greater a>a' => \case compare (a :: l) l' \with {
| lessOrEquals p => lessOrEquals $ rewrite {2} (MonoidData.interpretNF.cons {mData}) (+-comm *> lattice-lem (+-comm *> p))
| _ => uncomparable
}
}
\func insert (m : List V) (l : List (List V)) : List (List V) \elim l
| nil => m :: nil
| :: a l => \case compare a m \with {
| lessOrEquals p => a :: l
| greater p => m :: l
| uncomparable => a :: insert m l
}
\lemma insert-consistent (m : List V) (l : List (List V)) : mData.interpretNF m ∨ interpretLatticeNF l = interpretLatticeNF (insert m l) \elim l
| nil => zro-right
| :: a l => mcases \with {
| lessOrEquals p => rewrite interpretLatticeNF.cons $ inv +-assoc *> pmap (`∨ _) (+-comm *> p)
| greater p => repeat {2} (rewrite interpretLatticeNF.cons) $ inv +-assoc *> pmap (`∨ _) (+-comm *> p)
| uncomparable => repeat {2} (rewrite interpretLatticeNF.cons) $ inv +-assoc *> pmap (`∨ _) +-comm *> +-assoc *> pmap (_ ∨) (insert-consistent m l)
}
\func collapse (l : List (List V)) : List (List V)
| nil => nil
| :: a l => insert a (collapse l)
\lemma collapse-consistent (l : List (List V)) : interpretLatticeNF l = interpretLatticeNF (collapse l)
| nil => idp
| :: a l => rewrite interpretLatticeNF.cons (pmap (_ ∨) (collapse-consistent l) *> insert-consistent a (collapse l))
\func remove0 (l : List (\Sigma (List V) C)) : List (List V)
| nil => nil
| :: (_,false) l => remove0 l
| :: (m,true) l => m :: remove0 l
\lemma remove0-consistent (l : List (\Sigma (List V) C)) : interpretRingNF l = interpretLatticeNF (remove0 l)
| nil => idp
| :: (_,false) l => rewrite BaseData.cons $ pmap (`∨ _) zro_*-left *> zro-left *> remove0-consistent l
| :: (_,true) l => rewrite (BaseData.cons, interpretLatticeNF.cons) $ pmap2 (∨) ide-left (remove0-consistent l)
\func interpretLatticeNF (l : List (List V)) : L \elim l
| nil => bottom
| :: x nil => mData.interpretNF x
| :: x l => mData.interpretNF x ∨ interpretLatticeNF l
\where
\lemma cons (x : List V) (l : List (List V)) : interpretLatticeNF (x :: l) = mData.interpretNF x ∨ interpretLatticeNF l \elim l
| nil => inv zro-right
| :: a l => idp
\func lData => \new LData { | L => L | vars => vars }
\func normalize (t : RingTerm C V) => sort (collapse (map (\lam l => LData.removeDuplicates {lData} (sort l)) (remove0 (normalize' t))))
\protected \lemma perm-consistent {l l' : List (List V)} (p : Perm l l') : interpretLatticeNF l = interpretLatticeNF l' \elim l, l', p
| nil, nil, perm-nil => idp
| :: a1 l1, :: a2 l2, perm-:: idp p => repeat {2} (rewrite interpretLatticeNF.cons) (pmap (_ +) (perm-consistent p))
| :: a1 (:: a1' l1), :: a2 (:: a2' l2), perm-swap idp idp idp => repeat {2} (rewrite interpretLatticeNF.cons) (inv +-assoc *> pmap (`+ interpretLatticeNF l1) +-comm *> +-assoc)
| l1, l2, perm-trans p1 p2 => perm-consistent p1 *> perm-consistent p2
\protected \lemma sort-consistent (l : List (List V)) : interpretLatticeNF l = interpretLatticeNF (sort l)
=> rewrite (sort=insert l) (perm-consistent (Insertion.sort-perm l))
\lemma map_sort-consistent (l : List (List V)) : interpretLatticeNF l = interpretLatticeNF (map sort l)
| nil => idp
| :: a l => repeat {2} (rewrite interpretLatticeNF.cons) $ pmap2 (+) (CMonoidData.sort-consistent {mData} a) (map_sort-consistent l)
\lemma map_removeDuplicates-consistent (l : List (List V)) : interpretLatticeNF l = interpretLatticeNF (map (LData.removeDuplicates {lData}) l)
| nil => idp
| :: a l => repeat {2} (rewrite interpretLatticeNF.cons) $ pmap2 (∨) (LData.removeDuplicates-consistent {lData} a) (map_removeDuplicates-consistent l)
\protected \lemma normalize-consistent (t : RingTerm C V) : interpret t = interpretLatticeNF (normalize t)
=> normalize-consistent' t *> remove0-consistent _ *> map_sort-consistent _ *> map_removeDuplicates-consistent _ *> inv (pmap interpretLatticeNF (map_comp (LData.removeDuplicates {lData}) sort _)) *> collapse-consistent _ *> sort-consistent _
\protected \lemma terms-equality (t s : RingTerm C V) (p : interpretLatticeNF (normalize t) = interpretLatticeNF (normalize s)) : interpret t = interpret s
=> normalize-consistent t *> p *> inv (normalize-consistent s)
} \where {
\open AlgData
\open Sort
\open Sort.RedBlack
\open LinearOrder
\lemma lattice-lem {L : BoundedLattice} {a b x : L} (p : a ∨ b = b) : x ∧ a ∨ b = b
=> JoinSemilattice.join_<= (<=-transitive meet-right (JoinSemilattice.join_<=' p))
}
\class BaseRingData \extends AlgData {
\override C : Ring
\override R : Ring
\override alg : RingHom C R
\default mData => \new MonoidData
| pnegative => negative
| negate => BaseRingData.negate
\default interpretNF_negate (l : List (\Sigma (List V) C)) : negative (interpretRingNF l) = interpretRingNF (negate l) \elim l {
| nil => AddGroup.negative_zro
| :: a l => repeat {2} (rewrite BaseData.cons) (AddGroup.negative_+ *> +-comm *> pmap2 (+) (inv (pmap (`* _) (AddGroupHom.func-negative {alg}) *> Ring.negative_*-left)) (interpretNF_negate l))
}
} \where {
\func negate {C : Ring} {V : \Type} (l : List (\Sigma (List V) C)) : List (\Sigma (List V) C) \elim l
| nil => nil
| :: (m,c) l => (m, negative c) :: negate l
}
\class RingData \extends BaseRingData
| C => IntRing
| S => IntRing
| alg => intMap
| alg-comm => intComm
\class RatData \extends BaseRingData
| C => RatField
| S => RatField
| R => RatField
| alg => RingHom.id
| alg-comm x y => RatField.*-comm
\class RatAlgebraData \extends BaseRingData {
| C => RatField
| S => RatField
\override R : AAlgebra RatField
| alg => AAlgebra.coefHom {R}
| alg-comm x y => pmap (`* _) coefMap_*c *> inv *c-comm-left *> pmap (x *c) (ide-left *> inv ide-right) *> *c-comm-right *> inv (pmap (y *) coefMap_*c)
}
\class CRingData \extends CAlgData, RingData {
\override R : CRing
\func normalize (t : RingTerm C V) => remove0 (collapse (sort (map (\lam p => (sort p.1, p.2)) (RingData.normalize' t))))
\protected \lemma normalize-consistent (t : RingTerm C V) : RingData.interpret t = interpretRingNF (normalize t)
=> RingData.normalize-consistent' t *> CAlgData.map_sort-consistent _ *> normalizeList-consistent _
\protected \lemma terms-equality (t s : RingTerm C V) (p : interpretRingNF (normalize t) = interpretRingNF (normalize s)) : RingData.interpret t = RingData.interpret s
=> normalize-consistent t *> p *> inv (normalize-consistent s)
\protected \lemma replace-consistent (list : List (\Sigma (List V) C)) (l r : RingTerm C V) (is : List Nat) (a : List V) (c : C)
(p : interpretRingNF (remove0 (collapse (sort (map (\lam p => (sort p.1, p.2)) (CMonoidData.indices is list))))) = interpretRingNF (remove0 (collapse (sort (map (\lam t => (sort (a ++ t.1), c * t.2)) (normalize' l))))))
(rule : interpret l = interpret r)
: interpretRingNF list = interpretRingNF (map (\lam t => (a ++ t.1, c * t.2)) (normalize' r) ++ CMonoidData.removeIndices is list)
=> replace-consistent-lem is list *>
interpretRingNF_++ _ _ *>
pmap (`+ _) (CAlgData.map_sort-consistent _ *>
normalizeList-consistent _ *>
p *>
inv (normalizeList-consistent _) *>
pmap interpretRingNF (map_comp (\lam (t : \Sigma (List V) C) => (sort t.1, t.2)) (\lam t => (a ++ t.1, c * t.2)) (normalize' l)) *>
inv (CAlgData.map_sort-consistent _) *>
interpretNF_map-left c a _ *>
pmap (_ *) (inv (normalize-consistent' l) *> rule *> normalize-consistent' r) *>
inv (interpretNF_map-left c a _)) *>
inv (interpretRingNF_++ _ _)
} \where {
\open AlgData
\open Sort.RedBlack
}
\func idealElem {R : CRing} (gensCoeffs : List (\Sigma (c : R) (gen : R))) : R
| nil => 0
| :: (c, gen) xs => c * gen + idealElem xs
\lemma gensZeroToIdealZero {R : CRing} (gensCoeffs : List (\Sigma (c : R) (gen : R) (gen = 0))) : idealElem (map (\lam x => (x.1, x.2)) gensCoeffs) = 0
| nil => idp
| :: (c, gen, p) xs => argsZeroToSumZero (inv (argZeroToProdZero c (inv p))) (inv (gensZeroToIdealZero xs))
\where {
\lemma argZeroToProdZero {R : CRing} (a : R) {b : R} (p : zro = b) : a * b = 0 => coe (\lam j => a * (p @ j) = 0) zro_*-right right
\lemma argsZeroToSumZero {R : CRing} {a b : R} (p : zro = a) (q : zro = b) : a + b = 0 => coe (\lam j => p @ j + q @ j = 0) zro-right right
}