git.iko.soy/Idris-dev
on master help sign in
Add non-zero restriction to gcd
d89f3faFabian Heredia Montiel
libs/prelude/Prelude/Nat.idr+13−8
compare with master
unifiedsplit
@@ -91,6 +91,12 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
91-- Comparisons
91-- Comparisons
92--------------------------------------------------------------------------------
92--------------------------------------------------------------------------------
93
93
94+||| Proofs that `n` or `m` is not equal to Z
95+data NotBothZero : (n, m : Nat) -> Type where
96+ LeftIsNotZero : NotBothZero (S n) m
97+ RightIsNotZero : NotBothZero n (S m)
98+
99+
94||| Proofs that `n` is less than or equal to `m`
100||| Proofs that `n` is less than or equal to `m`
95||| @ n the smaller number
101||| @ n the smaller number
96||| @ m the larger number
102||| @ m the larger number
@@ -386,16 +392,15 @@ log2 (S n) = log2NZ (S n) SIsNotZ
386--------------------------------------------------------------------------------
392--------------------------------------------------------------------------------
387-- GCD and LCM
393-- GCD and LCM
388--------------------------------------------------------------------------------
394--------------------------------------------------------------------------------
389−partial
390−gcd : Nat -> Nat -> Nat
395+gcd : (a: Nat) -> (b: Nat) -> .{auto ok: NotBothZero a b} -> Nat
391−gcd a Z = a
396+gcd a Z = a
397+gcd Z b = b
392−gcd a b = assert_total (gcd b (a `modNat` b))
398+gcd a (S b) = assert_total $ gcd (S b) (modNatNZ a (S b) SIsNotZ)
393
399
394−partial
395lcm : Nat -> Nat -> Nat
400lcm : Nat -> Nat -> Nat
396−lcm _ Z = Z
401+lcm _ Z = Z
397−lcm Z _ = Z
402+lcm Z _ = Z
398−lcm x y = divNat (x * y) (gcd x y)
403+lcm a (S b) = assert_total $ divNat (a * (S b)) (gcd a (S b))
399
404
400
405
401--------------------------------------------------------------------------------
406--------------------------------------------------------------------------------