Grace/Cumulus/Algebra/Ring/Numeral.g17

Open in Workbench Download source

Imports

Core · Nat.Core

Declarations

Source

1-- Natural numbers inside a ring: ringNat(add, zero, one, n) is the n-fold sum2-- of one. Scoped ring numerals above 1 elaborate to it, and the ring tactic3-- adds and multiplies such coefficients through the laws proved here.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Ring.Numeral10import Core11import Nat.Core1213def ringNat (plus z u : Set, n : Nat) → Set14  | plus, z, u, zero => z15  | plus, z, u, succ(k) => plus(ringNat(plus, z, u, k), u)1617theorem ringNat.zero (add zero one : Set)18  shows ringNat(add, zero, one, 0) = zero19proof20  simp [ringNat]2122theorem ringNat.succ (add zero one : Set, n : Nat)23  shows ringNat(add, zero, one, succ(n)) =24    call2(add, ringNat(add, zero, one, n), one)25proof26  simp [ringNat]2728theorem IsRing.numeral_closed (A add zero neg mul one : Set, n : Nat)29  requires ring : IsRing(A, add, zero, neg, mul, one)30  shows ringNat(add, zero, one, n) ∈ A31proof32  induction n33  | zero =>34    rw ringNat.zero35    exact IsRing.zero_in_carrier with ring36  | succ(k) using ih =>37    have monoid := IsRing.multiplicative with ring38    have oneInA := IsMonoid.unit_in_carrier with monoid39    rw ringNat.succ40    exact IsRing.add_closed with ring, ih, oneInA4142theorem IsRing.numeral_one (A add zero neg mul one : Set)43  requires ring : IsRing(A, add, zero, neg, mul, one)44  shows ringNat(add, zero, one, 1) = one45proof46  have monoid := IsRing.multiplicative with ring47  have oneInA := IsMonoid.unit_in_carrier with monoid48  simp [ringNat]49  exact IsRing.add_left_identity with ring, oneInA5051theorem IsCommRing.numeral_add (A add zero neg mul one : Set, m n : Nat)52  requires ring : IsCommRing(A, add, zero, neg, mul, one)53  shows ringNat(add, zero, one, m + n) =54    call2(add, ringNat(add, zero, one, m), ringNat(add, zero, one, n))55proof56  induction n57  | zero =>58    have ordinary := IsCommRing.ring with ring59    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m60      with ordinary61    rw [add.right_unit, ringNat.zero]62    have rightIdentity := IsRing.add_right_identity with ordinary, mInA63    rw rightIdentity64    rfl65  | succ(k) using ih =>66    have ordinary := IsCommRing.ring with ring67    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m68      with ordinary69    have kInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, k70      with ordinary71    have monoid := IsRing.multiplicative with ordinary72    have oneInA := IsMonoid.unit_in_carrier with monoid73    rw [add.succ_right, ringNat.succ, ringNat.succ, ih]74    have reassociate := IsCommRing.add_assoc with ring, mInA, kInA, oneInA75    rw reassociate76    rfl7778theorem IsCommRing.numeral_mul (A add zero neg mul one : Set, m n : Nat)79  requires ring : IsCommRing(A, add, zero, neg, mul, one)80  shows ringNat(add, zero, one, m * n) =81    call2(mul, ringNat(add, zero, one, m), ringNat(add, zero, one, n))82proof83  induction n84  | zero =>85    have ordinary := IsCommRing.ring with ring86    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m87      with ordinary88    rw [mul.right_zero, ringNat.zero]89    have annihilate := IsRing.mul_zero with ordinary, mInA90    rw annihilate91    rfl92  | succ(k) using ih =>93    have ordinary := IsCommRing.ring with ring94    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m95      with ordinary96    have kInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, k97      with ordinary98    have monoid := IsRing.multiplicative with ordinary99    have oneInA := IsMonoid.unit_in_carrier with monoid100    have productInA := IsRing.mul_closed with ordinary, mInA, kInA101    rw [mul.succ_right, ringNat.succ]102    have split := IsCommRing.numeral_add at A, add, zero, neg, mul, one, m,103      m * k104      with ring105    rw [split, ih]106    have distribute := IsCommRing.mul_add with ring, mInA, kInA, oneInA107    have unit := IsCommRing.one_right with ring, mInA108    have commute := IsCommRing.add_comm with ring, mInA, productInA109    rw [distribute, unit, commute]110    rfl111