Create a gist now

Instantly share code, notes, and snippets.

@ssomayyajula /HA.idr
Last active Dec 29, 2016

What would you like to do?
Heyting arithmetic and Fast Integer Square Root in Idris
{- Heyting arithmetic and Fast Integer Square Root.
Author: Siva Somayyajula -}
induction : (P : Nat -> Type)
-> P Z
-> ((x : Nat) -> P x -> P (S x))
-> (n : Nat)
-> P n
induction P pz ps n = case n of
Z => pz
S n' => ps n' (induction P pz ps n')
natEq : (x, y, z : Nat) -> x = y -> x = z -> y = z
natEq _ _ _ Refl Refl = Refl
succPlusSucc : (x, y : Nat) -> x + S y = S (x + y)
succPlusSucc x y =
{- Proceed by induction on x -}
induction
(\x => x + S y = S (x + y))
{- Typechecker can infer Z + S y = S (Z + y) => S y = S y -}
Refl
{- Assuming x + S y = S (x + y), show S x + S y = S (S x + y).
Typechecker infers that S x + S y = S (S x + y) ~ S (x + S y) = S (S (x + y))
Proof:
We have
px : x + S y = S (x + y),
Refl : S (S (x + y)) = S (S (x + y)),
Given that sym px : S (x + y) = x + S y,
rewrite (sym px) in Refl replaces the first instance of
S (x + y) with x + S y in S (S (x + y)) = S (S (x + y))
to yield Refl : S (x + S y) = S (S (x + y)), as desired. -}
(\x => \px => rewrite (sym px) in Refl)
x
multPlusSucc : (x, y : Nat) -> x * S y = x * y + x
multPlusSucc x y =
{- Proof by induction on x. -}
induction
(\x => x * S y = x * y + x)
{- Typechecker can infer Z * S y = Z * y + Z => Z = Z -}
Refl
{- Assuming x * S y = x * y + x, show S x * S y = S x * y + S x.
Typechecker rewrites goal as S (y + x * S y) = (y + x * y) + S x,
and infers that Refl :
(y + x * y) + S x = (y + x * y) + S x
Transform the goal by the inductive hypothesis:
=> S (y + (x * y + x)) = (y + x * y) + S x
Use the theorem S (y + (x * y + x)) = y + S (x * y + x)
=> y + S (x * y + x) = (y + x * y) + S x
Use the theorem S (x * y + x) = x * y + S x
=> y + (x * y + S x) = (y + x * y) + S x
Use the theorem y + (x * y + S x) = (y + x * y) + S x
=> (y + x * y) + S x = (y + x * y) + S x
Since they're now the same type, their proof is reflexivity.
-}
(\x, px =>
rewrite px in
rewrite sym (succPlusSucc y (x * y + x)) in
rewrite sym (succPlusSucc (x * y) x) in
rewrite plusAssociative y (x * y) (S x) in
Refl)
x
notLteLt : {x, y : Nat} -> Not (x `LTE` y) -> y `LT` x
notLteLt {x} {y} =
induction
{- Proof by induction on x. -}
(\x => Not (x `LTE` y) -> y `LT` x)
{- Assume ~(0 <= y), but evidence for 0 <= y is given by LTEZero
Therefore by ex falso quodlibet (void), y `LT` x -}
(\nlte => void (nlte LTEZero))
{- Given
px : ~(x <= y) => y < x i.e. y + 1 <= x
nlte : ~(x + 1 <= y)
Show y < x + 1 i.e. y + 1 <= x + 1 i.e. y <= x.
Proof. Case analysis.
if ~(x <= y), apply the IH.
if y <= x => y < x + 1
-}
(\x, px, nlte =>
case (isLTE x y, isLTE y x) of
(No nlte', _) => lteSuccRight $ px nlte'
(_, Yes lte) => LTESucc lte
{- It's impossible for x <= y when the
assumption is ~(x <= y). -}
(Yes _, _) impossible)
x
{- forall n. exists r. r * r <= n < (r + 1) * (r + 1) -}
intSqrtPf : (n : Nat) -> (r : Nat ** ((r * r) `LTE` n, n `LT` (S r * S r)))
intSqrtPf n =
induction
{- Proof by induction on n. -}
(\n => (r : Nat ** ((r * r) `LTE` n, n `LT` (S r * S r))))
{- Base case: n = Z. Choose r = Z.
Z * Z <= Z and Z < 1 * 1, trivially.
Typechecker infers:
Z * Z <= Z => Z <= Z,
whose proof is LTEZero : Z `LTE` Z
Z < 1 * 1 => Z < 1,
whose proof is LTESucc LTEZero : 1 `LTE` 1 ~ Z `LT` 1 -}
(Z ** (LTEZero, LTESucc LTEZero))
{- Given
lte : r * r <= n
lt : n < (r + 1) * (r + 1) i.e. n + 1 <= r^2 + 2r + 1, show
exists r'. r' * r' <= n + 1 < (r' + 1) * (r' + 1)
Proof. By case analysis.
if (r + 1) * (r + 1) <= n + 1, then
r' = r + 1.
We get (r + 1) * (r + 1) <= n + 1 by the conditional.
If we add 1 to the LHS and 2r + 3 to the RHS of lt,
we get n + 1 < (r + 2) * (r + 2).
else
r' = r.
We get r * r <= n => r * r <= n + 1.
Since we know ~((r + 1) * (r + 1) <= n + 1),
we get n + 1 < (r + 1) * (r + 1). -}
(\n, (r ** (lte, lt)) =>
case isLTE (S r * S r) (S n) of
Yes lte' => (S r ** (lte',
let lt' =
LTESucc (lteTransitive lt (lteAddRight (S r * S r) {m = r + r})) in
let lt'' = lteSuccRight (lteSuccRight lt') in
{- Rewrite lt'' to match the goal type. -}
let lt1 =
replace {P = \x => LTE (S (S n)) (S (S (S (S x))))} (plusAssociative (r + r * S r) r r) lt'' in
let lt2 =
replace {P = \x => LTE (S (S n)) (S (S (S (S (x + r + r)))))} (sym (multRightSuccPlus r (S r))) lt1 in
let lt3 =
replace {P = \x => LTE (S (S n)) (S (S (S (S (x + r)))))} (plusCommutative (r * S (S r)) r) lt2 in
let lt4 =
replace {P = \x => LTE (S (S n)) (S (S (S (S x))))} (plusCommutative (r + r * S (S r)) r) lt3 in
let lt5 =
replace {P = \x => LTE (S (S n)) (S (S (S x)))} (plusSuccRightSucc r (r + r * S (S r))) lt4 in
let lt6 =
replace {P = \x => LTE (S (S n)) (S (S x))} (plusSuccRightSucc r (S (r + r * S (S r)))) lt5 in
lt6))
No nlte => (r ** (lteSuccRight lte, notLteLt nlte)))
n
intSqrt : Nat -> Nat
intSqrt n = fst (intSqrtPf n)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment