A formally verified implementation of Day One of the 2020 Advent of Code

DayOne.agda

module DayOne where

-- Lets build this up from scratch, for didactic purposes.
-- If we were doing this "for real" we ought to use agda-stdlib.

--------------------------------------------------------------------------------
-- Basic Definitions
--------------------------------------------------------------------------------

-- First, natural numbers and lists. Nothing too exciting here.

data ℕ : Set where
  zero : ℕ 
  succ : ℕ → ℕ

-- Lets us use numeric literals
{-# BUILTIN NATURAL ℕ #-}

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (succ n)

-- Sum types.
data _⊎_ (A B : Set) : Set where
  injₗ : A → A ⊎ B
  injᵣ : B → A ⊎ B

-- Product Types.
data _×_ (A B : Set) : Set where
 _,_ : A → B → A × B

-- The empty type. We use this to say that things are "impossible" or not true.
data ⊥ : Set where

-- Next, the identity type. We say that two things are equal when they
-- compute to exactly the same thing.
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {a} → a ≡ a

--------------------------------------------------------------------------------
-- Boring functions and lemmas
--------------------------------------------------------------------------------

_+_ : ℕ → ℕ → ℕ
zero + y = y
succ x + y = succ (x + y)

map : ∀ {A B} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ (map f xs)

_++_ : ∀ {A} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

map₂ : ∀ {A B C} → (A → B → C) → List A → List B → List C
map₂ f [] ys = []
map₂ f (x ∷ xs) ys = (map (f x) ys) ++ (map₂ f xs ys)

replicate : ∀ {A} → A → (n : ℕ) → Vec A n
replicate a zero = []
replicate a (succ n) = a ∷ replicate a n

-- This one is a little bit tricky. We can think of this as a generalization
-- of the following function:
-- ∀ {A} → List A × List A → List (A × A)
-- But generalized to Vectors rather than pairs.
--
-- We can also think of this as Haskells 'sequence'.
vectors : ∀ {A} {n} → Vec (List A) n → List (Vec A n)
vectors [] = [] ∷ []
vectors (x ∷ xs) = map₂ _∷_ x (vectors xs)

-- Gets a list of all possible ways of choosing 'k' elements from a list (with repitition)
_choose_ : ∀ {A} → List A → (k : ℕ) → List (Vec A k)
xs choose k = vectors (replicate xs k)

sum : ∀ {n} → Vec ℕ n → ℕ
sum [] = 0
sum (x ∷ xs) = x + sum xs

-- If the successors of two numbers are equal, then they themselves must be equal.
succ-injective : ∀ {x y} → succ x ≡ succ y → x ≡ y
succ-injective refl = refl

-- All functions respect equality.
cong : ∀ {X Y} {x y} (f : X → Y) → x ≡ y → f x ≡ f y
cong f refl = refl

--------------------------------------------------------------------------------
-- Decidable properties
--------------------------------------------------------------------------------

-- Now, for the first "new" thing: Decidable properties.
-- A property is considered decidable if we can compute a proof of it,
-- or compute a proof showing that it is impossible.
data Dec (P : Set) : Set where
  yes : P → Dec P 
  no  : (P → ⊥) → Dec P

dec-map : ∀ {P Q} → (P → Q) → (Q → P) → Dec P → Dec Q
dec-map f g (yes p) = yes (f p)
dec-map f g (no contra) = no λ q → contra (g q)

-- Shorthand for being able to decide a property of 'A' for every element.
Decidable : ∀ {A : Set} (P : A → Set) → Set
Decidable P = ∀ x → Dec (P x)

-- Equality of natural numbers is decidable!
nat-eq? : ∀ (x y : ℕ) → Dec (x ≡ y) 
nat-eq? zero zero = yes refl
nat-eq? zero (succ y) = no λ ()
nat-eq? (succ x) zero = no λ ()
nat-eq? (succ x) (succ y) with nat-eq? x y
... | yes eq = yes (cong succ eq )
... | no contra = no λ eq → contra (succ-injective eq)

-- If we have two decidable properties, then we can figure out if either of them are true.
_⊎?_ : ∀ {P Q} → Dec P → Dec Q → Dec (P ⊎ Q)
(yes p) ⊎? _ = yes (injₗ p)
_ ⊎? (yes q) = yes (injᵣ q)
(no contra-p) ⊎? (no contra-q) = no λ { (injₗ p) → contra-p p ; (injᵣ q) → contra-q q }

-- A proof that some property 'P' holds for some element of a list.
data Any {A : Set} (P : A → Set) : (List A) → Set where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

-- If we know that some property holds for some element of a list, then it
-- must either hold for the first element, or must hold for some element
-- in the tail.
locate : ∀ {A} {P : A → Set} {x} {xs} → Any P (x ∷ xs) → P x ⊎ (Any P xs)
locate (here px) = injₗ px
locate (there p) = injᵣ p

-- If we know that a property holds for either the first element or the tail of the list,
-- then it must hold for some element of the entire list.
somewhere : ∀ {A} {P : A → Set} {x} {xs} → P x ⊎ (Any P xs) → Any P (x ∷ xs)
somewhere (injₗ px) = here px
somewhere (injᵣ p) = there p

-- If our property 'P' is decidable, then we can decide if it holds anywhere in the list.
any? : ∀ {A : Set} {P : A → Set} → Decidable P  → Decidable (Any P)
any? P? [] = no λ ()
any? P? (x ∷ xs) = dec-map somewhere locate ((P? x) ⊎? any? P? xs)

--------------------------------------------------------------------------------
-- The Problem
--------------------------------------------------------------------------------

-- Do a collection of 'n' natural numbers sum to a goal?
_SumsTo_ : (n goal : ℕ) → Vec ℕ n → Set
_SumsTo_ _ goal xs = sum xs ≡ goal

-- The above property is decidable!
sums-to? : ∀ (n goal : ℕ) → Decidable (n SumsTo goal)
sums-to? n goal xs = nat-eq? (sum xs) goal

-- Now, for the punchline! We can decide if any 'k' elements chosen from 'xs' sum up to our goal.
choice-sum? : ∀ (k goal : ℕ) → (xs : List ℕ) → Dec (Any (k SumsTo goal) (xs choose k))
choice-sum? k goal xs = any? (sums-to? k goal) (xs choose k)