Friday, 2 March 2012

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 

invL :  {α β δ γ}  (α  β  δ  γ)  α  δ
invL {.α} {β} {α} {.β} refl = refl

invR :  {α β δ γ}  (α  β  δ  γ)  β  γ
invR {.α} {β} {α} {.β} refl = refl

invL :  {α β δ γ}  (α  β  δ  γ)  α  δ
invL {.α} {β} {α} {.β} refl = refl

invR :  {α β δ γ}  (α  β  δ  γ)  β  γ
invR {.α} {β} {α} {.β} refl = refl

invL :  {α β δ γ}  (α  β  δ  γ)  α  δ
invL {.α} {β} {α} {.β} refl = refl

invR :  {α β δ γ}  (α  β  δ  γ)  β  γ
invR {.α} {β} {α} {.β} 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  invR)
(α  β)  (δ  γ) ty   | no p = no (p  invL)
(α  β)  (δ  γ) 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  invR)
(α  β)  (δ  γ) ty   | no p = no (p  invL)
(α  β)  (δ  γ) 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  invR)
(α  β)  (δ  γ) ty   | no p = no (p  invL)
(α  β)  (δ  γ) 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))

3 comments:

  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.

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

    ReplyDelete
  3. http://bantalsilikon01.blogspot.com/2014/10/perumahan-baru-di-tangerang-graha-raya.html
    http://marinirseo.blogspot.com/2014/10/perumahan-baru-di-tangerang-graha-raya.html
    http://kopiluwakliar01.blogspot.com/2014/10/perumahan-baru-di-tangerang-graha-raya.html
    http://marinir-seo.blogspot.com/2014/10/marinir-seo.html
    http://bantalsilikon01.blogspot.com/
    http://bantalsilikon01.blogspot.com/2014/11/bantal-silikon.html
    http://bantalsilikon01.blogspot.com/2014/10/rekomendasi-untuk-cloud-dedicated.html

    http://asdf-14.blogspot.com/2014/10/hhh.html
    http://vvtiin.blogspot.com/2014/10/iii.html
    http://dfes12.blogspot.com/2014/10/rrr.html
    http://jkt-49.blogspot.com/2014/10/ooo.html
    http://seo-aaa.blogspot.com/2014/10/lll.html
    http://agen-seo16.blogspot.com/2014/10/fff.html
    http://agen-seo19.blogspot.com/2014/10/ccc.html
    http://agen-seo20.blogspot.com/2014/10/bbb.html
    http://bumbu-pecel01.blogspot.com/2014/10/xxx.html
    http://marinirseo17.blogspot.com/2014/10/ddd.html
    http://bumbupecel16.blogspot.com/2014/10/eee.html
    http://bumbupecel15.blogspot.com/2014/10/ggg.html
    http://marinirseo14.blogspot.com/2014/10/hhh.html
    http://marinirseo12.blogspot.com/2014/10/jjj.html
    http://vvty-ine.blogspot.com/2014/10/nnn.html
    http://give-a-power.blogspot.com/2014/10/ooo.html
    http://bumbupecel-12.blogspot.com/2014/10/ppp.html
    http://guru-seo-praktisi-123.blogspot.com/2014/10/rrr.html
    http://kopiluwakmalang11.blogspot.com/2014/10/ttt.html
    http://seo-malang-19.blogspot.com/2014/10/bbb.html
    http://bantalasdf.blogspot.com/2014/10/aaa.html
    http://blog-seo-konsultasi10.blogspot.com/2014/10/marinir-seo-abc.html

    ReplyDelete