[Agda] Re: Need help with coinductive proof

[Nils Anders Danielsson]

On 2009-08-26 11:59, Thorsten Altenkirch wrote:
> It is easy to show that it is a congruence for +'  but Agda doesn't seem 
> to like my proof of transitivity (even though I am quite sure it is 
> transitiv).

I have attached a proof of transitivity.

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

-------------- next part --------------
module Transitive where

open import Coinduction

data Coℕ′ : Set where
  zero : Coℕ′
  1+_  : (n : ∞ Coℕ′) → Coℕ′
  τ    : (n : ∞ Coℕ′) → Coℕ′

data _≈_ : Coℕ′ → Coℕ′ → Set where
  zero :                               zero ≈ zero
  1+_  : ∀ {m n} (p : ∞ (♭ m ≈ ♭ n)) → 1+ m ≈ 1+ n
  τ    : ∀ {m n} (p : ∞ (♭ m ≈ ♭ n)) → τ  m ≈ τ  n
  τʳ   : ∀ {m n} (p :      m ≈ ♭ n ) →    m ≈ τ  n
  τˡ   : ∀ {m n} (p :    ♭ m ≈   n ) → τ  m ≈    n

τʳ⁻¹ : ∀ {m n} → m ≈ τ n → m ≈ ♭ n
τʳ⁻¹ (τ  p) = τˡ    (♭ p)
τʳ⁻¹ (τʳ p) = p
τʳ⁻¹ (τˡ p) = τˡ (τʳ⁻¹ p)

τˡ⁻¹ : ∀ {m n} → τ m ≈ n → ♭ m ≈ n
τˡ⁻¹ (τ  p) = τʳ    (♭ p)
τˡ⁻¹ (τʳ p) = τʳ (τˡ⁻¹ p)
τˡ⁻¹ (τˡ p) = p

trans : ∀ {l m n} → l ≈ m → m ≈ n → l ≈ n

trans {l = zero} p q = tr p q
  where
  tr : ∀ {m n} → zero ≈ m → m ≈ n → zero ≈ n
  tr zero   q = q
  tr (τʳ p) q = tr p (τˡ⁻¹ q)

trans {l = 1+ l} p q = tr p q
  where
  tr : ∀ {l m n} → 1+ l ≈ m → m ≈ n → 1+ l ≈ n
  tr (1+ p) (1+ q) = 1+ (♯ trans (♭ p)   (♭ q))
  tr     p  (τʳ q) = τʳ (  tr       p       q)
  tr (τʳ p)     q  =       tr       p (τˡ⁻¹ q)

trans {l = τ l} p q = tr p q
  where
  tr : ∀ {l m n} → τ l ≈ m → m ≈ n → τ l ≈ n
  tr     p  (τ  q) = τ  (♯ trans (τˡ⁻¹ p) (τˡ (♭ q)))
  tr     p  (τʳ q) = τ  (♯ trans (τˡ⁻¹ p)        q)
  tr     p  (τˡ q) =       tr    (τʳ⁻¹ p)        q
  tr (τˡ p)     q  = τˡ (  trans       p         q)