Case Expression

The source code for this module: PartI/Case.ard
The source code for the exercises: PartI/CaseEx.ard

In this module we discuss three themes.

Firstly, we discuss case expressions and alternatives to them in the form of the helper functions. We also compare \case to \elim, point out at peculiarities of using case expressions in a dependently typed language and explain pattern matching on idp in \case.

Secondly, we explain a technique of views, allowing to define custom pattern matching principles.

Finally, we discuss an important class of predicates: decidable predicates, which are precisely the predicates P : A -> \Type such that for every x : A either P x or the negation of P x is provable.

filter via \case and via helper

Case expressions, like in Haskell, can be used for pattern matching on arbitrary expressions. For example, let us define the function filter that removes from a list xs : List A all elements that do not satisfy some predicate p : A -> Bool:

\func filter {A : \Type} (p : A -> Bool) (xs : List A) : List A \elim xs
  | nil => nil
  | cons x xs => \case p x \with {
    | true => cons x (filter p xs)
    | false => filter p xs
  }

Here we used case expression for pattern matching on the expression p x. Alternatively, we could introduce a helper function, defined by pattern matching, and invoke it in the place of \case usage:

\func filter' {A : \Type} (p : A -> Bool) (xs : List A) : List A \elim xs
  | nil => nil
  | cons x xs => helper (p x) x (filter p xs)
  \where
    \func helper {A : \Type} (b : Bool) (x : A) (r : List A) : List A \elim b
      | true => cons x r
      | false => r

Actually, every usage of case expression can be replaced in this way with an invocation of a helper function. It is just sometimes more convenient to use short case expressions instead of introducing countless amount of helpers.

Exercise 1: Implement any sorting algorithm using \case for pattern matching on the result of comparison of elements of a list.

Remark on \elim vs \case

A definition of a function by pattern matching can be given either with \elim or with \case. These two ways are almost equivalent, but there is one small difference: depending on whether f is defined via \case or via \elim, the expression f x evaluates to the \case expression or does not evaluate respectively. Consider, for example, the following two definitions:

\func f (x : Nat) : Nat => \case x \with { zero => 0 | suc n => n }
\func f' (x : Nat) : Nat | zero => 0 | suc n => n

f n evaluates to the body of the definition, whereas the expression f’ n is in normal form. The latter option makes normalized terms look nicer and for that reason is usually preferable.

\case in dependently typed languages

Case expressions are more subtle in dependently typed languages than in languages like Haskell. Let us assume, for example, we want to prove that p a = not (not (p a)) for some predicate p : A -> Bool and a : A. Of course, this statement can be proved as a consequence of a generalized statement x = not (not (x)), and that is the right way to do it, but we would like to show how it can be proven with \case:

\func not (b : Bool) : Bool
  | true => false
  | false => true

\func foo {A : \Type} (p : A -> Bool) (a : A) : p a = not (not (p a)) =>
   \case p a \as b \return b = not (not b) \with {
    | true => idp 
    | false => idp
  }

Here we specified explicitly the return type of the case expression by writing \return b = not (not b) before the keyword \with. We do this because this return type of \case depends on the expression p a that we match on. In order to describe the dependence, we introduce new bound variable b by writing \as b just after the expression p a.

In every clause we should return an expression, whose type is the expression obtained from the one written after \return by substituting the corresponding pattern. In example above we have:

| true => idp -- here we should return expression of type true = not (not true)
| false => idp -- and here of type false = not (not false)

As we said, we could use a helper function:

\func foo' {A : \Type} (p : A -> Bool) (a : A) : p a = not (not (p a)) =>
  helper (p a)
  \where
    \func helper (b : Bool) : b = not (not b) \elim b
      | true => idp
      | false => idp

\case with several arguments

We can pattern match on several expressions in \case. For example:

\data Ordering | LT | EQ | GT

\func compare (x y : Nat) : Ordering =>
  \case x < y, y < x \with {
    | true, true => EQ -- this will never be matched
    | true, false => LT
    | false, true => GT
    | false, false => EQ
  }

Proof of a fact about filter via \case

Let us consider one more example of a proof via \case: let us prove that the length of a filtered list filter xs is at most the length of the original list xs:

\data Empty

\func absurd {A : \Type} (e : Empty) : A

\data Unit | unit

\func \infix 4 <= (x y : Nat) : \Type
  | 0, _ => Unit
  | suc _, 0 => Empty
  | suc x, suc y => x <= y

\func length {A : \Type} (xs : List A) : Nat
  | nil => 0
  | cons _ xs => suc (length xs)

-- auxiliary helper lemma
\func <=-helper {x y : Nat} (p : x <= y) : x <= suc y \elim x, y
  | 0, _ => unit
  | suc x, 0 => absurd p
  | suc x, suc y => <=-helper p

\func filter-lem {A : \Type} (p : A -> Bool) (xs : List A) : length (filter p xs) <= length xs \elim xs
  | nil => unit
  | cons x xs => \case p x \as b \return length (\case b \with { | true => cons x (filter p xs) | false => filter p xs }) <= suc (length xs) \with {
    | true => filter-lem p xs
    | false => <=-helper (filter-lem p xs)
  }

Exercise 2: Define filter via if not using \case. Prove the lemma filter-lem for this version of filter.

\elim in \case

Suppose we want to prove that && is associative using \case:

\func \infixr 3 && (x y : Bool) : Bool \elim x
  | true => y
  | false => false

\func &&-assoc (x y z : Bool) : (x && y) && z = x && (y && z) => \case x \with {
  | true => {?}
  | false => {?}
}

This will not work since x will not be replaced with the corresponding pattern in each of the cases above. To make this work, we need to bind x again and explicitly specify the result type of the \case-expression:

\func &&-assoc (x y z : Bool) : (x && y) && z = x && (y && z) => \case x \as x' \return (x' && y) && z = x' && (y && z) \with {
  | true => idp
  | false => idp
}

This is a common pattern. In such cases, we can use keyword \elim to simplify the \case expression. It can be written before a variable in a \case expression. Then this variable will be replaced with corresponding patterns in each of the cases in the result type. Thus, we can rewrite the example above as follows:

\func &&-assoc (x y z : Bool) : (x && y) && z = x && (y && z) => \case \elim x \with {
  | true => idp
  | false => idp
}

Matching on idp in \case

When we match on some expression e, the connection between this expression and the result of the pattern matching gets lost. For example, we cannot even prove that expr equals pattern inside an expression of the form \case expr \with { | pattern => {?} }. Sometimes we need to remember such a connection. In these cases we can use the following trick: double pattern matching on the original expression e and on idp with explicitly written type depending on e. Consider an example:

\func baz {A : \Type} (B : Bool -> \Type) (p : A -> Bool) (a : A) (pt : B true) (pf : B false) : B (p a) =>
    -- Not only the return type can be specified explicitly, but also 
    -- the type of expressions we do matching on.
    -- And we can use variables bounded in \as.
    \case p a \as b, idp : b = p a \with {
      | true, q => transport B q pt -- here q : true = p a
      | false, q => transport B q pf -- here q : false = p a
    }

And a helper version again:

\func baz' {A : \Type} (B : Bool -> \Type) (p : A -> Bool) (a : A) (pt : B true) (pf : B false) : B (p a) => 
    helper B p a pt pf
           (p a) idp
  \where
    \func helper {A : \Type} (B : Bool -> \Type) (p : A -> Bool) (a : A) (pt : B true) (pf : B false)
                (b : Bool) (q : b = p a) : B (p a) \elim b
      | true => transport B q pt -- here q : true = p a
      | false => transport B q pf -- here q : false = p a

Exercise 3: Prove that, for every function f : Bool -> Bool and every x : Bool, it is true that f (f (f x)) = f x

One more example of \case

Let us consider one more example, demonstrating what we have just discussed:

\func bar {A : \Type} (p q : A -> Bool) (a : A) (s : q a = not (p a))
  : not (q a) = p a =>
  \case p a \as x, q a \as y, s : y = not x \return not y = x \with {
    | true, true, s' => inv s'
    | true, false, _ => idp
    | false, true, _ => idp
    | false, false, s' => inv s'
  }

-- helper version
\func bar' {A : \Type} (p q : A -> Bool) (a : A) (s : q a = not (p a))
  : not (q a) = p a => helper (p a) (q a) s
  \where
    \func helper (x y : Bool) (s : y = not x) : not y = x \elim x, y
      | true, true => inv s
      | true, false => idp
      | false, true => idp
      | false, false => inv s

Views

Views – is a technique that allows to define some kind of custom pattern matching for data types. For example, Nat has constructors zero and suc and by default we pattern match on them whenever we define a function from Nat. But we can also define a custom pattern matching for Nat as if Nat had constructors, say, even and odd.

Let us define a data type parameterized by the data type we are defining custom pattern matching for (Nat in our example). The constructors of this data type will correspond to the constructors that we want to use for our custom pattern matching (even and odd in our example). Each constructor should have a parameter of the form n = expr, where expr represents the custom pattern. In our example we have the following:

\data Parity (n : Nat)
  | even (k : Nat) (p : n = 2 * k)
  | odd (k : Nat) (p : n = 2 * k + 1)

Next, we define a function that converts elements of Nat to elements of Parity:

\func parity (n : Nat) : Parity n
  | 0 => even 0 idp
  | suc n => \case parity n \with {
    | even k p => odd k (pmap suc p)
    | odd k p => even (suc k) (pmap suc p)
  }

Now, in order to pattern match on n : Nat we should invoke \case on parity n. For example, let us define division by 2:

\func div2 (n : Nat) : Nat => \case parity n \with {
  | even k _ => k
  | odd k _ => k
  }

Exercise 4: Define the view, which represents a natural number as a pair of the quotient and the remainder of division by a positive m. Implement the division function.

Decidable predicates

Here we will discuss predicates in propositions-as-types logic, that is functions P : A -> \Type. A predicate is called decidable if there is a proof that for all x : A either P x or not P x. We can write the statement DecPred P saying that P is decidable as follows:

\data Decide (A : \Type)
  | yes A
  | no (A -> Empty)

\func DecPred {A : \Type} (P : A -> \Type) => \Pi (a : A) -> Decide (P a)

This notion of decidability is related to decidability in computability theory: if a predicate is decidable in this sense, then there exists an algorithm that for every x : A decides whether P x or not P x.

In particular, there exist undecidable predicates. For example, we can define the following predicate P : Nat -> \Type: P n encodes the statement “Turing machine with number n halts at the input n”. A simpler example – the predicate on pairs of functions Nat -> Nat, saying that they are equal.

An example of decidable predicate:

\func suc/=0 {n : Nat} (p : suc n = 0) : Empty => transport (\lam n => \case n \with { | 0 => Empty | suc _ => Unit }) p unit
 
-- the predicate \lam n => n = 0 is decidable
\func decide0 : DecPred (\lam (n : Nat) => n = 0) => \lam n =>
  \case n \as n' \return Decide (n' = 0) \with {
    | 0 => yes idp
    | suc _ => no suc/=0
  }

The above properties of decidability hold as long as our logic is intuitionistic. If we have the Law of Excluded Middle, then all predicates are decidable, and, in fact, the opposite implication is also true.

Exercise 5: Prove that the predicate ‘isEven’ is decidable.

Decidable equality

Let us consider the predicate DecEq A, saying that type A has decidable equality on it:

\func DecEq (A : \Type) => \Pi (a a' : A) -> Decide (a = a')

We can define a typeclass analogous to Eq in Haskell, but with a proof of decidability of equality instead of a function == : A -> A -> Bool. This is better since in Haskell == can be absolutely any function, not necessarily having anything to do with equality.

\class Eq (A : \Type) {
  | decideEq : DecEq A
  -- Functions declared inside a class have instance of
  -- the class as their first implicit parameter.
  \func \infix 4 == (a a' : A) : Bool => \case decideEq a a' \with {
    | yes _ => true
    | no _ => false
  }
} \where {
  -- Function == is equivalent to =='.
  \func \infix 4 ==' {e : Eq} (a a' : e.A) : Bool => \case e.decideEq a a' \with {
    | yes _ => true
    | no _ => false
  }
}

Let us define an instance for the type of natural numbers:

\func pred (n : Nat) : Nat
  | 0 => 0
  | suc n => n

\instance NatEq : Eq Nat
  | decideEq => decideEq
  \where
    \func decideEq (x y : Nat) : Decide (x = y)
      | 0, 0 => yes idp
      | 0, suc y => no (\lam p => suc/=0 (inv p))
      | suc x, 0 => no suc/=0
      | suc x, suc y => \case decideEq x y \with {
        | yes p => yes (pmap suc p)
        | no c => no (\lam p => c (pmap pred p))
      }

\func test1 : (0 == 0) = true => idp
\func test2 : (0 == 1) = false => idp

Exercise 6: Prove that if equality of elements of a type A is decidable, then equality of elements if List A is also decidable.

Exercise 7: Prove that if equality of elements of a type A is decidable, then every list of elements of A is either empty, consists of repetitions of one element or there exist two different elements in A.

Decidable predicates and functions A -> Bool

Decidable predicates A -> \Type correspond precisely to functions A -> Bool. Let us define the conversion functions:

\func FromBoolToDec {A : \Type} (p : A -> Bool) : \Sigma (P : A -> \Type) (DecPred P)
  => (\lam a => T (p a), \lam a => \case p a \as b \return Decide (T b) \with {
    | true => yes tt
    | false => no T-absurd
  })

\func FromDecToBool {A : \Type} (P : \Sigma (P : A -> \Type) (DecPred P)) : A -> Bool
  => \lam a => \case P.2 a \with {
    | yes _ => true
    | no _ => false
  }

Exercise 8: Prove that the functions ‘FromBoolToDec’ and ‘FromDecToBool’ are inverse to each other.

\func bdb {A : \Type} (p : A -> Bool) : FromDecToBool (FromBoolToDec p) = p => {?}

-- We cannot prove that 'FromBoolToDec (FromDecToBool P) = P', but we can prove a weaker statement:
-- these predicates are logically equivalent.

-- Equivalence of predicates
\func \infix 4 <-> {A : \Type} (P Q : A -> \Type) => \Pi (x : A) -> \Sigma (P x -> Q x) (Q x -> P x)

\func dbd {A : \Type} (P : \Sigma (P : A -> \Type) (DecPred P)) : (FromBoolToDec (FromDecToBool P)).1 <-> P.1 => {?}