termination - Agda:子列表的等价关系

Question

我想在 CoList(也许是 Nat) 上定义一个等式，它只考虑 just。当然，我不能只是从 CoList (Maybe A) 转到 CoList A，因为那样不一定有效。

那么，我的问题是如何定义这种等价关系(不考虑可决定性)？如果我可以将无限的 just 尾部视为非等价的，它有帮助吗？

下面的@gallais 建议我应该能够天真地定义这种关系:

open import Data.Colist
open import Data.Maybe
open import Coinduction
open import Relation.Binary

module _ where
  infix 4 _∼_

  data _∼_ {A : Set} : Colist (Maybe A) → Colist (Maybe A) → Set where
    end : [] ∼ []
    nothingˡ : ∀ {xs ys} → ∞ (♭ xs ∼ ys) → nothing ∷ xs ∼ ys
    nothingʳ : ∀ {xs ys} → ∞ (xs ∼ ♭ ys) → xs ∼ nothing ∷ ys
    justs : ∀ {x xs ys} → ∞ (♭ xs ∼ ♭ ys) → just x ∷ xs ∼ just x ∷ ys

但是证明它是可传递的会导致终止检查器出现(预期的)问题:

  refl : ∀ {A} → Reflexive (_∼_ {A})
  refl {A} {[]} = end
  refl {A} {just x ∷ xs} = justs (♯ refl)
  refl {A} {nothing ∷ xs} = nothingˡ (♯ nothingʳ (♯ refl)) -- note how I could have defined this the other way round as well...

  drop-nothingˡ : ∀ {A xs} {ys : Colist (Maybe A)} → nothing ∷ xs ∼ ys → ♭ xs ∼ ys
  drop-nothingˡ (nothingˡ x) = ♭ x
  drop-nothingˡ (nothingʳ x) = nothingʳ (♯ drop-nothingˡ (♭ x))

  trans : ∀ {A} → Transitive (_∼_ {A})
  trans end end = end
  trans end (nothingʳ e2) = nothingʳ e2
  trans (nothingˡ e1) e2 = nothingˡ (♯ trans (♭ e1) e2)
  trans (nothingʳ e1) (nothingˡ e2) = trans (♭ e1) (♭ e2) -- This is where the problem is
  trans (nothingʳ e1) (nothingʳ e2) = nothingʳ (♯ trans (♭ e1) (drop-nothingˡ (♭ e2)))
  trans (justs e1) (nothingʳ e2) = nothingʳ (♯ trans (justs e1) (♭ e2))
  trans (justs e1) (justs e2) = justs (♯ (trans (♭ e1) (♭ e2)))

所以我试着让双方都nothing的情况变得不那么模棱两可(就像@Vitus建议的那样):

module _ where
  infix 4 _∼_

  data _∼_ {A : Set} : Colist (Maybe A) → Colist (Maybe A) → Set where
    end : [] ∼ []
    nothings : ∀ {xs ys} → ∞ (♭ xs ∼ ♭ ys) → nothing ∷ xs ∼ nothing ∷ ys
    nothingˡ : ∀ {xs y ys} → ∞ (♭ xs ∼ just y ∷ ys) → nothing ∷ xs ∼ just y ∷ ys
    nothingʳ : ∀ {x xs ys} → ∞ (just x ∷ xs ∼ ♭ ys) → just x ∷ xs ∼ nothing ∷ ys
    justs : ∀ {x xs ys} → ∞ (♭ xs ∼ ♭ ys) → just x ∷ xs ∼ just x ∷ ys

  refl : ∀ {A} → Reflexive (_∼_ {A})
  refl {A} {[]} = end
  refl {A} {just x ∷ xs} = justs (♯ refl)
  refl {A} {nothing ∷ xs} = nothings (♯ refl)

  sym : ∀ {A} → Symmetric (_∼_ {A})
  sym end = end
  sym (nothings xs∼ys) = nothings (♯ sym (♭ xs∼ys))
  sym (nothingˡ xs∼ys) = nothingʳ (♯ sym (♭ xs∼ys))
  sym (nothingʳ xs∼ys) = nothingˡ (♯ sym (♭ xs∼ys))
  sym (justs xs∼ys) = justs (♯ sym (♭ xs∼ys))

  trans : ∀ {A} → Transitive (_∼_ {A})
  trans end ys∼zs = ys∼zs
  trans (nothings xs∼ys) (nothings ys∼zs) = nothings (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans (nothings xs∼ys) (nothingˡ ys∼zs) = nothingˡ (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans (nothingˡ xs∼ys) (nothingʳ ys∼zs) = nothings (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans (nothingˡ xs∼ys) (justs ys∼zs) = nothingˡ (♯ trans (♭ xs∼ys) (justs ys∼zs))
  trans (nothingʳ xs∼ys) (nothings ys∼zs) = nothingʳ (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans {A} {just x ∷ xs} {nothing ∷ ys} {just z ∷ zs} (nothingʳ xs∼ys) (nothingˡ ys∼zs) = ?
  trans (justs xs∼ys) (nothingʳ ys∼zs) = nothingʳ (♯ trans (justs xs∼ys) (♭ ys∼zs))
  trans (justs xs∼ys) (justs ys∼zs) = justs (♯ trans (♭ xs∼ys) (♭ ys∼zs))

但现在我不知道如何定义有问题的trans情况(我留下一个洞的那个)

Answer 1

在问题的评论部分经过深思熟虑和垃圾邮件(并拖延将我的本地 Agda 更新为具有真正终止检查器的版本)，我想出了这个:

module Subcolist where

open import Data.Colist
open import Data.Maybe
open import Coinduction
open import Relation.Binary

module _ {a} {A : Set a} where
  infix 4 _∼_

  data _∼_ : Colist (Maybe A) → Colist (Maybe A) → Set a 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


  refl : Reflexive _∼_
  refl {[]} = end
  refl {just x ∷ xs} = justs (♯ refl)
  refl {nothing ∷ xs} = nothings (♯ refl)

  sym : Symmetric _∼_
  sym end = end
  sym (nothings xs∼ys) = nothings (♯ sym (♭ xs∼ys))
  sym (nothingˡ xs∼ys) = nothingʳ   (sym   xs∼ys)
  sym (nothingʳ xs∼ys) = nothingˡ   (sym   xs∼ys)
  sym (justs    xs∼ys) = justs    (♯ sym (♭ xs∼ys))

  drop-nothingˡ : ∀ {xs} {ys : Colist (Maybe A)} → nothing ∷ xs ∼ ys → ♭ xs ∼ ys
  drop-nothingˡ (nothings r) = nothingʳ (♭ r)
  drop-nothingˡ (nothingˡ r) = r
  drop-nothingˡ (nothingʳ r) = nothingʳ (drop-nothingˡ r)

  drop-nothingʳ : ∀ {xs : Colist (Maybe A)} {ys} → xs ∼ nothing ∷ ys → xs ∼ ♭ ys
  drop-nothingʳ (nothings r) = nothingˡ (♭ r)
  drop-nothingʳ (nothingˡ r) = nothingˡ (drop-nothingʳ r)
  drop-nothingʳ (nothingʳ r) = r

  drop-nothings : ∀ {xs ys : ∞ (Colist (Maybe A))} → nothing ∷ xs ∼ nothing ∷ ys → ♭ xs ∼ ♭ ys
  drop-nothings (nothings r) = ♭ r
  drop-nothings (nothingˡ r) = drop-nothingʳ r
  drop-nothings (nothingʳ r) = drop-nothingˡ r

  []-trans : ∀ {xs ys : Colist (Maybe A)} → xs ∼ ys → ys ∼ [] → xs ∼ []
  []-trans xs∼ys end = xs∼ys
  []-trans xs∼ys (nothingˡ ys∼[]) = []-trans (drop-nothingʳ xs∼ys) ys∼[]

  mutual    
    just-trans : ∀ {xs ys zs} {z : A} → xs ∼ ys → ys ∼ just z ∷ zs → xs ∼ just z ∷ zs
    just-trans (justs r) (justs r₁) = justs (♯ (trans (♭ r) (♭ r₁)))
    just-trans (nothingˡ xs∼ys) ys∼zs = nothingˡ (just-trans xs∼ys ys∼zs)
    just-trans xs∼ys (nothingˡ ys∼zs) = just-trans (drop-nothingʳ xs∼ys) ys∼zs

    nothing-trans : ∀ {xs ys : Colist (Maybe A)} {zs} → xs ∼ ys → ys ∼ nothing ∷ zs → xs ∼ nothing ∷ zs
    nothing-trans (nothings xs∼ys) ys∼zs = nothings (♯ trans (♭ xs∼ys) (drop-nothings ys∼zs))
    nothing-trans (nothingˡ xs∼ys) ys∼zs = nothings (♯ (trans xs∼ys (drop-nothingʳ ys∼zs)))
    nothing-trans (nothingʳ xs∼ys) ys∼zs = nothing-trans xs∼ys (drop-nothingˡ ys∼zs)
    nothing-trans {xs = just x  ∷ xs} xs∼ys (nothingʳ ys∼zs) = nothingʳ (trans xs∼ys ys∼zs)
    nothing-trans end xs∼ys = xs∼ys

    trans : Transitive _∼_
    trans {k = []}           xs∼ys ys∼zs = []-trans      xs∼ys ys∼zs
    trans {k = nothing ∷ ks} xs∼ys ys∼zs = nothing-trans xs∼ys ys∼zs
    trans {k = just k  ∷ ks} xs∼ys ys∼zs = just-trans    xs∼ys ys∼zs

  equivalence : Setoid a a
  equivalence = record 
    { _≈_ = _∼_
    ; isEquivalence = record 
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
    }

我使用混合归纳-共同归纳，我相信它捕获了你想要的概念。我需要跳过一些障碍才能通过终止/生产力检查器，因为 trans 的原始版本没有通过它，但这似乎有效。它的部分灵感来自于我从 Nils Anders Danielsson 的偏性 monad 实现中学到的东西，其中有类似的关系定义。它没有这一个那么复杂，但是让 Agda 接受它的工作在很大程度上是相似的。稍微概括一下，将其视为一个 setoid 转换器似乎更友好，而不仅仅是假设 justs 情况的定义/命题相等，但这是一个微不足道的变化。

我确实注意到其他两个提案禁止 nothing ∷ nothing ∷ [] ∼ [] 这似乎与原始问题相反，所以我编辑了类型以再次支持它。我认为这样做会阻止 _∼_ 成为唯一的居住地，但解决这个问题可能会导致关系类型中出现更多的构造函数，而这比看起来值得付出更多的努力。

值得注意的是，在我撰写本文时，Agda 在其终止检查器中有一个适用于我的版本的开放错误 (#787)。我不确定是什么导致了这个错误，所以我不能保证我的版本是完全正确的，但它对我来说很有意义。