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)

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

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

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

`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

`rewrite`

constructIf `x : a ≡ b`

, it is also possible to write the following:

`f params rewrite x = body`

instead of that:

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

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

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)