# With-expression

TODO: syntax for nested with

### A simple example

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.

### More in depth (See also page 45 of Ulf Norell’s thesis)

When using a with the context is split in two parts

• the part needed to type the with arguments, and
• anything else

The with arguments are abstracted over the latter part and the goal type, but not the former.

In greek:

Consider

```  f : Γ → A
f xs with vs
```

assuming for simplicity that there’s no pattern matching in xs. First infer the types of vs

```  Γ ⊢ vs : As
```

Now find a well-formed context Γ₁, Γ₂ which is a permutation of Γ such that

```  Γ₁ ⊢ vs : As
```

Compute Δ by abstracting each type in As over earlier vs, so Γ₁ ⊢ vs : Δ and Δ{vs} = As (where (x : A)Θ {v,vs} = A, Θ[v/x]{vs}). Then compute B such that

```  Γ₁, Δ ⊢ B type  and
B[vs/Δ] = Γ₂ → A  (i.e. abstract Γ₂ → A over vs)
```

This gives the type of the with function:

```  withfun : Γ₁ → Δ → B
```

Note that the abstraction steps can fail to produce a well-typed term.

Some examples:

``` postulate
A     : Set
_+_   : A → A → A
T     : A → Set
mkT   : ∀ x → T x

-- x and y are needed to type the with argument, so the context
-- is split after y
f₁ : (x y : A)(t : T (x + y)) → T (x + y)
f₁ x y t with x + y
f₁ x y t | w = {!!}

-- Generated with function
with₁ : (x y : A) (w : A) (t : T w) → T w
with₁ x y w t = {!!}

-- x is not needed to type the with argument, so the context
-- is reordered with only y before the with argument
f₂ : (x y : A)(t : T (y + y)) → T (y + y)
f₂ x y t with y + y
f₂ x y t | w = {!!}

with₂ : (y : A) (w : A) (x : A) (t : T w) → T w
with₂ y w x t = {!!}

postulate
H : ∀ x y → T (x + y) → Set

-- Multiple with arguments are always inserted together, so in this case
-- t ends up on the left since it’s needed to type h and thus x + y isn’t
-- abstracted from the type of t
f₃ : (x y : A) (t : T (x + y)) (h : H x y t) → T (x + y)
f₃ x y t h with x + y | h
f₃ x y t h | w₁ | w₂ = {!!}  -- t : T (x + y), goal : T w₁

with₃ : (x y : A) (t : T (x + y)) (h : H x y t) (w₁ : A) (w₂ : H x y t) → T w₁
with₃ x y t h w₁ w₂ = {!!}

-- But earlier with arguments are abstracted from the types of later ones
f₄ : (x y : A) (t : T (x + y)) → T (x + y)
f₄ x y t with x + y | t
f₄ x y t | w₁ | w₂ = {!!}  -- t : T (x + y), w₂ : T w₁, goal : T w₁

with₄ : (x y : A) (t : T (x + y)) (w₁ : A) (w₂ : T w₁) → T w₁
with₄ x y t w₁ w₂ = {!!}
```