Arithmetic

Arithmetic examples

Open in Workbench View on GitHub

1-- Arithmetic examples2-- 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 Passmore67-- The first executable GRACE17 surface module.89def plus (x y : Nat) -> Nat10  | zero, y => y11  | succ(x), y => succ(plus(x, y))1213notation infixl 60 "+" => plus1415theorem plus.left_unit (n : Set)16  shows 0 + n = n17proof18  simp [plus]1920theorem plus.right_unit (n : Nat)21  shows n + 0 = n22proof23  induction n24  | zero => settle with plus25  | succ(k) using ih => settle with plus, ih2627theorem plus.succ_right (m : Set, n : Nat)28  shows n + succ(m) = succ(n + m)29proof30  induction n31  | zero => settle with plus32  | succ(k) using ih => settle with plus, ih3334theorem plus.associative (y z : Set, n : Nat)35  shows (n + y) + z = n + (y + z)36proof37  induction n38  | zero => settle with plus39  | succ(k) using ih => settle with plus, ih4041theorem plus.commutative (y n : Nat)42  shows n + y = y + n43proof44  induction n45  | zero => settle with plus, plus.right_unit46  | succ(k) using ih => settle with plus, plus.succ_right, ih4748theorem plus.swap (b : Nat, c : Set, a : Nat)49  shows a + (b + c) = b + (a + c)50proof51  induction a52  | zero => settle with plus53  | succ(k) using ih => settle with plus, plus.succ_right, ih5455def times (x y : Nat) -> Nat56  | zero, y => zero57  | succ(x), y => y + times(x, y)5859notation infixl 70 "*" => times6061theorem times.right_zero (n : Nat)62  shows n * 0 = 063proof64  induction n65  | zero => settle with times66  | succ(k) using ih => settle with times, plus, ih6768theorem times.succ_right (y n : Nat)69  shows n * succ(y) = n + n * y70proof71  induction n72  | zero => settle with times, plus73  | succ(k) using ih => settle with times, plus, plus.swap, ih7475theorem times.commutative (y n : Nat)76  shows n * y = y * n77proof78  induction n79  | zero => settle with times, times.right_zero80  | succ(k) using ih => settle with times, times.succ_right, ih8182theorem times.distributes_right (y z n : Nat)83  shows (n + y) * z = n * z + y * z84proof85  induction n86  | zero => settle with plus, times87  | succ(k) using ih => settle with plus, times, plus.associative, ih8889-- Hundreds of reductions, but exactly one kernel proof node.90theorem times.ground_70091  shows 7 * 100 = 70092proof93  compute9495-- A value beyond JavaScript's safe-integer range. The source term, checked96-- computation certificate, and machine term each contain compact decimals.97eval 7000000000 * 10000000009899theorem times.ground_bigint100  shows 7000000000 * 1000000000 = 7000000000000000000101proof102  compute103