MagicWith

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.