为了尝试不同的方法，我决定使用列表语义的数据类型：
data Sem (A : Set) : Set where
[] : Sem A
⊥ : Sem A
_∷_ : A → ∞ (Sem A) → Sem A
以及列表及其语义之间不可判定的二元关系：
data _HasSem_ {A : Set} : Colist (Maybe A) → Sem A → Set where
[] : [] HasSem []
⊥ : ∀ {l} → ∞ (♭ l HasSem ⊥) → (nothing ∷ l) HasSem ⊥
n∷_ : ∀ {l s} → ♭ l HasSem s → (nothing ∷ l) HasSem s
_∷_ : ∀ {l s} x → ∞ (♭ l HasSem ♭ s) → (just x ∷ l) HasSem (x ∷ s)
然后从语义上定义列表相等性很容易：
a ≈ b = ∀ s → a HasSem s → b HasSem s
isEquivalence 基本上是微不足道的，除了sym，看起来你需要使箭头双向（a HasSem ⇔ b HasSem s）以建设性地证明这一点。
然后我试图证明我的平等概念等同于 copumpkin 的，但我遇到了一些麻烦。我能够建设性地证明一个方向：
from : ∀ {a b} → a ∼ b → a ≈ b
但是，在假设 Excluded Middle 之后，我只能走另一个方向：
LEM = (A : Set) → Dec A
to : LEM → ∀ {a b} → a ≈ b → a ∼ b
我无法证明任何一个更好的非建设性版本to：
nicer-to : ∀ {a b} → a ≈ b → ¬ ¬ a ∼ b -- Not proven
完整代码如下。还有一些其他属性的证明，例如语义的存在性和唯一性证明，假设为 LEM。
module colists where
open import Coinduction
open import Data.Colist hiding (_≈_)
data Sem (A : Set) : Set where
[] : Sem A
⊥ : Sem A
_∷_ : A → ∞ (Sem A) → Sem A
open import Data.Maybe
data _HasSem_ {A : Set} : Colist (Maybe A) → Sem A → Set where
[] : [] HasSem []
⊥ : ∀ {l} → ∞ (♭ l HasSem ⊥) → (nothing ∷ l) HasSem ⊥
n∷_ : ∀ {l s} → ♭ l HasSem s → (nothing ∷ l) HasSem s
_∷_ : ∀ {l s} x → ∞ (♭ l HasSem ♭ s) → (just x ∷ l) HasSem (x ∷ s)
open import Function.Equivalence
_≈_ : ∀ {A : Set} → Colist (Maybe A) → Colist (Maybe A) → Set
a ≈ b = ∀ s → a HasSem s → b HasSem s
data _∼_ {A : Set} : Colist (Maybe A) → Colist (Maybe A) → Set where
end : [] ∼ []
nothings : ∀ { xs ys} (r : ∞ (♭ xs ∼ ♭ ys)) → (nothing ∷ xs) ∼ (nothing ∷ ys)
nothingˡ : ∀ { xs ys} (r : (♭ xs ∼ ys)) → (nothing ∷ xs) ∼ ys
nothingʳ : ∀ { xs ys} (r : ( xs ∼ ♭ ys)) → xs ∼ (nothing ∷ ys)
justs : ∀ {x xs ys} (r : ∞ (♭ xs ∼ ♭ ys)) → (just x ∷ xs) ∼ (just x ∷ ys)
module WithA (A : Set) where
CLMA = Colist (Maybe A)
from-[] : ∀ {a b : CLMA} → a ∼ b → a HasSem [] → b HasSem []
from-[] end [] = []
from-[] (nothingʳ r) a-has = n∷ (from-[] r a-has)
from-[] (nothings r) (n∷ y) = n∷ (from-[] (♭ r) y)
from-[] (nothingˡ r) (n∷ y) = from-[] r y
from-[] (justs _) ()
from-⊥ : ∀ {a b : CLMA} → a ∼ b → a HasSem ⊥ → b HasSem ⊥
from-⊥ (nothings r) (⊥ y) = ⊥ (♯ (from-⊥ (♭ r) (♭ y)))
from-⊥ (nothingˡ r) (⊥ y) = from-⊥ r (♭ y)
from-⊥ (nothingʳ r) (⊥ y) = ⊥ (♯ (from-⊥ r (⊥ y)))
from-⊥ (nothings r) (n∷ y) = ⊥ (♯ (from-⊥ (♭ r) y))
from-⊥ (nothingˡ r) (n∷ y) = from-⊥ r y
from-⊥ (nothingʳ r) (n∷ y) = ⊥ (♯ (from-⊥ r (⊥ (♯ y))))
from-⊥ (justs _) ()
from-⊥ end ()
from' : ∀ {a b : CLMA} {s} → a ∼ b → a HasSem s → b HasSem s
from-∷ : ∀ {a b : CLMA} {x s} → a ∼ b → a HasSem (x ∷ s) → b HasSem (x ∷ s)
from' {a} {b} {[]} eq sem = from-[] eq sem
from' {a} {b} {⊥} eq sem = from-⊥ eq sem
from' {a} {b} {y ∷ y'} eq sem = from-∷ eq sem
from-∷ (nothings r) (n∷ y) = n∷ from-∷ (♭ r) y
from-∷ (nothingˡ r) (n∷ y) = from-∷ r y
from-∷ (nothingʳ r) (n∷ y) = n∷ from-∷ r (n∷ y)
from-∷ (nothingʳ r) (x ∷ y) = n∷ (from-∷ r (x ∷ y))
from-∷ (justs r) (x ∷ y) = x ∷ ♯ from' (♭ r) (♭ y)
from-∷ end ()
from : ∀ {a b : CLMA} → a ∼ b → a ≈ b
from eq sem has = from' eq has
refl : ∀ (a : CLMA) → a ≈ a
refl a = λ s z → z
trans : ∀ (a b c : CLMA) → a ≈ b → b ≈ c → a ≈ c
trans a b c ab bc s as = bc s (ab s as)
open import Relation.Nullary
open import Data.Product
data AllNothing : CLMA → Set where
allNothing : ∀ {l} → ∞ (AllNothing (♭ l)) → AllNothing (nothing ∷ l)
[] : AllNothing []
data HasJust : CLMA → Set where
just : ∀ x l → HasJust (just x ∷ l)
nothing : ∀ l → HasJust (♭ l) → HasJust (nothing ∷ l)
import Data.Empty
notSomeMeansAll : ∀ {x} → ¬ HasJust x → AllNothing x
notSomeMeansAll {[]} ns = []
notSomeMeansAll {just x ∷ xs} ns with ns (just x xs)
... | ()
notSomeMeansAll {nothing ∷ xs} ns = allNothing {xs} ( ♯ notSomeMeansAll {♭ xs} (λ z → ns (nothing xs z)) )
data HasBot : CLMA → Set where
⊥ : ∀ l → ∞ (HasBot (♭ l)) → HasBot (nothing ∷ l)
_∷_ : ∀ x l → HasBot (♭ l) → HasBot (x ∷ l)
data IsBot : CLMA → Set where
⊥ : ∀ {l} → ∞ (IsBot (♭ l)) → IsBot (nothing ∷ l)
data IsEmpty : CLMA → Set where
[] : IsEmpty []
n∷_ : ∀ {l} → IsEmpty (♭ l) → IsEmpty (nothing ∷ l)
getAfterJust : {a : CLMA} → HasJust a → A × CLMA
getAfterJust (just x l) = x , ♭ l
getAfterJust (nothing l y) = getAfterJust y
data SemStream : Colist (Maybe A) → Set where
[] : ∀ {l} → IsEmpty l → SemStream l
⊥ : ∀ {l} → IsBot l → SemStream l
_∷_ : ∀ {l} → (hj : HasJust l) → ∞ (SemStream (proj₂ (getAfterJust hj))) → SemStream l
getSem : ∀ {a} → SemStream a → Sem A
go : ∀ {a} → SemStream a → ∞ (Sem A)
go rec = ♯ getSem rec
getSem ([] _) = []
getSem (⊥ _) = ⊥
getSem {a} (hj ∷ rec) = proj₁ (getAfterJust hj) ∷ go (♭ rec)
getSem-empty-good : ∀ {a} → IsEmpty a → a HasSem []
getSem-empty-good [] = []
getSem-empty-good (n∷ y) = n∷ getSem-empty-good y
getSem-good : ∀ {a} (s : SemStream a) → a HasSem getSem s
getSem-good ([] emp) = getSem-empty-good emp
getSem-good (⊥ (⊥ y)) = ⊥ (♯ getSem-good (⊥ (♭ y)))
getSem-good (just x l ∷ y) = x ∷ (♯ getSem-good (♭ y))
getSem-good (nothing l y ∷ y') = n∷ getSem-good (y ∷ y')
allNothing-variants' : ∀ {a} → ¬ IsEmpty a → AllNothing a → IsBot a
allNothing-variants' nie (allNothing y) = ⊥ (♯ allNothing-variants' (λ z → nie (n∷ z)) (♭ y))
allNothing-variants' nie [] with nie []
... | ()
open import Data.Sum
module WithEM (EM : (A : Set) → Dec A) where
allNothing-variants : ∀ {a} → AllNothing a → IsEmpty a ⊎ IsBot a
allNothing-variants {a} an with EM (IsEmpty a)
... | yes ie = inj₁ ie
... | no nie = inj₂ (allNothing-variants' nie an)
mustbe : ∀ (a : CLMA) → SemStream a
mustbe a with EM (HasJust a)
mustbe a | yes p = p ∷ (♯ mustbe _)
mustbe a | no ¬p with notSomeMeansAll ¬p
... | all with allNothing-variants all
... | inj₁ x = [] x
... | inj₂ y = ⊥ y
mustbe' : ∀ (a : CLMA) → ∃ (λ s → a HasSem s)
mustbe' a = getSem (mustbe a) , getSem-good (mustbe a)
data Sem-Eq : Sem A → Sem A → Set where
[] : Sem-Eq [] []
⊥ : Sem-Eq ⊥ ⊥
_∷_ : ∀ x {a b} → ∞ (Sem-Eq (♭ a) (♭ b)) → Sem-Eq (x ∷ a) (x ∷ b)
sem-unique⊥ : ∀ {x b} → x HasSem ⊥ → x HasSem b → Sem-Eq ⊥ b
sem-unique⊥ () []
sem-unique⊥ s⊥ (⊥ y) = ⊥
sem-unique⊥ (⊥ y) (n∷ y') = sem-unique⊥ (♭ y) y'
sem-unique⊥ (n∷ y) (n∷ y') = sem-unique⊥ y y'
sem-unique' : ∀ {x a b} → x HasSem a → x HasSem b → Sem-Eq a b
sem-unique' [] [] = []
sem-unique' (⊥ y) hasb = sem-unique⊥ (⊥ y) hasb
sem-unique' (n∷ y) (⊥ y') = sem-unique' y (♭ y')
sem-unique' (n∷ y) (n∷ y') = sem-unique' y y'
sem-unique' (x ∷ y) (.x ∷ y') = x ∷ (♯ sem-unique' (♭ y) (♭ y'))
to' : ∀ {a b : Colist (Maybe A)} {s} → a HasSem s → b HasSem s → a ∼ b
to' [] [] = end
to' [] (n∷ y) = nothingʳ (to' [] y)
to' (⊥ y) (⊥ y') = nothings (♯ to' (♭ y) (♭ y'))
to' (⊥ y) (n∷ y') = nothings (♯ to' (♭ y) y')
to' (n∷ y) [] = nothingˡ (to' y [])
to' (n∷ y) (⊥ y') = nothings (♯ to' y (♭ y'))
to' (n∷ y) (n∷ y') = nothings (♯ to' y y')
to' (n∷ y) (x ∷ y') = nothingˡ (to' y (x ∷ y'))
to' (x ∷ y) (n∷ y') = nothingʳ (to' (x ∷ y) y')
to' (x ∷ y) (.x ∷ y') = justs (♯ to' (♭ y) (♭ y'))
to : ∀ (a b : Colist (Maybe A)) → a ≈ b → a ∼ b
to a b eq with mustbe' a
... | s , a-s with eq s a-s
... | b-s = to' a-s b-s
hasSem-respects : ∀ {x s1 s2} → x HasSem s1 → Sem-Eq s1 s2 → x HasSem s2
hasSem-respects [] [] = []
hasSem-respects (⊥ y) ⊥ = ⊥ y
hasSem-respects (n∷ y) eq = n∷ hasSem-respects y eq
hasSem-respects (x ∷ y) (.x ∷ y') = x ∷ ♯ hasSem-respects (♭ y) (♭ y')
sym' : ∀ (a b : CLMA) → a ≈ b → b ≈ a
sym' a b eq s b-s with mustbe' a
... | s' , a-s' = hasSem-respects a-s' (sem-unique' (eq s' a-s') b-s)