Grace/Core/Nat/Algebra.g17

Open in Workbench Download source

Imports

Grace.Core.Nat

Declarations

• add.right_unit theorem derivation
• add.succ_right theorem derivation
• add.right_one theorem derivation
• add.associative theorem derivation
• add.associative_reverse theorem derivation
• add.commutative theorem derivation
• add.successor_shift theorem derivation
• add.swap theorem derivation
• add.closed theorem derivation
• mul.right_zero theorem derivation
• mul.left_unit theorem derivation
• mul.right_unit theorem derivation
• mul.succ_right theorem derivation
• mul.commutative theorem derivation
• mul.closed theorem derivation
• mul.distributes_right theorem derivation
• mul.distributes_left theorem derivation
• mul.associative theorem derivation

Source

1-- Natural-number algebra2-- Part of the Grace17 proof assistant for mathematics based on set theory.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.Core.Nat.Algebra8namespace Grace.Core.Nat.Algebra9import Grace.Core.Nat10export open Grace.Core.Nat.Algebra1112theorem add.right_unit (n : Nat)13  shows add(n, 0) = n14proof15  induction n16  | zero => settle with add17  | succ(k) using ih => settle with add, ih1819theorem add.succ_right (m : Set, n : Nat)20  shows add(n, succ(m)) = succ(add(n, m))21proof22  induction n23  | zero => settle with add24  | succ(k) using ih => settle with add, ih2526theorem add.right_one (n : Nat)27  shows add(n, 1) = succ(n)28proof29  simp [add.succ_right, add.right_unit]3031theorem add.associative (y z : Set, n : Nat)32  shows add(add(n, y), z) = add(n, add(y, z))33proof34  induction n35  | zero => settle with add36  | succ(k) using ih => settle with add, ih3738theorem add.associative_reverse (y z : Set, n : Nat)39  shows add(n, add(y, z)) = add(add(n, y), z)40proof41  simp [add.associative]4243theorem add.commutative (y n : Nat)44  shows add(n, y) = add(y, n)45proof46  induction n47  | zero => settle with add, add.right_unit48  | succ(k) using ih => settle with add, add.succ_right, ih4950theorem add.successor_shift (a k : Nat)51  shows add(a, succ(k)) = add(succ(a), k)52proof53  simp [add.succ_right, add]5455theorem add.swap (b : Nat, c : Set, a : Nat)56  shows add(a, add(b, c)) = add(b, add(a, c))57proof58  induction a59  | zero => settle with add60  | succ(k) using ih => settle with add, add.succ_right, ih6162theorem add.closed (y : Nat, x : Nat)63  shows Nat(add(x, y))64proof65  induction x66  | zero => settle with add67  | succ(k) using ih => settle with add, Naturals.constructor.succ, ih6869theorem mul.right_zero (n : Nat)70  shows mul(n, 0) = 071proof72  induction n73  | zero => settle with mul74  | succ(k) using ih => settle with mul, add, ih7576theorem mul.left_unit (n : Nat)77  shows mul(1, n) = n78proof79  simp [mul, add, add.right_unit]8081theorem mul.right_unit (n : Nat)82  shows mul(n, 1) = n83proof84  induction n85  | zero => settle with mul86  | succ(k) using ih => settle with mul, add, ih8788theorem mul.succ_right (y n : Nat)89  shows mul(n, succ(y)) = add(n, mul(n, y))90proof91  induction n92  | zero => settle with mul, add93  | succ(k) using ih => settle with mul, add, add.swap, ih9495theorem mul.commutative (y n : Nat)96  shows mul(n, y) = mul(y, n)97proof98  induction n99  | zero => settle with mul, mul.right_zero100  | succ(k) using ih => settle with mul, mul.succ_right, ih101102theorem mul.closed (y : Nat, x : Nat)103  shows Nat(mul(x, y))104proof105  induction x106  | zero => settle with mul, Naturals.constructor.zero107  | succ(k) using ih => settle with mul, add.closed, ih108109theorem mul.distributes_right (y z : Nat, n : Nat)110  shows mul(add(n, y), z) = add(mul(n, z), mul(y, z))111proof112  induction n113  | zero => settle with add, mul114  | succ(k) using ih => settle with add, mul, add.associative, ih115116theorem mul.distributes_left (y z : Nat, x : Nat)117  shows mul(x, add(y, z)) = add(mul(x, y), mul(x, z))118proof119  induction x120  | zero => settle with add, mul121  | succ(k) using ih => settle with mul, add.associative, add.swap, mul.closed, ih122123theorem mul.associative (y z : Nat, x : Nat)124  shows mul(mul(x, y), z) = mul(x, mul(y, z))125proof126  induction x127  | zero => settle with mul128  | k + 1 using ih => settle with mul, mul.distributes_right, mul.closed, ih129130end Grace.Core.Nat.Algebra131