### 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.

### Generating etags automatically when needed

Have you ever wanted M-. (the emacs command which finds the definition of the term under the cursor) to just "do the right thing" and go to the most current definition site, but were in a language that didn't have an inferior process set-up to query about source locations correctly (as is done in lisp, ocaml and some other languages with sophisticated emacs interfaces)?

Well, fret no more. Here is an approach that will let you save the appropriate files and regenerate your TAGS file automatically when things change assuring that M-. takes you to the appropriate place.

You will have to reset the tags-table-list or set it when you first use M-. and you'll want to change the language given to find and etags in the 'create-prolog-tags function (as you're probably not using prolog), but otherwise it shouldn't require much customisation.

And finally, you will need to run etags once manually, or run 'M-x create-prolog-tags' in order to get the initia…

### 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 …

### Formalisation of Tables in a Dependent Language

I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of…