```
module Sets.With_Functions where

open import Data.Nat using (zero; suc; ℕ; _+_)
open import Data.Bool
open import Data.Empty using (⊥)
open import Data.List using (List; length; _∷_; [])
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; sym; cong)```

# Types with function application in indices

Consider the following two types that are equivalent:

```
data Even : ℕ → Set where
double : ∀ n → Even (n + n)

data Even′ (m : ℕ) : Set where
double : ∀ n → m ≡ n + n → Even′ m```

There exist conversion functions between those types:

```
toEven : ∀ {m} → Even′ m → Even m
toEven {.(n + n)} (double n refl) = double n

toEven′ : ∀ {m} → Even m → Even′ m
toEven′ {.(n + n)} (double n) = double n refl```

# Usage

Although `Even` and `Even′` are equivalent, `Even′` is much easier to use. In order to see this, let us try to prove that `Even n` is decidable for all `n`.

The concept of "decidable" is modelled by the `Dec` set (we will discuss that later, just take a quick look at its definition for now):

```
infix 3 ¬_

¬_ : ∀ {A} → Set A → Set A
¬ P = P → ⊥

data Dec (A : Set) : Set where
yes :   A → Dec A
no  : ¬ A → Dec A```

# Lemmata

Consider the following lemmata for the proofs:

```
suc-+ : ∀ n m → suc (n + m) ≡ n + suc m
suc-+ zero    m = refl
suc-+ (suc n) m = cong suc (suc-+ n m)

prev-≡ : ∀ {n m} → suc n ≡ suc m → n ≡ m
prev-≡ {.m} {m} refl = refl```

# Proof for `Even′`

With the help of the lemmata, the proof for `Even′` could be given as follows. Note the use of a new construct, the `with` keyword in the function definitions. This keyword is used to implement pattern matching on the value of the recursive invocation.

```
nextEven′ : ∀ {n} → Even′ n → Even′ (suc (suc n))
nextEven′ {.(n₁ + n₁)} (double n₁ refl)
= double (suc n₁) (cong suc (suc-+ n₁ n₁))

prevEven′ : ∀ {n} → Even′ (suc (suc n)) → Even′ n
prevEven′ {m} (double zero ())
prevEven′ {m} (double (suc n) x)
= double n (prev-≡ (trans (prev-≡ x) (sym (suc-+ n n))))

¬Even′1 : ¬ (Even′ 1)
¬Even′1 (double zero ())
¬Even′1 (double (suc zero) ())
¬Even′1 (double (suc (suc n)) ())

isEven′ : (n : ℕ) → Dec (Even′ n)
isEven′ zero       = yes (double zero refl)
isEven′ (suc zero) = no ¬Even′1
isEven′ (suc (suc n)) with (isEven′ n)
... | yes e = yes (nextEven′ e)
... | no ¬p = no (λ x → ¬p (prevEven′ x))```

Just for the sake of comparison, here is an example of using `with` in a regular function definition.

```
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```

# The `rewrite` construct

If `x : a ≡ b`, it is also possible to write the following:

``f params rewrite x = body``

``````f params with a | x
... | ._ | refl = body``````

The `rewrite` construct has the effect of rewriting the goal and the context by the given equation (left to right).

The function can be rewritten with using several equations (in sequence) by separating them with vertical bars (`|`):

``f params rewrite x₁ | x₂ | … = body``

It is also possible to add with clauses after rewriting:

``````f params rewrite xs with x
... | p = body``````

Note that pattern matching happens before rewriting. If you want to rewrite and then do pattern matching you can use a `with` after the rewrite.

# Proof for `Even`

Now try to construct the proof with using `Even`. As part of this, we will soon come to the conclusion that `¬Even1` is only possible to prove when a trick is employed:

```
¬Even1 : ∀ {n} → Even n → ¬ (n ≡ 1)
¬Even1 (double zero) ()
¬Even1 (double (suc zero)) ()
¬Even1 (double (suc (suc n))) ()```

For proving `nextEven`, we will need to do a rewriting (see above):

```
nextEven : ∀ {n} → Even n → Even (suc (suc n))
nextEven {.(n₁ + n₁)} (double n₁) rewrite (cong suc (suc-+ n₁ n₁)) = double (suc n₁)```

However, we could prove `prevEven` only with the help of `prevEven′` that demonstrates that `Even′` is actually easier to use:

```
prevEven : ∀ {n} → Even (suc (suc n)) → Even n
prevEven e = toEven (prevEven′ (toEven′ e))```

Note that proving `isEven` is similar to proving `isEven′`:

```
isEven : (n : ℕ) → Dec (Even n)
isEven zero       = yes (double zero)
isEven (suc zero) = no (λ x → ¬Even1 x refl)
isEven (suc (suc n)) with (isEven n)
... | yes e = yes (nextEven e)
... | no ¬p = no (λ x → ¬p (prevEven x))```

# Further examples

```
data  _≤″_ : ℕ → ℕ → Set  where
diff : ∀ i j → i ≤″ j + i

infix 4 _≤″_

data Vec (A : Set) : ℕ -> Set where
vec : (x : List A) -> Vec A (length x)```