Day2a.org

Verified AOC in Idris: Day 2 Puzzle 1

Some Imports

import System.File
import Data.Strings
import Data.Either
import Data.List
import Data.List.Quantifiers
import Data.List.Elem
import Decidable.Equality
import Data.Void
import Data.Nat
import Data.Nat.Order
import Decidable.Decidable
import Decidable.Order
import Data.String.Parser

Datatypes describing the solution

Constraint on whether a password is valid or not

Contains the character, and the min/max number of times that character can occur.

record Constraint where
  constructor MkConstraint
  char : Char
  min , max : Nat

Define the number of occurrences of a character in a string of text

count : Char -> List Char -> Nat
count chr pwd = length (filter (== chr) pwd)

A proof that a given password matches a constraint

record MatchesConstr (c : Constraint) (pwd : List Char) where
  constructor MkMatches
  enough : LTE (min c) (length (filter (== (char c)) pwd))
  fewEnough : LTE (length (filter (== (char c)) pwd)) (max c)

It’s decidable whether a password matches a constraint

We build this from the fact that ordering on Nat is decidable.

decMatches : (c : Constraint) -> (pwd : List Char) -> Dec (MatchesConstr c pwd)
decMatches c pwd =
  case (Data.Nat.Order.lte (min c) (count (char c) pwd), Data.Nat.Order.lte (count (char c) pwd) (max c)) of
    (Yes pf1, Yes pf2) => Yes $ MkMatches pf1 pf2
    (No npf, _) => No (\ match => absurdity (npf $ enough match))
    (_, No npf) => No (\ match => absurdity (npf $ fewEnough match))

Define an existential wrapper

Basically, we want to wrap each constraint-password pair with a proof that the password either does or doesn’t satisfy the constraint.

record MatchDecision where
  constructor MkMatchDec
  constr : Constraint
  pwd : String
  decision : Dec (MatchesConstr c (fastUnpack pwd))

We can build a match decision from any constraint-string pair

packDecision : (Constraint , String) -> MatchDecision
packDecision (constr , pwd) = MkMatchDec constr pwd (decMatches constr _)

We also define a function that takes one of the records, and determines whether it was or wasn’t a match.

checkMatch : MatchDecision -> Bool
checkMatch matchDec with (decision matchDec)
  checkMatch matchDec | Yes _ = True
  checkMatch matchDec | No _ = False

The Whole Solution

Given a list of constraint-password pairs, a solution is valid if the count matches the number of matches in the list

Solution : List (Constraint , String) -> Nat -> Type
Solution pairs numMatch =
  numMatch = length (filter checkMatch $ map packDecision pairs)

Show that the solution is decidable and always exists

Nothing fancy here. The definition of solution tells us how to compute it, so we just compute it using that definition. Idris is smart enough to know that when we put Refl as the proof that the solution is equal to the length of filtering, that it should use that function to fill in the actual definition.

decideSoln : (input : List (Constraint , String)) -> (numMatch : Nat ** Solution input numMatch)
decideSoln input = (_ ** Refl)

Parsing the Input

We can use Idris’s parsing library to build a fairly simple, but elegant parser for AOC’s data format.

Parse a single line of input

lineToPair : Parser (Constraint, String)
lineToPair = do
   min <- natural
   string "-"
   max <- natural
   space
   chr <- alphaNum
   string ":"
   space
   pwd <- takeWhile (\ c => not (c == '\n'))
   pure $ (MkConstraint chr min max, pwd)

Parse multiple lines of input into a list

parseLines : Parser (List (Constraint, String))
parseLines = sepBy lineToPair (string "\n")

Read the input file and print the solution

Show Constraint where
  show c = show (min c , max c , char c)

This is a partial function, so we don’t need to do a bunch of monadic error handling.

%default partial
main : IO ()
main = do
  (Right contents) <- readFile "Day2.in"
  let (Right (input, _)) = parse parseLines contents
  let (count ** soln) = decideSoln input
  putStrLn $ show count