Grace/Cumulus/Algebra/Polynomial/Associativity.g17

Open in Workbench Download source

Imports

Terms

Declarations

Source

1-- Associativity of convolution by induction on finite sums of monomial terms.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.Associativity8import Terms910predicate PolynomialAssociates (I A add zero neg mul one p q r : Set) :=11  polynomialProduct(I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r) = polynomialProduct(I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r))1213def associatingFirsts (I A add zero neg mul one q r : Set) : Set :=14  {p ∈ polynomials(I, A, zero) | PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)}1516def associatingMiddles (I A add zero neg mul one p r : Set) : Set :=17  {q ∈ polynomials(I, A, zero) | PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)}1819def associatingThirds (I A add zero neg mul one p q : Set) : Set :=20  {r ∈ polynomials(I, A, zero) | PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)}2122section Rings23variable (I A add zero neg mul one : Set)24hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)2526theorem PolynomialAssociates.zero_first (q r : Set)27  requires memberQ : q ∈ polynomials(I, A, zero)28  requires memberR : r ∈ polynomials(I, A, zero)29  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), q, r)30proof31  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *32  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), q with *33  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *34  have left0 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, q with *35  have right0 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, q with *36  have left1 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, r with *37  have right1 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, r with *38  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *39  have left2 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *40  have right2 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *41  unfold PolynomialAssociates42  cc4344theorem PolynomialAssociates.zero_middle (p r : Set)45  requires memberP : p ∈ polynomials(I, A, zero)46  requires memberR : r ∈ polynomials(I, A, zero)47  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero), r)48proof49  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *50  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *51  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), r with *52  have left0 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, p with *53  have right0 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, p with *54  have left1 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, r with *55  have right1 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, r with *56  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *57  have left2 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *58  have right2 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *59  unfold PolynomialAssociates60  cc6162theorem PolynomialAssociates.zero_third (p q : Set)63  requires memberP : p ∈ polynomials(I, A, zero)64  requires memberQ : q ∈ polynomials(I, A, zero)65  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, constantFunction(monomials(I), A, zero))66proof67  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *68  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *69  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, constantFunction(monomials(I), A, zero) with *70  have left0 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, p with *71  have right0 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, p with *72  have left1 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, q with *73  have right1 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, q with *74  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *75  have left2 := polynomialProduct.zero_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q) with *76  have right2 := polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q) with *77  unfold PolynomialAssociates78  cc7980theorem PolynomialAssociates.add_first (p q r s : Set)81  requires memberP : p ∈ polynomials(I, A, zero)82  requires memberQ : q ∈ polynomials(I, A, zero)83  requires memberR : r ∈ polynomials(I, A, zero)84  requires memberS : s ∈ polynomials(I, A, zero)85  requires first : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)86  requires second : PolynomialAssociates(I, A, add, zero, neg, mul, one, s, q, r)87  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, s), q, r)88proof89  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *90  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *91  have pair2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, s, q with *92  have distribute0 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, p, s, q with *93  have distribute1 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, s, q), r with *94  have distribute2 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, p, s, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *95  unfold PolynomialAssociates at first96  unfold PolynomialAssociates at second97  unfold PolynomialAssociates98  cc99100theorem PolynomialAssociates.add_middle (p q r s : Set)101  requires memberP : p ∈ polynomials(I, A, zero)102  requires memberQ : q ∈ polynomials(I, A, zero)103  requires memberR : r ∈ polynomials(I, A, zero)104  requires memberS : s ∈ polynomials(I, A, zero)105  requires first : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)106  requires second : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, s, r)107  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, s), r)108proof109  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *110  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, s with *111  have pair2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *112  have pair3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, s, r with *113  have distribute0 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, q, s with *114  have distribute1 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, s), r with *115  have distribute2 := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, q, s, r with *116  have distribute3 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r), polynomialProduct(I, A, add, zero, neg, mul, one, s, r) with *117  unfold PolynomialAssociates at first118  unfold PolynomialAssociates at second119  unfold PolynomialAssociates120  cc121122theorem PolynomialAssociates.add_third (p q r s : Set)123  requires memberP : p ∈ polynomials(I, A, zero)124  requires memberQ : q ∈ polynomials(I, A, zero)125  requires memberR : r ∈ polynomials(I, A, zero)126  requires memberS : s ∈ polynomials(I, A, zero)127  requires first : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, r)128  requires second : PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, s)129  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, p, q, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, r, s))130proof131  have pair0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *132  have pair1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *133  have pair2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, s with *134  have distribute0 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r, s with *135  have distribute1 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, q, r, s with *136  have distribute2 := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, s) with *137  unfold PolynomialAssociates at first138  unfold PolynomialAssociates at second139  unfold PolynomialAssociates140  cc141142theorem PolynomialAssociates.terms (a b c m n k : Set)143  requires coefficientA : a ∈ A144  requires coefficientB : b ∈ A145  requires coefficientC : c ∈ A146  requires monomialM : m ∈ monomials(I)147  requires monomialN : n ∈ monomials(I)148  requires monomialK : k ∈ monomials(I)149  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n), polynomialTerm(I, A, zero, c, k))150proof151  have ordinary := IsCommRing.ring with ring152  have ab := IsRing.mul_closed at A, add, zero, neg, mul, one, a, b with *153  have bc := IsRing.mul_closed at A, add, zero, neg, mul, one, b, c with *154  have mn := monomialProduct.member at I, m, n with *155  have nk := monomialProduct.member at I, n, k with *156  have product0 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, b, m, n with *157  have product1 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, b, c, n, k with *158  have product2 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, call2(mul, a, b), c, monomialProduct(I, m, n), k with *159  have product3 := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, call2(mul, b, c), m, monomialProduct(I, n, k) with *160  have coefficients : call2(mul, call2(mul, a, b), c) = call2(mul, a, call2(mul, b, c)) by ring161  have monomials := monomialProduct.associative at I, m, n, k with *162  unfold PolynomialAssociates163  cc164165theorem PolynomialAssociates.two_terms (a b m n r : Set)166  requires coefficientA : a ∈ A167  requires coefficientB : b ∈ A168  requires monomialM : m ∈ monomials(I)169  requires monomialN : n ∈ monomials(I)170  requires memberR : r ∈ polynomials(I, A, zero)171  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n), r)172proof173  have ordinary := IsCommRing.ring with ring174  have zeroIn := IsRing.zero_in_carrier with ordinary175  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *176  have termA := polynomialTerm.member at I, A, zero, a, m with *177  have termB := polynomialTerm.member at I, A, zero, b, n with *178  have base : constantFunction(monomials(I), A, zero) ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))179    apply associatingThirds.membership.backward180    constructor181    . exact zeroPolynomial182    . exact PolynomialAssociates.zero_third with *183  have terms : ∀ d ∈ A, ∀ j ∈ monomials(I), polynomialTerm(I, A, zero, d, j) ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))184    intros d hd j hj185    have member := polynomialTerm.member at I, A, zero, d, j with *186    apply associatingThirds.membership.backward187    constructor188    . exact member189    . exact PolynomialAssociates.terms with *190  have sums : ∀ f ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), ∀ g ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))191    intros f hf g hg192    have first := associatingThirds.membership.forward with hf193    have second := associatingThirds.membership.forward with hg194    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *195    apply associatingThirds.membership.backward196    constructor197    . exact member198    . exact PolynomialAssociates.add_third with *199  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, associatingThirds(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), r with *200  have result := associatingThirds.membership.forward with generated201  exact result.right202203theorem PolynomialAssociates.one_term (a m q r : Set)204  requires coefficientA : a ∈ A205  requires monomialM : m ∈ monomials(I)206  requires memberQ : q ∈ polynomials(I, A, zero)207  requires memberR : r ∈ polynomials(I, A, zero)208  shows PolynomialAssociates(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), q, r)209proof210  have ordinary := IsCommRing.ring with ring211  have zeroIn := IsRing.zero_in_carrier with ordinary212  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *213  have termA := polynomialTerm.member at I, A, zero, a, m with *214  have base : constantFunction(monomials(I), A, zero) ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r)215    apply associatingMiddles.membership.backward216    constructor217    . exact zeroPolynomial218    . exact PolynomialAssociates.zero_middle with *219  have terms : ∀ d ∈ A, ∀ j ∈ monomials(I), polynomialTerm(I, A, zero, d, j) ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r)220    intros d hd j hj221    have member := polynomialTerm.member at I, A, zero, d, j with *222    apply associatingMiddles.membership.backward223    constructor224    . exact member225    . exact PolynomialAssociates.two_terms with *226  have sums : ∀ f ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r), ∀ g ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r)227    intros f hf g hg228    have first := associatingMiddles.membership.forward with hf229    have second := associatingMiddles.membership.forward with hg230    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *231    apply associatingMiddles.membership.backward232    constructor233    . exact member234    . exact PolynomialAssociates.add_middle with *235  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, associatingMiddles(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), r), q with *236  have result := associatingMiddles.membership.forward with generated237  exact result.right238239theorem polynomialProduct.associative (p q r : Set)240  requires memberP : p ∈ polynomials(I, A, zero)241  requires memberQ : q ∈ polynomials(I, A, zero)242  requires memberR : r ∈ polynomials(I, A, zero)243  shows polynomialProduct(I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r) = polynomialProduct(I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r))244proof245  have ordinary := IsCommRing.ring with ring246  have zeroIn := IsRing.zero_in_carrier with ordinary247  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *248  have base : constantFunction(monomials(I), A, zero) ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r)249    apply associatingFirsts.membership.backward250    constructor251    . exact zeroPolynomial252    . exact PolynomialAssociates.zero_first with *253  have terms : ∀ d ∈ A, ∀ j ∈ monomials(I), polynomialTerm(I, A, zero, d, j) ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r)254    intros d hd j hj255    have member := polynomialTerm.member at I, A, zero, d, j with *256    apply associatingFirsts.membership.backward257    constructor258    . exact member259    . exact PolynomialAssociates.one_term with *260  have sums : ∀ f ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r), ∀ g ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ associatingFirsts(I, A, add, zero, neg, mul, one, q, r)261    intros f hf g hg262    have first := associatingFirsts.membership.forward with hf263    have second := associatingFirsts.membership.forward with hg264    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *265    apply associatingFirsts.membership.backward266    constructor267    . exact member268    . exact PolynomialAssociates.add_first with *269  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, associatingFirsts(I, A, add, zero, neg, mul, one, q, r), p with *270  have result := associatingFirsts.membership.forward with generated271  exact result.right272273end Rings274