[Agda] Re: Agda beats Coq

[Nils Anders Danielsson]

On 2008-11-21 10:01, Nils Anders Danielsson wrote:

>   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≈ ~ ?

> (Note that the pattern matching on {tree ._} is not part of Anton's
> approach [...]

Agda handles mixed recursion/corecursion now, so it is possible to
replace the definition above with the following:

   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₂} t₁≈t₂
     with destruct t₁ | destruct t₂ | destruct≈ t₁≈t₂
   ... | .leaf         | .leaf         | leaf          ~ tree leaf
   ... | .(node _ _ _) | .(node _ _ _) | node l≈ x≡ r≈ ~
     tree (node (map-cong f l≈) (≡-cong f x≡) (map-cong f r≈))

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