Brief background: I'm implementing contexts and renamings using de Bruijn indices, and then extending those notions with an "undefined" name, written ε. The undefined name induces a partial order on names in Γ, and also on renamings between Γ and Γ'. Looking up a name in a renaming (get
) and a related function put
which inverts get
in a specific way give rise to a (rather trivial) Galois connection. Here's the pared-down code:
module Temp where
open import Relation.Binary
open import Data.Fin using (Fin; zero; suc)
open import Data.Maybe renaming (nothing to ε; just to [_]) hiding (map)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
-- Pointed version of Fin, with ε indicating an undefined name.
Name : ℕ → Set
Name = Maybe ∘ Fin
-- The type of names below x.
data ↓_ {Γ} : Name Γ → Set where
ε : {x : Name Γ} → ↓ x
[_] : (x : Fin Γ) → ↓ [ x ]
-- A proof that two upper-bounded names are related.
data _≤_ {Γ} : {x : Name Γ} → ↓ x → ↓ x → Set where
ε : {x : Name Γ} {x : ↓ x} → ε ≤ x
[_] : (x : Fin Γ) → [ x ] ≤ [ x ]
≤-refl : ∀ {Γ} {y : Name Γ} → Reflexive (_≤_ {x = y})
≤-refl {x = ε} = ε
≤-refl {x = [ x ]} = [ x ]
-- Functorial action of suc on a name.
suc⁺₀ : ∀ {Γ} → Name Γ → Name (suc Γ)
suc⁺₀ ε = ε
suc⁺₀ [ x ] = [ suc x ]
-- Lifting of suc⁺₀ to down-sets.
suc⁺ : ∀ {Γ} {x : Name Γ} → ↓ x → ↓ suc⁺₀ x
suc⁺ ε = ε
suc⁺ [ x ] = [ suc x ]
-- A renaming from Γ Γ′.
data Ren : ℕ → ℕ → Set where
[] : ∀ {Γ} → Ren zero Γ
_∷_ : ∀ {Γ Γ′} → Name Γ′ → Ren Γ Γ′ → Ren (suc Γ) Γ′
-- The type of renamings below ρ.
data Ren-↓_ : ∀ {Γ Γ′} → Ren Γ Γ′ → Set where
[] : ∀ {Γ} → Ren-↓ ([] {Γ})
_∷_ : ∀ {Γ Γ′} {x : Name Γ′} {ρ : Ren Γ Γ′} →
↓ x → Ren-↓ ρ → Ren-↓ (x ∷ ρ)
-- Least renaming below ρ.
Ren-ε : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} → Ren-↓ ρ
Ren-ε {ρ = []} = []
Ren-ε {ρ = _ ∷ _} = ε ∷ Ren-ε
-- Interpret a renaming as a function.
get₀ : ∀ {Γ Γ′} → Ren Γ Γ′ × Name Γ → Name Γ′
get₀ (_ , ε) = ε
get₀ (x ∷ _ , [ zero ]) = x
get₀ (_ ∷ ρ , [ suc y ]) = get₀ (ρ , [ y ])
-- Lift get₀ to down-sets.
get : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} {x : Name Γ} →
Ren-↓ ρ × ↓ x → ↓ get₀ (ρ , x)
get (_ , ε) = ε
get (x ∷ _ , [ zero ]) = x
get ( _ ∷ ρ , [ suc x ]) = get (ρ , [ x ])
-- Lower adjoint of get.
put : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} (x : Name Γ) →
↓ get₀ (ρ , x) → Ren-↓ ρ × ↓ x
put ε ε = Ren-ε , ε
put {ρ = _ ∷ _} [ zero ] ε = Ren-ε , ε
put {ρ = ._ ∷ _} [ zero ] [ x ] = [ x ] ∷ Ren-ε , [ zero ]
put {ρ = _ ∷ _} [ suc x ] u = map (_∷_ ε) suc⁺ (put [ x ] u)
That's the set up. What I'd now like to do is show that get
and put
form a Galois connection. One way to do this is to show that each function is monotone, and that of their two composites, one is inflationary, and the other deflationary. This is all fine, except that I get stuck trying to show that the get∘put
composite is inflationary:
id≤get∘put : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} (x : Name Γ)
(u : ↓ get₀ (ρ , x)) → u ≤ get (put x u)
id≤get∘put ε ε = ε
id≤get∘put {ρ = _ ∷ _} [ zero ] ε = ε
id≤get∘put {ρ = ._ ∷ _} [ zero ] [ _ ] = ≤-refl
id≤get∘put {ρ = y ∷ ρ} [ suc x ] u
with put [ x ] u | id≤get∘put {ρ = ρ} [ x ] u
... | ρ′ , x′ | u′ = {!!}
In my context, I have that u ≤ get (ρ′ , x′)
from the recursive invocation of the function. I would like to be able to use this to derive the goal, namely u ≤ get (ε ∷ ρ′ , suc⁺ x′)
. Intuitively, this should be easy, as looking up x'
in ρ′
should be the same as looking up the successor of x'
in ρ′
extended with an additional name. In fact it should be easy to show that get (ρ′ , x′)
equals get (ε ∷ ρ′ , suc⁺ x′)
.
But if I try to state the corresponding lemma:
-- Not typeable, because ≡ requires homogeneous types?
postulate
not-ok : ∀ {Γ Γ′} {ρ : Ren Γ Γ′} {x : Name Γ}
(ρ′ : Ren-↓ ρ) (x′ : ↓ x) → get (ρ′ , x′) ≡ get (ε ∷ ρ′ , suc⁺ x′)
then Agda complains because the two invocations of get
(which is get₀
lifted to down-sets) have different types. This is because the type of get
mentions the value computed by get₀
.
However, the two invocations don't "really" have different types, in that I can prove the following lemma:
-- This is related to the lemma I want, but not quite it.
ok : ∀ {Γ Γ′} (ρ₀ : Ren Γ Γ′) (x₀ : Name Γ) →
get₀ (ρ₀ , x₀) ≡ get₀ (ε ∷ ρ₀ , suc⁺₀ x₀)
ok _ ε = refl
ok (_ ∷ _) [ zero ] = refl
ok (_ ∷ ρ) [ suc x ] = ok ρ [ x ]
I haven't yet used heterogeneous equality in Agda, and to be honest I don't really know how to use it. Would it allow me to state the lemma I need?