Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Nat Nullify Test Athena
module Nat {
datatype N := zero | (S N)
declare +: [N N] -> N [200] # precedence 200
declare *: [N N] -> N [300] # precedence 300
declare **: [N N] -> N [400] # precedence 400
declare Nul: [N] -> N
# Some variables to use in definitions & proofs
define [n m x y] := [?n:N ?m:N ?x:N ?y:N]
define one := (S zero)
# Universally quantified definitions of addition, multiplication and exponentiation
assert* [
(n + S m = S (n + m))
(n + zero = n)
(x * zero = zero)
(x * (S y) = x * y + x)
(x ** zero = one)
(x ** S n = x * x ** n)
]
# Definitions of Nul function
assert* nul-axioms := [(Nul S n = Nul n) (Nul zero = zero)]
define [nul-n nul-z] := nul-axioms
# 8 ** 3
define eight-pow-3 := (Nul (** (S (S (S (zero)))) (S (S (S (S (S (S (S (S zero))))))))))
# Proof that forall Natural numbers, Nul n = zero
by-induction (forall n . Nul n = zero) {
zero => (!chain-> [
(Nul zero) = zero [nul-z]
])
| (S n) => let {ind-hypothesis := (Nul n = zero)}
conclude conc := (Nul (S n) = zero)
(!chain-> [
(Nul S n) = (Nul n) [nul-n]
= zero [ind-hypothesis]
])
}
# Proof that Nul 8 ** 3 = zero
(!chain [eight-pow-3 = zero [(forall n . Nul n = zero)] ])
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment