[Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)

[Nils Anders Danielsson]

On 2009-08-28 18:35, Edsko de Vries wrote:
> would Agda accept it?

Yes, the following relation is trivial:

  data _∼_ : PCoℕ → PCoℕ → Set where
    zero   :                                 zero  ∼ zero
    suc    : ∀ {m n} (m∼n : ∞ (♭ m ∼ ♭ n)) → suc m ∼ suc n
    τ      : ∀ {m n} (m∼n : ∞ (♭ m ∼ ♭ n)) → τ   m ∼ τ   n
    τˡ     : ∀ {m n} (m∼n :    ♭ m ∼   n ) → τ   m ∼     n
    τʳ     : ∀ {m n} (m∼n :      m ∼ ♭ n ) →     m ∼ τ   n

    -- Transitivity.
    _∼⟨_⟩_ : ∀ n₁ {n₂ n₃}
             (n₁∼n₂ : n₁ ∼ n₂) (n₂∼n₃ : n₂ ∼ n₃) → n₁ ∼ n₃

    -- Reflexivity.
    _∎     : ∀ n → n ∼ n

  trivial : ∀ m n → m ∼ n
  trivial m n =
    m       ∼⟨ τʳ (m ∎) ⟩
    τ (♯ m) ∼⟨ τ (♯ trivial m n) ⟩
    τ (♯ n) ∼⟨ τˡ (n ∎) ⟩
    n       ∎

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