### Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language.

In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure.

And so we arrive at our story. In Coq, equality is something of a nightmare. In Agda, by contrast, often times this nightmare is avoided with clever structuring of the rules for elimination in pattern matching. However, Agda's lack of a system of tactics brings the nightmare home to roost in a different nest. This proof was 1 line in Coq, and amounts to evocation of the tactic decide equality. decide equality..

(Thanks to Saizan for showing me how to do this: Eq.agda)

First of course, we need to set up our modules etc...

```module SystemFPlus where

open import Function
open import Data.Fin using (Fin)
open import Data.Nat hiding (_*_)
open import Data.Bool renaming (_≟_ to _≟_Bool)
open import Data.List
open import Data.Unit using (⊤)
open import Relation.Nullary.Core
open import Data.Sum
open import Data.Product
--open import Relation.Binary.EqReasoning
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; refl)
```

Next we write down an inductive definition for System-F style types.

```data Ty : Set where
① : Ty                -- unit type
ι : ℕ → Ty           -- universal abstraction vars
η : ℕ → Ty           -- μ vars
_⇒_ : Ty → Ty → Ty  -- implication
_⊗_ : Ty → Ty → Ty  -- conjunction
_⊕_ : Ty → Ty → Ty  -- disjunction
μ : Ty → Ty          -- inductive types
Π : Ty → Ty          -- universal quantification
```

Next we have to do the business which is relatively usual in Agda, when proving negative goals under a constructor, that is, define explicit inversion principles. It turns out that you don't generally have to do this if you're not under a constructor and inside a λ but I haven't found a way to avoid it when you are, and you almost always are when you're proving false for something decidable.

```invι : ∀ {n m} → (ι n ≡ ι m) → n ≡ m
invι refl = refl

invη : ∀ {n m} → (η n ≡ η m) → n ≡ m
invη refl = refl

invμ : ∀ {α β} → (μ α ≡ μ β) → α ≡ β
invμ refl = refl

invΠ : ∀ {α β} → (Π α ≡ Π β) → α ≡ β
invΠ refl = refl

inv⇒L : ∀ {α β δ γ} → (α ⇒ β ≡ δ ⇒ γ) → α ≡ δ
inv⇒L {.α} {β} {α} {.β} refl = refl

inv⇒R : ∀ {α β δ γ} → (α ⇒ β ≡ δ ⇒ γ) → β ≡ γ
inv⇒R {.α} {β} {α} {.β} refl = refl

inv⊕L : ∀ {α β δ γ} → (α ⊕ β ≡ δ ⊕ γ) → α ≡ δ
inv⊕L {.α} {β} {α} {.β} refl = refl

inv⊕R : ∀ {α β δ γ} → (α ⊕ β ≡ δ ⊕ γ) → β ≡ γ
inv⊕R {.α} {β} {α} {.β} refl = refl

inv⊗L : ∀ {α β δ γ} → (α ⊗ β ≡ δ ⊗ γ) → α ≡ δ
inv⊗L {.α} {β} {α} {.β} refl = refl

inv⊗R : ∀ {α β δ γ} → (α ⊗ β ≡ δ ⊗ γ) → β ≡ γ
inv⊗R {.α} {β} {α} {.β} refl = refl
```

Now comes the epic annoyance. This function could have been written by a program. It's absolutely vanilla, and yet I'm forced to write out the full cross-product of possibilities almost all of which lead to the conclusion: (λ ()), which is essentially, "no, and you should know why". Since it knows why, it seems unnecessarily arduous for me to have to write out every case!

```_≟_ty : Decidable {A = Ty} _≡_
①       ≟ ① ty      = yes refl
①       ≟ (ι m) ty   = no (λ ())
①       ≟ (η m) ty   = no (λ ())
①       ≟ (δ ⇒ γ) ty = no (λ ())
①       ≟ (δ ⊕ γ) ty = no (λ ())
①       ≟ (δ ⊗ γ) ty = no (λ ())
①       ≟ (μ β) ty   = no (λ ())
①       ≟ (Π β) ty   = no (λ ())
(ι n)   ≟ ① ty       = no (λ ())
(ι n)   ≟ (ι m) ty   with n ≟ m
(ι .n)  ≟ (ι n) ty   | yes refl = yes refl
(ι n)   ≟ (ι m) ty   | no p  = no (p ∘ invι)
(ι n)   ≟ (η m) ty   = no (λ ())
(ι n)   ≟ (δ ⇒ γ) ty = no (λ ())
(ι n)   ≟ (δ ⊕ γ) ty = no (λ ())
(ι n)   ≟ (δ ⊗ γ) ty = no (λ ())
(ι n)   ≟ (μ β) ty   = no (λ ())
(ι n)   ≟ (Π β) ty   = no (λ ())
(η n)   ≟ ① ty       = no (λ ())
(η n)   ≟ (ι m) ty   = no (λ ())
(η n)   ≟ (η m) ty   with n ≟ m
(η .n)  ≟ (η n) ty   | yes refl = yes refl
(η n)   ≟ (η m) ty   | no p  = no (p ∘ invη)
(η n)   ≟ (δ ⇒ γ) ty = no (λ ())
(η n)   ≟ (δ ⊕ γ) ty = no (λ ())
(η n)   ≟ (δ ⊗ γ) ty = no (λ ())
(η n)   ≟ (μ β) ty   = no (λ ())
(η n)   ≟ (Π β) ty   = no (λ ())
(μ α)   ≟ ① ty       = no (λ ())
(μ α)   ≟ (ι m) ty   = no (λ ())
(μ α)   ≟ (η m) ty   = no (λ ())
(μ α)   ≟ (δ ⇒ γ) ty = no (λ ())
(μ α)   ≟ (δ ⊕ γ) ty = no (λ ())
(μ α)   ≟ (δ ⊗ γ) ty = no (λ ())
(μ α)   ≟ (μ β) ty   with α ≟ β ty
(μ .β)  ≟ (μ β) ty   | yes refl = yes refl
(μ α)   ≟ (μ β) ty   | no p  = no (p ∘ invμ)
(μ α)   ≟ (Π β) ty   = no (λ ())
(Π α)   ≟ ① ty       = no (λ ())
(Π α)   ≟ (ι m) ty   = no (λ ())
(Π α)   ≟ (η m) ty   = no (λ ())
(Π α)   ≟ (δ ⇒ γ) ty = no (λ ())
(Π α)   ≟ (δ ⊕ γ) ty = no (λ ())
(Π α)   ≟ (δ ⊗ γ) ty = no (λ ())
(Π α)   ≟ (Π β) ty   with α ≟ β ty
(Π .α)  ≟ (Π α) ty   | yes refl = yes refl
(Π α)   ≟ (Π β) ty   | no p  = no (p ∘ invΠ)
(Π α)   ≟ (μ β) ty   = no (λ ())
(α ⇒ β) ≟ ① ty      = no (λ ())
(α ⇒ β) ≟ (ι m) ty   = no (λ ())
(α ⇒ β) ≟ (η m) ty   = no (λ ())
(α ⇒ β) ≟ (δ ⇒ γ) ty   with α ≟ δ ty
(.α ⇒ β) ≟ (α ⇒ γ) ty  | yes refl with β ≟ γ ty
(.α ⇒ .β) ≟ (α ⇒ β) ty | yes refl | yes refl = yes refl
(.α ⇒ δ) ≟ (α ⇒ γ) ty  | yes refl | no p = no (p ∘ inv⇒R)
(α ⇒ β) ≟ (δ ⇒ γ) ty   | no p = no (p ∘ inv⇒L)
(α ⇒ β) ≟ (δ ⊕ γ) ty = no (λ ())
(α ⇒ β) ≟ (δ ⊗ γ) ty = no (λ ())
(α ⇒ β) ≟ (μ δ) ty   = no (λ ())
(α ⇒ β) ≟ (Π δ) ty   = no (λ ())
(α ⊕ β) ≟ ① ty      = no (λ ())
(α ⊕ β) ≟ (ι m) ty   = no (λ ())
(α ⊕ β) ≟ (η m) ty   = no (λ ())
(α ⊕ β) ≟ (δ ⊕ γ) ty   with α ≟ δ ty
(.α ⊕ β) ≟ (α ⊕ γ) ty  | yes refl with β ≟ γ ty
(.α ⊕ .β) ≟ (α ⊕ β) ty | yes refl | yes refl = yes refl
(.α ⊕ δ) ≟ (α ⊕ γ) ty  | yes refl | no p = no (p ∘ inv⊕R)
(α ⊕ β) ≟ (δ ⊕ γ) ty   | no p = no (p ∘ inv⊕L)
(α ⊕ β) ≟ (δ ⇒ γ) ty = no (λ ())
(α ⊕ β) ≟ (δ ⊗ γ) ty = no (λ ())
(α ⊕ β) ≟ (μ δ) ty   = no (λ ())
(α ⊕ β) ≟ (Π δ) ty   = no (λ ())
(α ⊗ β) ≟ ① ty      = no (λ ())
(α ⊗ β) ≟ (ι m) ty   = no (λ ())
(α ⊗ β) ≟ (η m) ty   = no (λ ())
(α ⊗ β) ≟ (δ ⊗ γ) ty   with α ≟ δ ty
(.α ⊗ β) ≟ (α ⊗ γ) ty  | yes refl with β ≟ γ ty
(.α ⊗ .β) ≟ (α ⊗ β) ty | yes refl | yes refl = yes refl
(.α ⊗ δ) ≟ (α ⊗ γ) ty  | yes refl | no p = no (p ∘ inv⊗R)
(α ⊗ β) ≟ (δ ⊗ γ) ty   | no p = no (p ∘ inv⊗L)
(α ⊗ β) ≟ (δ ⇒ γ) ty = no (λ ())
(α ⊗ β) ≟ (δ ⊕ γ) ty = no (λ ())
(α ⊗ β) ≟ (μ δ) ty   = no (λ ())
(α ⊗ β) ≟ (Π δ) ty   = no (λ ())
```

Well there has to be a better way right? So I thought I'd try to cook one up. It turns out that you can solve a decidable equality problem by injection into a domain with a decidable equality. So I went about thinking about what kind of decidable equality might have a domain with a similar enough shape that we could do the incoding without to much difficulty. I came up with the following program. It hardly saves any time at all unfortunately, but it does make me wonder if there isn't a more efficient way of doing it, perhaps using vectors, modules with decidable equalities for the carried data and with a single data constructor. Perhaps containers are the solution? I'm not sure. Anyhow, if you have a big inductive data type (such as a rich programming term language) this approach might save you trouble.

The trick is essentially to create an isomorphism with something like a Gödel coding. Since numbers are a hassle, and we need to have an isomorphism, it's more natural to do it into a space of trees where the trees have the same basic shape. We encode each operator as a number up to a finite size, whose limited nature is dictated by Fin n. This ensures that we don't have to worry about what to do with numbers bigger than the number of operators we have. The rest should be fairly self explanatory. Hopefully this gives someone ideas of a better way...

```module TyDec where

open import Function using (_∘_)
open import Data.Nat hiding (_*_)
open import Data.Fin renaming (zero to fzero ; suc to fsuc)
open import Data.Fin.Props renaming (_≟_ to _≟_fin)
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Relation.Nullary.Core
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; refl; trans; sym; cong)

data Ty : Set where
① : Ty
ι : ℕ → Ty
η : ℕ → Ty
μ : Ty → Ty
Π : Ty → Ty
_⇒_ : Ty → Ty → Ty
_⊗_ : Ty → Ty → Ty
_⊕_ : Ty → Ty → Ty

data Tree : Set where
Nullary : Tree
NullaryNat : Fin 2 → ℕ → Tree
Unary : Fin 2 → Tree → Tree
Binary : Fin 3 → Tree → Tree → Tree

invNullaryNat1 : ∀ {op1 op2 n1 n2} → NullaryNat op1 n1 ≡ NullaryNat op2 n2 → op1 ≡ op2
invNullaryNat1 refl = refl

invNullaryNat2 : ∀ {op1 op2 n1 n2} → NullaryNat op1 n1 ≡ NullaryNat op2 n2 → n1 ≡ n2
invNullaryNat2 refl = refl

invUnary1 : ∀ {op1 op2 t1 t2} → Unary op1 t1 ≡ Unary op2 t2 → op1 ≡ op2
invUnary1 refl = refl

invUnary2 : ∀ {op1 op2 t1 t2} → Unary op1 t1 ≡ Unary op2 t2 → t1 ≡ t2
invUnary2 refl = refl

invBinary1 : ∀ {op1 op2 l1 l2 r1 r2} → Binary op1 l1 r1 ≡ Binary op2 l2 r2 → op1 ≡ op2
invBinary1 refl = refl

invBinary2 : ∀ {op1 op2 l1 l2 r1 r2} → Binary op1 l1 r1 ≡ Binary op2 l2 r2 → l1 ≡ l2
invBinary2 refl = refl

invBinary3 : ∀ {op1 op2 l1 l2 r1 r2} → Binary op1 l1 r1 ≡ Binary op2 l2 r2 → r1 ≡ r2
invBinary3 refl = refl

_≟_tree : Decidable {A = Tree} _≡_
Nullary               ≟ Nullary               tree = yes refl
Nullary               ≟ (NullaryNat op n)     tree = no (λ())
Nullary               ≟ (Unary op t)          tree = no (λ())
Nullary               ≟ (Binary op l r)       tree = no (λ())
(NullaryNat op n)     ≟ Nullary               tree = no (λ ())
(NullaryNat op1 n1)   ≟ (NullaryNat op2 n2)   tree with op1 ≟ op2 fin
(NullaryNat .op1 n1)  ≟ (NullaryNat op1 n2)   tree | yes refl with n1 ≟ n2
(NullaryNat .op1 .n1) ≟ (NullaryNat op1 n1)   tree | yes refl | yes refl = yes refl
(NullaryNat .op1 n1)  ≟ (NullaryNat op1 n2)   tree | yes refl | no p = no (p ∘ invNullaryNat2)
(NullaryNat op1 n1)   ≟ (NullaryNat op2 n2)   tree | no p  = no (p ∘ invNullaryNat1)
(NullaryNat op1 n1)   ≟ (Unary op t)          tree = no (λ())
(NullaryNat op1 n1)   ≟ (Binary op l r)       tree = no (λ())
(Unary op1 t1)        ≟ Nullary               tree = no (λ())
(Unary op1 t1)        ≟ (NullaryNat op n)     tree = no (λ())
(Unary op1 t1)        ≟ (Unary op2 t2)        tree with op1 ≟ op2 fin
(Unary .op1 t1)       ≟ (Unary op1 t2)        tree | yes refl with t1 ≟ t2 tree
(Unary .op1 .t1)      ≟ (Unary op1 t1)        tree | yes refl | yes refl = yes refl
(Unary .op1 t1)       ≟ (Unary op1 t2)        tree | yes refl | no p = no (p ∘ invUnary2)
(Unary op1 t1)        ≟ (Unary op2 t2)        tree | no p = no (p ∘ invUnary1)
(Unary op1 t1)        ≟ (Binary op2 l r)      tree = no (λ())
(Binary op l r)       ≟ Nullary               tree = no (λ())
(Binary op1 l r)      ≟ (NullaryNat op2 n)    tree = no (λ())
(Binary op1 l r)      ≟ (Unary op2 t)         tree = no (λ())
(Binary op1 l1 r1)    ≟ (Binary op2 l2 r2)    tree with op1 ≟ op2 fin
(Binary .op1 l1 r1)   ≟ (Binary op1 l2 r2)    tree | yes refl with l1 ≟ l2 tree
(Binary .op1 .l1 r1)  ≟ (Binary op1 l1 r2)    tree | yes refl | yes refl with r1 ≟ r2 tree
(Binary .op1 .l1 .r1) ≟ (Binary op1 l1 r1)    tree | yes refl | yes refl | yes refl = yes refl
(Binary .op1 .l1 r1)  ≟ (Binary op1 l1 r2)    tree | yes refl | yes refl | no p = no (p ∘ invBinary3)
(Binary .op1 l1 r1)   ≟ (Binary op1 l2 r2)    tree | yes refl | no p = no (p ∘ invBinary2)
(Binary op1 l1 r1)    ≟ (Binary op2 l2 r2)    tree | no p = no (p ∘ invBinary1)

{-
Op codes

Nullary
ι = 0
η = 1

Unary
μ = 0
Π = 1

Binary
⇒ = 0
⊗ = 1
⊕ = 2
-}

jni : Tree → Ty
jni Nullary                              = ①
jni (NullaryNat fzero n)                 = ι n
jni (NullaryNat (fsuc fzero) n)          = η n
jni (NullaryNat (fsuc (fsuc ())) n)
jni (Unary fzero t)                      = μ (jni t)
jni (Unary (fsuc fzero) t)               = Π (jni t)
jni (Unary (fsuc (fsuc ())) t)
jni (Binary fzero l r)                   = (jni l) ⇒ (jni r)
jni (Binary (fsuc fzero) l r)            = (jni l) ⊗ (jni r)
jni (Binary (fsuc (fsuc fzero)) l r)     = (jni l) ⊕ (jni r)
jni (Binary (fsuc (fsuc (fsuc ()))) l r)

injEx : (x : Ty) -> Σ Tree \ t -> jni t ≡ x
injEx ①                         = Nullary , refl
injEx (ι n)                     = NullaryNat fzero n , refl
injEx (η n)                     = NullaryNat (fsuc fzero) n , refl
injEx (μ t)                     with injEx t
injEx (μ .(jni tree))           | tree , refl = (Unary fzero tree) , refl
injEx (Π t)                     with injEx t
injEx (Π .(jni tree))           | tree , refl = (Unary (fsuc fzero) tree) , refl
injEx (t ⇒ s)                   with injEx t
injEx (.(jni tr1) ⇒ s)          | tr1 , refl with injEx s
injEx (.(jni tr1) ⇒ .(jni tr2)) | tr1 , refl | tr2 , refl = (Binary fzero tr1 tr2) , refl
injEx (t ⊗ s)                   with injEx t
injEx (.(jni tr1) ⊗ s)          | tr1 , refl with injEx s
injEx (.(jni tr1) ⊗ .(jni tr2)) | tr1 , refl | tr2 , refl = (Binary (fsuc fzero) tr1 tr2) , refl
injEx (t ⊕ s)                   with injEx t
injEx (.(jni tr1) ⊕ s)          | tr1 , refl with injEx s
injEx (.(jni tr1) ⊕ .(jni tr2)) | tr1 , refl | tr2 , refl = (Binary (fsuc (fsuc fzero)) tr1 tr2) , refl

inj : Ty → Tree
inj = proj₁ ∘ injEx -- strip off the existential proof

injeq : ∀ {x y} -> inj x ≡ inj y -> x ≡ y
injeq {x} {y} p = trans (sym (proj₂ (injEx _))) (trans (cong jni p) (proj₂ (injEx _)))

_≟_ty : (x y : Ty) -> Dec (x ≡ y)
x ≟ y ty with (inj x) ≟ (inj y) tree
x ≟ y ty | yes p = yes (injeq p)
x ≟ y ty | no p = no (p ∘ (cong inj))
```

1. > It's absolutely vanilla, and yet I'm forced to write out the full cross-product of possibilities almost all of which lead to the conclusion: (λ ()), which is essentially, "no, and you should know why".
How do case split, refine and auto do here? I never yet semi-auto-generated something that big, yet at least the trivial cases should be within reach (and you can report bugs if not).
Also, I understand that reflection enables writing tactics - but that Agda is not focusing on going after Coq but on programming, because competition is too strong on theorem proving per se.

2. I used split refine and auto on these, but it still takes a long time and generates an irritatingly large amount of code.

### Managing state in Prolog monadically, using DCGs.

Prolog is a beautiful language which makes a lot of irritating rudimentary rule application and search easy. I have found it is particularly nice when trying to deal with compilers which involve rule based transformation from a source language L to a target language L'.

However, the management of these rules generally requires keeping track of a context, and this context has to be explicitly threaded through the entire application, which involves a lot of irritating and error prone sequence variables. This often leads to your code looking something a bit like this:

compile(seq(a,b),(ResultA,ResultB),S0,S2) :- compile(a,ResultA,S0,S1), compile(b,ResultB,S1,S2).
While not the worst thing, I've found it irritating and ugly, and I've made a lot of mistakes with incorrectly sequenced variables. It's much easier to see sequence made explicitly textually in the code.

While they were not designed for this task, but rather for parsing, DCGs turn out to be a convenient …

### Automated Deduction and Functional Programming

I just got "ML for the working programmer" in the mail a few days ago,
and worked through it at a breakneck pace since receiving it. It
turns out that a lot of the stuff from the "Total Functional
Programming" book is also in this one. Paulson goes through the use
of structural recursion and extends the results by showing techniques
for proving a large class of programs to be terminating. Work with
co-algebras and bi-simulation didn't quite make it in, except for a