Search code examples
pattern-matchingagda

Failure in pattern matching in Agda 2.5.1.2

Given the following datatype which encodes a verified comparison between two natural numbers:

open import Agda.Builtin.Nat

data Compare : Nat -> Nat -> Set where
  LT : {m : Nat} {n : Nat} -> Compare m (suc (m + n))
  EQ : {m : Nat} -> Compare m m
  GT : {m : Nat} {n : Nat} -> Compare (suc (m + n)) m

the following code correctly compares numbers and computes their difference:

comparehelper : {m : Nat} {n : Nat} -> (Compare m n) -> Compare (suc m) (suc n)
comparehelper LT = LT
comparehelper EQ = EQ
comparehelper GT = GT

compare : (m : Nat) (n : Nat) -> Compare m n
compare 0 0 = EQ
compare (suc _) 0 = GT
compare 0 (suc _) = LT
compare (suc m) (suc n) = comparehelper (compare m n)

differencehelper : {m : Nat} {n : Nat} -> (Compare m n) -> Nat
differencehelper (LT {n = difflt1}) = suc difflt1
differencehelper EQ = 0
differencehelper (GT {n = difflt1}) = suc difflt1

difference : Nat -> Nat -> Nat
difference m n = differencehelper (compare m n)

but the following, apparently functionally identical, code does not (the pattern matching fails type checking):

compare' : (m : Nat) (n : Nat) -> Compare m n
compare' 0 0 = EQ
compare' (suc _) 0 = GT
compare' 0 (suc _) = LT
compare' (suc m) (suc n) with compare' m n
... | LT = LT
... | EQ = EQ
... | GT = GT

difference' : Nat -> Nat -> Nat
difference' m n with compare' m n
... | LT {n = difflt1} = suc difflt1
... | EQ = 0
... | GT {n = difflt1} = suc difflt1

What is the explanation for the difference in behavior? As stated in the question, I am running Agda 2.5.1.2.

Solution

  • The issue here is that pattern-matching on a value of type Compare m n refines the patterns for m and n.

    So the scheme compare' (suc m) (suc n) which ... stands for is not valid anymore. You have to repeat the left hand side with refined patterns e.g.

    compare' (suc m) (suc n) with compare' m n
compare' (suc m) (suc .(suc m + _)) | LT = LT
compare' (suc m) (suc .m)           | EQ = EQ
compare' (suc .(suc m + _)) (suc m) | GT = GT

    I have used underscores here for the variables which are in scope but not explicitly named (they are implicit arguments to LT and GT respectively). The fact that they are not named but required in the patterns can be a good clue that they should maybe be explicit arguments of the LT and GT constructors.

    Alternatively, if you don't care about the patterns, you can use underscores (which may stand for any pattern including dotted ones) and write:

    compare' (suc _) (suc _) | LT = LT
compare' (suc _) (suc _) | EQ = EQ
compare' (suc _) (suc _) | GT = GT

    As @asr mentioned newer versions of Agda will support your current pattern-match because dot patterns have been made optional.