# Hacking Agda's pattern matching

by

Looooong time no see! Recently I have wrote some Agda, and I’ve found something worth writing about.

```{-# OPTIONS --allow-unsolved-meta #-}
module 2021-3-2-AgdaEtaFunc (A : Set) (B : A -> Set) where
open import Agda.Builtin.Equality
private ImF = forall {x} -> B x
private ExF = forall x -> B x
```

It all starts from a friend asking me about function extensionality in vanilla Agda (we all know we have that in cubical Agda). He postulated the extensionality of both implicit and explicit function types:

```Implicit = {f g : ImF} -> ((x : A) -> f {x} ≡ g {x}) -> _≡_ {A = ImF} f g
Explicit = {f g : ExF} -> ((x : A) -> f x ≡ g x) -> f ≡ g
```

And he wants to eliminate one of the postulates, because postulating is not elegant in general. So, I started with rewriting with `Implicit` to prove `Explicit`. Is that doable?

```explicit₀ : Implicit -> Explicit
explicit₀ im p rewrite im p  = {! im p !}
```

In the above goal, the type of `im p` is `(λ {x} -> f x) ≡ (λ {x} -> g x)`, and the goal type after rewrite is still `f ≡ g`. So, Agda is unhappy with this rewrite. Also, we have refined our goal: we wanna prove `(λ {x} -> f x) ≡ (λ {x} -> g x) -> f ≡ g`.

Note that we could prove these (that Jon pointed out in a tweet):

```fact₀ : {f g : ImF} -> (λ {x} -> f {x}) ≡ (λ {x} -> g {x}) -> _≡_ {A = ImF} f g
fact₀ p = p

fact₁ : {f g : ExF} -> (λ x -> f x) ≡ (λ x -> g x) -> f ≡ g
fact₁ p = p
```

But we could not turn `(λ {x} -> f x) ≡ (λ {x} -> g x)` to `f ≡ g`, because this function could not be eta-shortened. I think this is just impossible. In the end, I came up with a solution: I hacked Agda’s dependent pattern matching.

First, I proved a lemma that converts this equation:

explicit function `f : ExF` after an implicit eta expansion `λ {x} -> f x` is propositionally equal to `g : ImF`

into this equation:

explicit function `f : ExF` is propositionally equal to implicit function `g : ImF` after an explicit eta expansion `λ x -> g {x}`

The proof is reflexivity. I think it’s because Agda finds a MGU (most general unifier, see Norell and Jesper’s papers on pattern matching about this notion) – `[(λ {x} -> f x) / g]`, a substitution. It is the result of the positive success of the pattern matching over `refl`, and apply this substitution to the goal, and `g` gets replaced by `λ {x} -> f x`. So, the result type is substituted to `f ≡ (λ x -> f x)`, which, by Agda’s eta rule is a definitional equality.

This process is similar to your pattern matching over `p : a ≡ b` where Agda obtains `[a / b]` as a MGU and substitutes your goal with it. So, the very idea of this lemma is that the parameter type `(λ {x} -> f x) ≡ g` has its right-hand side in a reference form (unlike previously rewrited proofs, which are all eta-expanded lambdas).

```lemma : (f : ExF) (g : ImF) -> (λ {x} -> f x) ≡ g -> f ≡ (λ x -> g {x})
lemma _ _ refl = refl
```

With `lemma` we could very easily prove `Implicit -> Explicit`:

```explicit₁ : Implicit -> Explicit
explicit₁ im {f = f} {g = g} p = lemma f (λ {x} -> g x) (im p)
```

We could polish this proof with some inference capabilities in Agda, to make it shorter (and harder to read):

```explicit₂ : Implicit -> Explicit
explicit₂ im {g = g} p = lemma _ (g _) (im p)
```

I’ll leave the proof of `Explicit -> Implicit` as an exercise :)

Tweet this Top 