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]):
[tweet]: https://twitter.com/jonmsterling/status/1362803441974804483
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 tog : ImF
into this equation: explicit functionf : ExF
is propositionally equal to implicit functiong : 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 overrefl
, and apply this substitution to the goal, andg
gets replaced byλ {x} -> f x
. So, the result type is substituted tof ≡ (λ x -> f x)
, which, by Agda’s eta rule is a definitional equality. This process is similar to your pattern matching overp : 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 :)