Created
September 30, 2014 17:28
-
-
Save ahmadsalim/350bf6d21ea36353c86a to your computer and use it in GitHub Desktop.
Bisimulation proof in Agda with copatterns
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Inspired by http://www.cse.chalmers.se/research/group/logic/AIM/AIM6/SetzerCoInduction.pdf | |
| {-# OPTIONS --copatterns #-} | |
| module Bisim where | |
| data ℕ : Set where | |
| zero : ℕ | |
| succ : ℕ → ℕ | |
| {-# BUILTIN NATURAL ℕ #-} | |
| data Vec (A : Set) : ℕ → Set where | |
| [] : Vec A zero | |
| _∷_ : ∀ {n} → A → Vec A n → Vec A (succ n) | |
| data _≡_ {A : Set} (a : A) : A → Set where | |
| reflexive : a ≡ a | |
| record Stream (A : Set) : Set where | |
| coinductive | |
| constructor _∷_ | |
| field | |
| head : A | |
| tail : Stream A | |
| open Stream | |
| take : ∀ {n A} → Stream A → Vec A n | |
| take {zero} s = [] | |
| take {succ n} s = head s ∷ take {n} (tail s) | |
| ones : Stream ℕ | |
| head ones = 1 | |
| tail ones = ones | |
| ssucc : Stream ℕ → Stream ℕ | |
| head (ssucc s) = succ (head s) | |
| tail (ssucc s) = ssucc (tail s) | |
| twos : Stream ℕ | |
| head twos = 2 | |
| tail twos = twos | |
| record Bisim {A : Set} (s s' : Stream A) : Set where | |
| coinductive | |
| constructor _∷_ | |
| field | |
| phead : head s ≡ head s' | |
| ptail : Bisim (tail s) (tail s') | |
| open Bisim | |
| Bisim-ssucc⋆ones-twos : Bisim (ssucc ones) twos | |
| phead Bisim-ssucc⋆ones-twos = reflexive | |
| ptail Bisim-ssucc⋆ones-twos = Bisim-ssucc⋆ones-twos | |
| postulate bisim-eq : ∀ {A} {s s' : Stream A} → Bisim s s' → s ≡ s' | |
| succ⋆ones≡twos : ssucc ones ≡ twos | |
| succ⋆ones≡twos = bisim-eq Bisim-ssucc⋆ones-twos |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment