The Coq mailing list

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

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.

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)