Idris2 proofs of leftPad and fulcrum from the Great theorem prover showdown. https://www.hillelwayne.com/post/theorem-prover-showdown/
An attempt was made to make readable proofs which can be easily followed.
Some final observations:
-
idris2 is not made for intrinsics proofs, even though it provides facilities for it. It can be felt in the way the standard library is organised. Some proofs are missing (proofs about Int, about some list functions), the proofs feel a bit disorganized.
-
These challenges seem to be picked out for imperative approaches, most of the time you don't work with indexes or lengths in functional programming, but rather use higher abstractions.
-
unlike the imperative counterpart, both leftPad and fulcrum's functional implementation can be easily seen as correct by a quick glance. I would never go to such lengths to prove these correct, even a quick test on the repl should give enough confidence for these functions. On the other hand, the imperative impementation is harder to follow, can possibly have off by one errors (the spec even had an off by one error!). Proving seems to yield more benifits for the imperative part.
-
The proofs in dafny are quite concise, however they are not really that easy to follow. They are also not giving insights in the problem domain. On the other hand, the proofs giving here can be easily reused, and also give more insights in how to reason about code. You could build a library of proofs, which you can reuse for other problems.
-
Often a hard proof can become easy by making slight alterations to the function body, or by trying a slightly different proof. For example, I had a hard time with range, until I rewrote it in terms of rangeAux, after which the proofs became trivial.
-
Rewriting bodies in idris2 can be a big pain, it often amounts to trial and error with rearranging view patterns. rewrite makes it a lot easier, but it starts from the goal, which doesn't work with readable proofs (which start from the arguments). The alternative is cong and replace, but they require you to pass the whole body as argument, which ends up very verbose. It helps to keep function bodies very small.
-
The interesting part is the informal reasoning, and these proofs show that informal reasoning usually correct. In fact, I spend more time on tedious details when proving these facts, than on actual problems with the proofs themselves.
module Main
import Data.List
import Data.List.Reverse
import Data.List.Equalities
import Data.List.Elem
import Data.So
import Data.Nat
import Data.Bool
import Data.Int.Order
import Proofs.Readable
import Decidable.Equality.Core
import Control.Function
total
leftPad : Nat -> a -> List a -> List a
leftPad n x l =
case length l `isGT` n of
Yes _ => l
No _ => replicate (n `minus` length l ) x ++ l
||| proof that replicate replicates the argument.
total
replicate_replicates : {x:a} ->
{y:a} ->
{n:Nat} ->
y `Elem` replicate n x ->
x = y
replicate_replicates {n} el with (replicate n x) proof p
replicate_replicates {n = (S k)} Here | ((z :: xs)) =
fst $ biinjective p
replicate_replicates {n = 0} (There w) | ((z :: xs)) =
absurd p -- the emptly list has no elements
replicate_replicates {n = (S k)} (There w) | ((z :: xs)) =
replicate_replicates {n=k} (rewrite (snd $ biinjective p) in w)
||| proof that leftpad always consists of the replicated character
||| followed by the given strings. Here proven with an existential.
||| This proof is fairly trivial.
total
leftPad_prepends : {n:Nat} ->
{l:List a} ->
{x:a} ->
(m:Nat ** (leftPad n x l = (replicate m x ++ l)))
leftPad_prepends {n} {l} with (S n `isLTE` length l) proof p
_ | (Yes prf) = (Z ** Refl)
_ | (No contra) = ((n `minus` length l) ** Refl)
total
maximumLte : (n:Nat) -> (m:Nat) -> LTE n m -> m = maximum n m
maximumLte 0 m LTEZero =
m
=~
maximum 0 m
=~
qed
maximumLte (S left) (S right) (LTESucc x) =
S right
=~ cong S (maximumLte left right x) >~
S (maximum left right)
=~
maximum (S left) (S right)
=~
qed
||| proof of the length of leftPad
total
leftPadLen : (n:Nat) -> (x:a) -> (l:List a) -> length (leftPad n x l) = maximum (length l) n
leftPadLen n x l with (isGT (length l) n)
leftPadLen n x l | (Yes prf) =
length l
=~ maximumLte n (length l) (lteSuccLeft prf) >~
maximum n (length l)
=~ maximumCommutative n (length l) >~
maximum (length l) n
=~
qed
leftPadLen n x l | (No contra) =
let p2 : LTE (length l) n
p2 = fromLteSucc $ notLTEImpliesGT contra in
length (replicate (minus n (length l)) x ++ l)
=~ lengthDistributesOverAppend _ _ >~
Prelude.List.length (replicate (minus n (length l)) x) + length l
=~ cong (\n => n + length l) (lengthReplicate _ ) >~
minus n (length l) + Prelude.List.length l
=~ plusMinusLte _ _ p2 >~
n
=~ maximumLte _ _ p2 >~
maximum (length l) n
=~
qed
||| find the minimum element with the index in the string
total
minIndexAux : (l:List Int) ->
NonEmpty l =>
(Nat, Int)
minIndexAux (x :: []) = (0, x)
minIndexAux (x :: (y :: xs)) =
let (ix, min) = minIndexAux (y :: xs)
in if x < min then (0, x) else (S ix, min)
minIndexAuxHasIndex : {l:List Int} ->
NonEmpty l =>
( prf: InBounds (fst (minIndexAux l)) l **
index (fst (minIndexAux l)) l = snd (minIndexAux l))
minIndexAuxHasIndex {l = (x :: [])} = (InFirst ** Refl)
minIndexAuxHasIndex {l = (x :: (x2::xs2))} with (minIndexAux (x2::xs2)) proof p
_ | (ix, min) with (x < min)
_ | False = let (recBnd ** recPrf) = minIndexAuxHasIndex {l=x2::xs2}
in rewrite (sym $ cong fst p)
in rewrite (sym $ cong snd p)
in (InLater recBnd ** recPrf)
_ | True = (InFirst ** Refl)
minIndexIsMinimum : {l:List Int} ->
NonEmpty l =>
snd (minIndexAux l) = foldr1 Prelude.min l
minIndexIsMinimum {l = (x :: [])} = Refl
minIndexIsMinimum {l = (x :: (y :: xs))}
with (minIndexAux (y :: xs)) proof p | (minIndexIsMinimum {l=y::xs}) proof p2
_ | (ix, min_) | rec with (x < min_) proof p3
_ | False = rewrite sym $ trans (cong snd $ sym p) rec in
rewrite p3 in Refl
_ | True = rewrite sym $ trans (cong snd $ sym p) rec in
rewrite p3 in Refl
total
minIndex : (l:List Int) ->
NonEmpty l =>
Nat
minIndex l = fst $ minIndexAux l
||| list scanl with proof of NonEmptyness.
total
scanlNe : (f:a -> b -> a) -> a -> List b -> (l:List a ** NonEmpty l)
scanlNe f x [] = ([x] ** IsNonEmpty)
scanlNe f x (y :: xs) = (x :: (fst $ scanlNe f (f x y) xs) ** IsNonEmpty)
||| list scanr with proof of NonEmptyness.
total
scanrNe : (b -> a -> a) -> a -> List b -> (l:List a ** NonEmpty l)
scanrNe f x [] = ([x] ** IsNonEmpty)
scanrNe f x (y :: xs) = case scanrNe f x xs
of (z::zs ** _) => ((f y z :: z :: zs) ** IsNonEmpty)
total
scanr : (b -> a -> a) -> a -> List b -> List a
scanr f x l = fst $ scanrNe f x l
total
scanl : (a -> b -> a) -> a -> List b -> List a
scanl f x l = fst $ scanlNe f x l
total
scanrFoldrProof : (f:(b -> a -> a)) ->
(x:a) ->
(l:List b) ->
scanr f x l = map (foldr f x) (tails l)
scanrFoldrProof f x [] = [x] =~ [x] =~ qed
scanrFoldrProof f x (y :: xs)
with (scanrFoldrProof f x xs) | (scanrNe f x xs) proof p
_ | rec | (x2 :: xs2 ** _) =
let recHead : x2 === foldr f x xs
recHead = fst (biinjective rec) in
f y x2 :: x2 :: xs2
=~ cong (\r => f y r :: x2 :: xs2) recHead >~
f y (foldr f x xs) :: x2 :: xs2
=~ cong (f y (foldr f x xs) ::) rec >~
f y (foldr f x xs) :: map (\x3 => foldr f x x3) (tails xs)
=~
foldr f x (y::xs) :: map (\x3 => foldr f x x3) (tails xs)
=~
map (\x3 => foldr f x x3) ((y::xs) :: tails xs)
=~
map (\x3 => foldr f x x3) (tails (y::xs))
=~
qed
total
zipWithMap : {l:List a} ->
zipWith f (map g l) (map h l) =
map (\x => f (g x) (h x)) l
zipWithMap {l = []} = Refl
zipWithMap {l = (x :: xs)} = cong (f (g x) (h x) ::) $ zipWithMap {l=xs}
total
scanlFoldlProof : (f:(a -> b -> a)) ->
(x:a) ->
(l:List b) ->
scanl f x l = map (foldl f x) (inits l)
scanlFoldlProof f x [] = [x] =~ [x] =~ qed
scanlFoldlProof f x (y :: xs)
with (scanlFoldlProof f (f x y) xs)
_ | rec = scanl f x (y :: xs)
=~
x :: scanl f (f x y) xs
=~ cong (x::) rec >~
x :: map (foldl f (f x y)) (inits xs)
=~
x :: map (\xs2 => foldl f x (y :: xs2)) (inits xs)
=~
x :: map (foldl f x . (y ::)) (inits xs)
=~ cong (x::) (sym $ mapFusion (foldl f x) (y ::) (inits xs)) >~
x :: map (foldl f x) (map (y ::) (inits xs))
=~
map (foldl f x) ([] :: map (y ::) (inits xs))
=~
map (foldl f x) (inits (y :: xs))
=~
qed
||| Proof that zipwith preserves NonEmptyness.
total
zipwithNonEmpty : (l:List a) ->
(m:List b) ->
NonEmpty l =>
NonEmpty m =>
NonEmpty (zipWith f l m)
zipwithNonEmpty [] _ impossible
zipwithNonEmpty _ [] impossible
zipwithNonEmpty (x :: xs) (y :: ys) = IsNonEmpty
total
foldlSnoc : (x : a) ->
(y : b) ->
(xs : List b) ->
(f : (a -> b -> a)) ->
foldl f x (snoc xs y) = f (foldl f x xs) y
foldlSnoc x y [] f = Refl
foldlSnoc x y (z :: xs) f = foldlSnoc (f x z) y xs f
total
foldlReverse : (f:(a -> b -> a)) ->
(x:a) ->
(l:List b) ->
foldl f x (reverse l) = foldr (flip f) x l
foldlReverse f x [] = x =~ x =~ qed
foldlReverse f x (y :: xs) =
foldl f x (reverse (y::xs))
=~
foldl f x (reverseOnto [y] xs)
=~ cong (foldl f x) (reverseOntoSpec [y] xs) >~
foldl f x (reverse xs ++ [y])
=~ foldlSnoc x y (reverse xs) f >~
f (foldl f x (reverse xs)) y
=~ cong (\r => f r y) (foldlReverse f x xs) >~
f (foldr (flip f) x xs) y
=~
foldr (flip f) x (y :: xs)
=~
qed
total
foldrReverse : (f:(a -> b -> a)) ->
(x:a) ->
(l:List b) ->
foldl f x l = foldr (flip f) x (reverse l)
foldrReverse f x l =
foldl f x l
=~ cong (foldl f x) (sym $ reverseInvolutive l) >~
foldl f x (reverse (reverse l))
=~ foldlReverse f x (reverse l) >~
foldr (flip f) x (reverse l)
=~
qed
||| ranges of Nats. The first argument is the length, and the second
||| the starting value. By having the first argument descending in the
||| recursive case, this is easier to prove total, and to prove
||| theorems about.
total
rangeAux : Nat -> Nat -> List Nat
rangeAux Z x = []
rangeAux (S k) x = x :: rangeAux k (S x)
total
rangeAuxLength : (n:Nat) -> length (rangeAux n x) = n
rangeAuxLength 0 = Refl
rangeAuxLength (S k) = cong S $ rangeAuxLength k
total
rangeAuxMapSucc : {n:Nat} -> {x:Nat} -> rangeAux n (S x) = map S (rangeAux n x)
rangeAuxMapSucc {n = 0} = [] =~ [] =~ qed
rangeAuxMapSucc {n = (S k)} =
rangeAux (S k) (1 + x)
=~
S x :: rangeAux k (2 + x)
=~ cong (S x ::) (rangeAuxMapSucc {n=k}) >~
S x :: map S (rangeAux k (1 + x))
=~
map S (rangeAux (S k) x)
=~
qed
||| range of Nats. The implementation and proofs follow trivially
||| from `rangeAux`
total
range : Nat -> Nat -> List Nat
range x y = rangeAux (minus (S y) x) x
total
rangeLength : {n:Nat} ->
{m:Nat} ->
length (range n m) = minus (S m) n
rangeLength = rangeAuxLength (minus (S m) n)
total
rangeMapSucc : {x:Nat} ->
{y:Nat} ->
range (S x) (S y) = map S (range x y)
rangeMapSucc = rangeAuxMapSucc {n=minus (S y) x} {x=x}
total
tailsMapRange : {l:List a} ->
map (\n => drop n l) (range 0 (length l)) = tails l
tailsMapRange {l = []} = [[]] =~ [[]] =~ qed
tailsMapRange {l = (x :: xs)} =
map (\n => drop n (x::xs)) (range 0 (length (x::xs)))
=~
(x::xs) :: map (\n => drop n (x::xs)) (range 1 (length (x::xs)))
=~ cong (\r => (x::xs) :: map (\n => drop n (x::xs)) r)
(rangeMapSucc {x=0} {y=length xs}) >~
(x::xs) :: map (\n => drop n (x::xs)) (map S (range 0 (length xs)))
=~ cong ((x::xs) ::)
(mapFusion (\n => drop n (x::xs)) S (range 0 (length xs))) >~
(x::xs) :: map (\n => drop (S n) (x::xs)) (range 0 (length xs))
=~
(x::xs) :: map (\n => drop n xs) (range 0 (length xs))
=~ cong ((x::xs)::) (tailsMapRange {l=xs}) >~
(x::xs) :: tails xs
=~
tails (x::xs)
=~
qed
total
initsMapRange : {l:List a} ->
map (\n => take n l) (range 0 (length l)) = inits l
initsMapRange {l = []} = [[]] =~ [[]] =~ qed
initsMapRange {l = (x :: xs)} =
map (\n => take n (x::xs)) (range 0 (length (x::xs)))
=~
map (\n => take n (x::xs)) (0 :: range 1 (length (x::xs)))
=~
[] :: map (\n => take n (x::xs)) (range 1 (length (x::xs)))
=~ cong (\r => [] :: map (\n => take n (x::xs)) r)
(rangeMapSucc {x=0} {y=length xs}) >~
[] :: map (\n => take n (x::xs)) (map S (range 0 (length xs)))
=~ cong ([] ::)
(mapFusion (\n => take n (x::xs)) S (range 0 (length xs))) >~
[] :: map (\n => take (S n) (x::xs)) (range 0 (length xs))
=~
[] :: map (\n => x :: take n xs) (range 0 (length xs))
=~ cong ([] ::)
(sym (mapFusion (x::) (\n => take n xs) (range 0 (length xs)))) >~
[] :: map (x::) (map (\n => take n xs) (range 0 (length xs)))
=~ cong (\r => [] :: map (x::) r) (initsMapRange {l=xs}) >~
[] :: map (x::) (inits xs)
=~
inits (x::xs)
=~
qed
||| efficient implementation of fulcrum.
total
fulcrum : List Int -> Nat
fulcrum l =
let (lft ** lne) = scanlNe (+) 0 l
(rt ** rne) = scanrNe (+) 0 l
zipwith_ne_prf = zipwithNonEmpty _ _ @{lne} @{rne} {f=(-)}
in minIndex (zipWith (-) lft rt) @{zipwith_ne_prf}
||| implementation that matches the spec, but with quadratic
||| complexity.
total
fulcrumSpec : List Int -> Nat
fulcrumSpec l =
minIndex
(map (\i => foldl (+) 0 (take i l) - foldr (+) 0 (drop i l)) $
range 0 (length l))
||| Proof that any two NonEmpty proofs for the same list are the same
||| proof. These seems trivial, but has to be proven explicitly to
||| idris.
total
NonEmptyEq : (neL:NonEmpty (x::xs)) ->
(neM: NonEmpty (y::ys)) ->
((x::xs) = (y::ys)) ->
(neL = neM)
NonEmptyEq IsNonEmpty IsNonEmpty prf =
rewrite fst (biinjective prf) in
rewrite snd (biinjective prf) in
Refl
||| congruence over functions which take NonEmpty values is tricky,
||| since we need to prove that the NonEmpty proofs are the same.
||| This function handles it.
total
congNE : (f : (x:List Int) -> NonEmpty x => y) ->
{l:List Int} ->
{m:List Int} ->
(l = m) ->
(neA: NonEmpty l) =>
(neB: NonEmpty m) =>
(f l = f m)
congNE f Refl {l=l1::ls} {m=l1::ls} =
let neEq : (neA = neB)
neEq = NonEmptyEq neA neB Refl
in rewrite neEq in Refl
total
scanlRange : {l:List a} ->
{f: b -> a -> b} ->
{x : b} ->
scanl f x l =
map (\i => foldl f x (take i l)) (range 0 (length l))
scanlRange =
scanl f x l
=~ (scanlFoldlProof _ _ {l=l}) >~
map (foldl f x) (inits l)
=~ cong (map (foldl f x)) (sym $ initsMapRange {l=l}) >~
map (foldl f x) (map (\n => take n l) (range 0 (length l)))
=~ mapFusion (foldl f x) (\n => take n l) (range 0 (length l)) >~
map (\i => foldl f x (take i l)) (range 0 (length l))
=~
qed
total
scanrRange : {l:List a} ->
{f: a -> b -> b} ->
{x : b} ->
scanr f x l =
map (\i => foldr f x (drop i l)) (range 0 (length l))
scanrRange =
scanr f x l
=~ (scanrFoldrProof _ _ {l=l}) >~
map (foldr f x) (tails l)
=~ cong (map (foldr f x)) (sym $ tailsMapRange {l=l}) >~
map (foldr f x) (map (\n => drop n l) (range 0 (length l)))
=~ mapFusion (foldr f x) (\n => drop n l) (range 0 (length l)) >~
map (\i => foldr f x (drop i l)) (range 0 (length l))
=~
qed
total
fulcrumBody : (l : List Int) ->
{sl : List Int} ->
{sr : List Int} ->
{neSl : NonEmpty sl} ->
{neSr : NonEmpty sr} ->
(scanlNe (+) 0 l = (sl ** neSl)) ->
(scanrNe (+) 0 l = (sr ** neSr)) ->
zipWith (-) sl sr =
map (\i => foldl (+) 0 (take i l) -
foldr (+) 0 (drop i l))
(range 0 (length l))
fulcrumBody l nePrfL nePrfR =
zipWith (-) sl sr
=~ cong (\r => zipWith (-) r sr) (cong fst $ sym nePrfL)
>~ zipWith (-)
(scanl (+) 0 l)
sr
=~ cong (\r => zipWith (-) (scanl (+) 0 l) r) (cong fst $ sym nePrfR)
>~ zipWith (-)
(scanl (+) 0 l)
(scanr (+) 0 l)
=~ cong (\r => zipWith (-) r (scanr (+) 0 l)) scanlRange
>~ zipWith (-)
(map (\i => foldl (+) 0 (take i l)) (range 0 (length l)))
(scanr (+) 0 l)
=~ cong (\r => zipWith (-) (map (\i => foldl (+) 0 (take i l)) (range 0 (length l))) r) scanrRange
>~ zipWith (-)
(map (\i => foldl (+) 0 (take i l)) (range 0 (length l)))
(map (\i => foldr (+) 0 (drop i l)) (range 0 (length l)))
=~ zipWithMap {l=(range 0 (length l))} >~
map
(\i => foldl (+) 0 (take i l) - foldr (+) 0 (drop i l))
(range 0 (length l))
=~
qed
total
fulcrumMatchesSpec : (l:List Int) -> fulcrum l = fulcrumSpec l
fulcrumMatchesSpec l with (scanlNe (+) 0 l) proof p1
_ | (sl ** neSl) with (scanrNe (+) 0 l) proof p2
_ | (sr ** neSr) = congNE minIndex
(fulcrumBody l p1 p2 {neSl} {neSr})
{neA=neA}
{neB=neB}
where neA : NonEmpty (zipWith (-) sl sr)
neA = zipwithNonEmpty sl sr
neB : NonEmpty ((map (\i => foldl (+) 0 (take i l) -
foldr (+) 0 (drop i l)) $
range 0 (length l)))
neB = IsNonEmpty
--
-- Local Variables:
-- idris-load-packages: ("readable-proofs" "contrib")
-- End: