title: Agda: Equivalence relation for sub-colists
body: <p>I would like to define an equality on <code>CoList (Maybe Nat)</code>s that only takes the <code>just</code>s into account. Of course, I can't just go from <code>CoList (Maybe A)</code> to <code>CoList A</code>, because that wouldn't necessarily be productive.</p>
  
  <p>My question, then, is how could I define such an equivalence relation (with no eye towards decideability)? Does it help, if I can regard infinite <code>just</code> tails as non-equivalent? </p>
  
  <p>@gallais, below, suggests I should be able to naïvely define this relation:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>but proving it's transitive gets into (expected) problems from the termination checker:</p>
  
  <pre><code>  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)))
  </code></pre>
  
  <p>So I tried making the case where both sides are <code>nothing</code> less ambiguous (like how @Vitus suggested):</p>
  
  <pre><code>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))
  </code></pre>
  
  <p>but now I don't know how to define the problematic case of <code>trans</code> (the one where I left a hole)</p>