[Agda] Re: Agda beats Coq

[Nils Anders Danielsson]

On 2008-11-20 23:21, Dan Doel wrote:

> [...] all the unfolding that needs to happen to make types check
> automatically happens because of the observations we need to make.

This is the key point. I have another example, which I think illustrates
this well.

First an unsuccessful codata approach:

   -- Possibly infinite trees.

   codata Tree (A : Set) : Set where
     leaf : Tree A
     node : (l : Tree A) (x : A) (r : Tree A) -> Tree A

   map : forall {A B} -> (A -> B) -> Tree A -> Tree B
   map f leaf         ~ leaf
   map f (node l x r) ~ node (map f l) (f x) (map f r)

   -- Tree equality.

   codata _≈_ {A : Set} : (t₁ t₂ : Tree A) -> Set where
     leaf : leaf ≈ leaf
     node : forall {l₁ l₂ x₁ x₂ r₁ r₂}
            (l≈ : l₁ ≈ l₂) (x≡ : x₁ ≡ x₂) (r≈ : r₁ ≈ r₂) ->
            node l₁ x₁ r₁ ≈ node l₂ x₂ r₂

   map-cong : forall {A B} (f : A -> B) {t₁ t₂ : Tree A} ->
              t₁ ≈ t₂ -> map f t₁ ≈ map f t₂
   map-cong f leaf            ~ ?
   map-cong f (node l≈ x≡ r≈) ~ ?

How do you prove that map preserves equality? The type of the last goal
is

   map f (node .l₁ .x₁ .r₁) ≈ map f (node .l₂ .x₂ .r₂),

and the node constructor of _≈_ does not match this type. One can
perhaps get around this in some way, but the proof will likely be
inelegant.

Let's try to emulate Anton's approach instead (without his syntactic
sugar, since it has not been implemented):

   mutual

     data TreeD (A : Set) : Set where
       leaf : TreeD A
       node : (l : Tree A) (x : A) (r : Tree A) -> TreeD A

     codata Tree (A : Set) : Set where
       tree : (d : TreeD A) -> Tree A

   destruct : forall {A} -> Tree A -> TreeD A
   destruct (tree d) = d

   map : forall {A B} -> (A -> B) -> Tree A -> Tree B
   map f t with destruct t
   map f t | leaf       ~ tree leaf
   map f t | node l x r ~ tree (node (map f l) (f x) (map f r))

   mutual

     data _≈D_ {A : Set} : (t₁ t₂ : TreeD A) -> Set where
       leaf : leaf ≈D leaf
       node : forall {l₁ l₂ x₁ x₂ r₁ r₂}
              (l≈ : l₁ ≈ l₂) (x≡ : x₁ ≡ x₂) (r≈ : r₁ ≈ r₂) ->
              node l₁ x₁ r₁ ≈D node l₂ x₂ r₂

     -- Note that the type is not indexed on codata, only parameterised.

     codata _≈_ {A : Set} (t₁ t₂ : Tree A) : Set where
       tree : (d≈ : destruct t₁ ≈D destruct t₂) -> t₁ ≈ t₂

   destruct≈ : forall {A} {t₁ t₂ : Tree A} ->
               t₁ ≈ t₂ -> destruct t₁ ≈D destruct t₂
   destruct≈ (tree eq) = eq

   map-cong : forall {A B} (f : A -> B) {t₁ t₂ : Tree A} ->
              t₁ ≈ t₂ -> map f t₁ ≈ map f t₂
   map-cong f t₁≈t₂ with destruct≈ t₁≈t₂
   map-cong f {tree ._} {tree ._} t₁≈t₂ | leaf          ~ ?
   map-cong f {tree ._} {tree ._} t₁≈t₂ | node l≈ x≡ r≈ ~ ?

Now the last goal has type

   map f (tree (node .l₁ .x₁ .r₁)) ≈ map f (tree (node .l₂ .x₂ .r₂)).

Note that we can use the tree constructor of _≈_ here, because its type
matches anything. In

   map-cong f {tree ._} {tree ._} t₁≈t₂ | node l≈ x≡ r≈ ~ tree ?

the goal has type

   destruct (map f (tree (node .l₁ .x₁ .r₁))) ≈D
   destruct (map f (tree (node .l₂ .x₂ .r₂)))

which, due to the presence of destruct, evaluates to

   node (map f .l₁) (f .x₁) (map f .r₁) ≈D
   node (map f .l₂) (f .x₂) (map f .r₂),

which can easily be proved. Note that there is no need to use explicit
unfoldings; the use of destruct in the type of tree ensures that things
evaluate exactly when we want them to (in this example, at least).

(Note that the pattern matching on {tree ._} is not part of Anton's
approach, but I think it is harmless. In fact, both map and map-cong
could just as well be written without destruct(≈):

   map : forall {A B} -> (A -> B) -> Tree A -> Tree B
   map f (tree leaf)         ~ tree leaf
   map f (tree (node l x r)) ~ tree (node (map f l) (f x) (map f r))

   map-cong : forall {A B} (f : A -> B) {t₁ t₂ : Tree A} ->
              t₁ ≈ t₂ -> map f t₁ ≈ map f t₂
   map-cong f {tree ._} {tree ._} (tree leaf)            ~ tree leaf
   map-cong f {tree ._} {tree ._} (tree (node l≈ x≡ r≈)) ~
     tree (node (map-cong f l≈) (≡-cong f x≡) (map-cong f r≈))

However, destruct needs to be used in _≈_.)

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.