The Coq mailing list

[Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>]

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.