InversionHell.lagda.md

description
Inversion hell.

module InversionHell where

Preterms in STLC

We start with an intrinsically scoped, extrinsically-typed raw syntax for STLC.

data Tp : Type where
  “𝕆” : Tp
  _“⇒”_ : Tp → Tp → Tp

data Tm (Γ : Nat) : Type where
  “var” : Fin Γ → Tm Γ
  “lam” : Tm (suc Γ) → Tm Γ
  “app” : Tm Γ → Tm Γ → Tm Γ
  “yes” : Tm Γ
  “no”  : Tm Γ

Renamings

The definition of renamings is standard.

data Rn : Nat → Nat → Type where
  doneʳ : Rn 0 0
  keepʳ : ∀ {Γ Δ} → Rn Γ Δ → Rn (suc Γ) (suc Δ)
  dropʳ : ∀ {Γ Δ} → Rn Γ Δ → Rn (suc Γ) Δ

Normal definitions of identities and composites.

idʳ : ∀ {Γ} → Rn Γ Γ
idʳ {Γ = zero} = doneʳ
idʳ {Γ = suc Γ} = keepʳ idʳ

_∘ʳ_ : ∀ {Γ Δ Θ} → Rn Δ Θ → Rn Γ Δ → Rn Γ Θ
ρ₁ ∘ʳ doneʳ = ρ₁
keepʳ ρ₁ ∘ʳ keepʳ ρ₂ = keepʳ (ρ₁ ∘ʳ ρ₂)
dropʳ ρ₁ ∘ʳ keepʳ ρ₂ = dropʳ (ρ₁ ∘ʳ ρ₂)
ρ₁ ∘ʳ dropʳ ρ₂ = dropʳ (ρ₁ ∘ʳ ρ₂)

Action of renaming on variables

Rather than implementing the action of renaming as a function, we implement it as a ternary relation. We do this for a couple of reasons:

• This is a green-slime prevention measure.
• This is what you get when you take the displayed POV seriously; note that this will end up being a discrete fibration over the category of renamings.
• Because Reed thinks it is interesting. No further explanation required 😎.

data RnVar : ∀ {Γ Δ} → Rn Γ Δ → Fin Δ → Fin Γ → Type where
  keep-zeroʳ
    : ∀ {Γ Δ} {ρ : Rn Γ Δ}
    → RnVar (keepʳ ρ) fzero fzero
  keep-sucʳ
    : ∀ {Γ Δ} {ρ : Rn Γ Δ} {i : Fin Δ} {i[ρ] : Fin Γ}
    → RnVar ρ i i[ρ]
    → RnVar (keepʳ ρ) (fsuc i) (fsuc i[ρ])
  dropʳ
    : ∀ {Γ Δ} {ρ : Rn Γ Δ} {i : Fin Δ} {i[ρ] : Fin Γ}
    → RnVar ρ i i[ρ]
    → RnVar (dropʳ ρ) i (fsuc i[ρ])

Now comes inversion hell. These lemmas aren't too bad.

keep-var-inv
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x : Fin Δ} {y : Fin Γ}
  → RnVar (keepʳ ρ) (fsuc x) (fsuc y) → RnVar ρ x y
keep-var-inv (keep-sucʳ x-ρ) = x-ρ

drop-var-inv
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x : Fin Δ} {y : Fin Γ}
  → RnVar (dropʳ ρ) x (fsuc y) → RnVar ρ x y
drop-var-inv (dropʳ x-ρ) = x-ρ

The inversion relation is decidable.

instance
  Dec-RnVar
    : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x : Fin Δ} {y : Fin Γ}
    → Dec (RnVar ρ x y)
  Dec-RnVar {ρ = keepʳ ρ} {x = fzero} {y = fzero} = yes keep-zeroʳ
  Dec-RnVar {ρ = keepʳ ρ} {x = fzero} {y = fsuc y} = no (λ ())
  Dec-RnVar {ρ = keepʳ ρ} {x = fsuc x} {y = fzero} = no (λ ())
  Dec-RnVar {ρ = keepʳ ρ} {x = fsuc x} {y = fsuc y} = invmap keep-sucʳ keep-var-inv (holds? (RnVar ρ x y))
  Dec-RnVar {ρ = dropʳ ρ} {x = x} {y = fzero} = no (λ ())
  Dec-RnVar {ρ = dropʳ ρ} {x = x} {y = fsuc y} = invmap dropʳ drop-var-inv (holds? (RnVar ρ x y))

This is when things start to get annoying. These inversion lemmas are basically the same as the ones above, but we need to write them separately.

keep-im-inv
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x[ρ] : Fin Γ}
  → Σ[ x ∈ Fin (suc Δ) ] (RnVar (keepʳ ρ) x (fsuc x[ρ]))
  → Σ[ x ∈ Fin Δ ] RnVar ρ x x[ρ]
keep-im-inv (fsuc x , keep-sucʳ ρ-x) = x , ρ-x

drop-im-inv
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x[ρ] : Fin Γ}
  → Σ[ x ∈ Fin Δ ] (RnVar (dropʳ ρ) x (fsuc x[ρ]))
  → Σ[ x ∈ Fin Δ ] RnVar ρ x x[ρ]
drop-im-inv (x , dropʳ ρ-x) = x , ρ-x

Better algorithm than a linear scan for computing preimages.

instance
  Dec-Inv-RnVar
    : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x[ρ] : Fin Γ}
    → Dec (Σ[ x ∈ Fin Δ ] RnVar ρ x x[ρ])
  {-# OVERLAPPING Dec-Inv-RnVar #-}

  Dec-Inv-RnVar {ρ = keepʳ ρ} {x[ρ] = fzero} = yes (fzero , keep-zeroʳ)
  Dec-Inv-RnVar {ρ = keepʳ ρ} {x[ρ] = fsuc x[ρ]} with holds? (Σ[ x ∈ Fin _ ] RnVar ρ x x[ρ])
  ... | yes (x , ρ-x) = yes (fsuc x , keep-sucʳ ρ-x)
  ... | no ¬ρ-x = no (¬ρ-x ∘ keep-im-inv)
  Dec-Inv-RnVar {ρ = dropʳ ρ} {x[ρ] = fzero} = no λ ()
  Dec-Inv-RnVar {ρ = dropʳ ρ} {x[ρ] = fsuc x[ρ]} with holds? (Σ[ x ∈ Fin _ ] RnVar ρ x x[ρ])
  ... | yes (x , ρ-x) = yes (x , dropʳ ρ-x)
  ... | no ¬ρ-x = no (¬ρ-x ∘ drop-im-inv)

Action of renaming on terms

This is when the suffering starts to really kick in.

data RnTm {Γ Δ} (ρ : Rn Γ Δ) : Tm Δ → Tm Γ → Type where
  “var”
    : ∀ {x : Fin Δ} {x[ρ] : Fin Γ}
    → RnVar ρ x x[ρ]
    → RnTm ρ (“var” x) (“var” x[ρ])
  “lam”
    : ∀ {e : Tm (suc Δ)} {e[ρ] : Tm (suc Γ)}
    → RnTm (keepʳ ρ) e e[ρ]
    → RnTm ρ (“lam” e) (“lam” e[ρ])
  “app”
    : ∀ {e₁ e₂ : Tm Δ} {e₁[ρ] e₂[ρ] : Tm Γ}
    → RnTm ρ e₁ e₁[ρ] → RnTm ρ e₂ e₂[ρ]
    → RnTm ρ (“app” e₁ e₂) (“app” e₁[ρ] e₂[ρ])
  “yes” : RnTm ρ “yes” “yes”
  “no” : RnTm ρ “no” “no”

So many inversion lemmas! If we add more cases, this just gets worse... We also need inversion lemmas for images as well. This feels like we should have a macro that generates all of the inversion lemmas, and then a class that lets us combines inversion lemmas for things like the image inversion lemmas, products of inversion lemmas, etc.

rn-tm-var-inv
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {x₁ : Fin Δ} {x₂ : Fin Γ}
  → RnTm ρ (“var” x₁) (“var” x₂)
  → RnVar ρ x₁ x₂
rn-tm-var-inv (“var” ρ-x) = ρ-x

rn-tm-lam-inv
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {e₁ : Tm (suc Δ)} {e₂ : Tm (suc Γ)}
  → RnTm ρ (“lam” e₁) (“lam” e₂)
  → RnTm (keepʳ ρ) e₁ e₂
rn-tm-lam-inv (“lam” ρ-e) = ρ-e

rn-tm-app-inv²
  : ∀ {Γ Δ} {ρ : Rn Γ Δ} {f₁ e₁ : Tm Δ} {f₂ e₂ : Tm Γ}
  → RnTm ρ (“app” f₁ e₁) (“app” f₂ e₂)
  → RnTm ρ f₁ f₂ × RnTm ρ e₁ e₂
rn-tm-app-inv² (“app” ρ-f ρ-e) = ρ-f , ρ-e

Living in disneyland

The code I'd like to write looks something like this:

-- Dec-Inv-RnVar {ρ = keepʳ ρ} {x[ρ] = fzero} = yes (fzero , keep-zeroʳ)
-- Dec-Inv-RnVar {ρ = keepʳ ρ} {x[ρ] = fsuc x[ρ]} = inversion (holds? (Σ[ x ∈ Fin _ ] RnVar ρ x x[ρ]))
-- Dec-Inv-RnVar {ρ = dropʳ ρ} {x[ρ] = fzero} = no λ ()
-- Dec-Inv-RnVar {ρ = dropʳ ρ} {x[ρ] = fsuc x[ρ]} = inversion (holds? (Σ[ x ∈ Fin _ ] RnVar ρ x x[ρ]))