Jason Orendorff jorendorff

porglezomp / Leftpad.idr

Last active August 13, 2024 22:22

Taking on Hillel's challenge to formally verify leftpad (https://twitter.com/Hillelogram/status/987432181889994759)

	-- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris
	import Data.Vect

	-- `minus` is saturating subtraction, so this works like we want it to
	eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
	eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
	eq_max Z (S _) = Refl
	eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

	-- The type here says "the result is" padded to (maximum k n), and is padding plus the original