When using the `with`

construct to pattern match on intermediate results the terms matched on are abstracted from the goal type and possibly also from the types of previous arguments. This makes it possible to prove properties of functions defined by with, simply by following the same recursion pattern.

An example

filter : {A : Set} -> (A -> Bool) -> List A -> List A filter p [] = [] filter p (x :: xs) with p x ... | true = x :: filter p xs ... | false = filter p xs module Proof {A : Set}(P : List A -> Set) where proof : (p : A -> Bool)(xs : List A) -> P (filter p xs) proof p [] = ?_{0}proof p (x :: xs) with p x ... | true = ?_{1}... | false = ?_{2}

Before the `with`

in `proof`

the goal was `P (filter p (x :: xs))`

which reduces to `P (filter p (x :: xs) | p x)`

. When performing the `with`

, `p x`

is abstracted from the goal type so in the two branches we have `?1 : P (filter p (x :: xs) | true)`

which reduces to `P (x :: filter p xs)`

and `?2 : P (filter p (x :: xs) | false)`

which reduces to `P (filter p xs)`

.

For the full example see test/succeed/Filter.agda.

Page last modified on October 16, 2007, at 09:43 AM

Powered by
PmWiki