Skip to content

Instantly share code, notes, and snippets.

@donovancrichton
Last active February 26, 2020 09:19
Show Gist options
  • Save donovancrichton/b11b675be1e079e4d2ccd9611e0caa6f to your computer and use it in GitHub Desktop.
Save donovancrichton/b11b675be1e079e4d2ccd9611e0caa6f to your computer and use it in GitHub Desktop.
Proving extensionally equivalent fibonacci functions using Idris
%default total
||| A stream (an infinite list) of natural numbers representing the
||| fibbonacci sequence.
fibs : Stream Nat
fibs = f 0 1
where
f : Nat -> Nat -> Stream Nat
f a b = a :: f b (a + b)
||| A constructive proof that forall natural numbers 'n', and
||| some stream 'xs', the length of the list derived by
||| taking the first n + 1 elements of 'xs' is always greater than 'n'.
nAlwaysLteSn : (n : Nat) -> (xs : Stream a) ->
LTE (S n) (length (Stream.take (S n) xs))
nAlwaysLteSn Z (value :: xs) = lteRefl
nAlwaysLteSn (S k) (value :: xs) =
let rec = nAlwaysLteSn k xs
in LTESucc rec
||| A constructive proof that forall natural numbers 'n' and some
||| list 'xs'. Given a proof that n < the length of 'xs'. Then n is
||| a valid index into 'xs'.
ltLenAlwaysBound : (n : Nat) -> (xs : List a) ->
(prf : LTE (S n) (length xs)) -> InBounds n xs
ltLenAlwaysBound Z [] prf = absurd prf
ltLenAlwaysBound Z (x :: xs) prf = InFirst
ltLenAlwaysBound (S k) [] prf = absurd prf
ltLenAlwaysBound (S k) (x :: xs) prf =
let rec = ltLenAlwaysBound k xs
in InLater (rec (fromLteSucc prf))
||| A function that returns the fibonacci term at index 'n'.
fib' : Nat -> Nat
fib' n =
let p1 = nAlwaysLteSn n fibs
xs = take (S n) fibs
p2 = ltLenAlwaysBound n xs p1
in List.index n (take (S n) fibs) {ok = p2}
||| A second function that returns the fibonacci term at index 'n'.
fib'' : Nat -> Nat
fib'' n = f n 0 1
where
f : Nat -> Nat -> Nat -> Nat
f Z a b = a
f (S k) a b = f k b (a + b)
||| An axiom of functional extensionality.
||| (two functions are equal if they "do the same thing").
postulate
functional_extensionality : {a, b : Type} -> {f, g : a -> b} ->
(prf : (x : a) -> f x = g x) -> f = g
fibIsFib : (\x => fib'' x) = (\x => fib' x)
fibIsFib = functional_extensionality $ \x => ?test
-- Gives the following type error:
-- 56 | fibIsFib = functional_extensionality $ \x => ?test
-- | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- When checking deferred type of Main.test:
-- Type mismatch between
-- LTE (S x1) (S (length (take x1 (Main.fibs, f 1 1))))
-- and
-- LTE (S x1) (S (length (take x1 (1 :: Delay (Main.fibs, f 1 2)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment