{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Nat where open import Agda.Builtin.Bool data Nat : Set where zero : Nat suc : (n : Nat) → Nat {-# BUILTIN NATURAL Nat #-} infix 4 _==_ _<_ infixl 6 _+_ _-_ infixl 7 _*_ _+_ : Nat → Nat → Nat zero + m = m suc n + m = suc (n + m) {-# BUILTIN NATPLUS _+_ #-} _-_ : Nat → Nat → Nat n - zero = n zero - suc m = zero suc n - suc m = n - m {-# BUILTIN NATMINUS _-_ #-} _*_ : Nat → Nat → Nat zero * m = zero suc n * m = m + n * m {-# BUILTIN NATTIMES _*_ #-} _==_ : Nat → Nat → Bool zero == zero = true suc n == suc m = n == m _ == _ = false {-# BUILTIN NATEQUALS _==_ #-} _<_ : Nat → Nat → Bool _ < zero = false zero < suc _ = true suc n < suc m = n < m {-# BUILTIN NATLESS _<_ #-} -- Helper function div-helper for Euclidean division. --------------------------------------------------------------------------- -- -- div-helper computes n / 1+m via iteration on n. -- -- n div (suc m) = div-helper 0 m n m -- -- The state of the iterator has two accumulator variables: -- -- k: The quotient, returned once n=0. Initialized to 0. -- -- j: A counter, initialized to the divisor m, decreased on each iteration step. -- Once it reaches 0, the quotient k is increased and j reset to m, -- starting the next countdown. -- -- Under the precondition j ≤ m, the invariant is -- -- div-helper k m n j = k + (n + m - j) div (1 + m) div-helper : (k m n j : Nat) → Nat div-helper k m zero j = k div-helper k m (suc n) zero = div-helper (suc k) m n m div-helper k m (suc n) (suc j) = div-helper k m n j {-# BUILTIN NATDIVSUCAUX div-helper #-} -- Proof of the invariant by induction on n. -- -- clause 1: div-helper k m 0 j -- = k by definition -- = k + (0 + m - j) div (1 + m) since m - j < 1 + m -- -- clause 2: div-helper k m (1 + n) 0 -- = div-helper (1 + k) m n m by definition -- = 1 + k + (n + m - m) div (1 + m) by induction hypothesis -- = 1 + k + n div (1 + m) by simplification -- = k + (n + (1 + m)) div (1 + m) by expansion -- = k + (1 + n + m - 0) div (1 + m) by expansion -- -- clause 3: div-helper k m (1 + n) (1 + j) -- = div-helper k m n j by definition -- = k + (n + m - j) div (1 + m) by induction hypothesis -- = k + ((1 + n) + m - (1 + j)) div (1 + m) by expansion -- -- Q.e.d. -- Helper function mod-helper for the remainder computation. --------------------------------------------------------------------------- -- -- (Analogous to div-helper.) -- -- mod-helper computes n % 1+m via iteration on n. -- -- n mod (suc m) = mod-helper 0 m n m -- -- The invariant is: -- -- m = k + j ==> mod-helper k m n j = (n + k) mod (1 + m). mod-helper : (k m n j : Nat) → Nat mod-helper k m zero j = k mod-helper k m (suc n) zero = mod-helper 0 m n m mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j {-# BUILTIN NATMODSUCAUX mod-helper #-} -- Proof of the invariant by induction on n. -- -- clause 1: mod-helper k m 0 j -- = k by definition -- = (0 + k) mod (1 + m) since m = k + j, thus k < m -- -- clause 2: mod-helper k m (1 + n) 0 -- = mod-helper 0 m n m by definition -- = (n + 0) mod (1 + m) by induction hypothesis -- = (n + (1 + m)) mod (1 + m) by expansion -- = (1 + n) + k) mod (1 + m) since k = m (as l = 0) -- -- clause 3: mod-helper k m (1 + n) (1 + j) -- = mod-helper (1 + k) m n j by definition -- = (n + (1 + k)) mod (1 + m) by induction hypothesis -- = ((1 + n) + k) mod (1 + m) by commutativity -- -- Q.e.d.