Hacking Agda's pattern matching

Hacking Agda's pattern matching

2021, Mar 2 by Tesla Ice Zhang

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

RSS Feed