Werner Germán Busch's questions

我想证明

¬Any≃All¬ : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs

我已经定义

to [] t = []
to (x :: xs) v = (v ∘ here) ∷ to xs (v ∘ there)

from [] [] ()
from (x :: xs´) (¬Px ∷ ¬Pxs´) = λ { (here Px) → ¬Px Px ; (there Pxs´) → (from xs´ ¬Pxs´) Pxs´}

问题来自于试图定义

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v 

我的想法是写类似这样的内容：

FromTo [] t = extensionality (λ {()})
FromTo (x :: xs´) v =
  begin
    ((from (x :: xs´)) ∘ (to (x :: xs´))) v 
  ≡⟨⟩
    (from (x :: xs´))(to (x :: xs´) v)
  ≡⟨⟩
    (from (x :: xs´))((v ∘ here) ∷ (to xs´ (v ∘ there)))
  ≡⟨⟩
    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩ -- PARSE ERROR
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨ FromTo xs´ (λ u → v (there u)) ⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (v ∘ there) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → v (there Pxs´) }
  ≡⟨⟩
    v
  ∎

我遇到的问题是我有一个奇怪的解析错误：

 Parse error
≡⟨⟩<ERROR>
        λ { (here Px´) → v (h...

位于此处：

    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }

我尝试了各种方法，想看看是不是缺少了空格，制表符是否错误，还是其他什么原因，但都无济于事。当两个 lambda 被 ≡⟨⟩ 分隔时，就会出现问题。

我正在用 PLFA 在 Agda 中做一个代码练习，以实现“一个列表的反转附加到另一个列表上，就是第二个列表的反转附加到第一个列表的反转上”的证明。

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

我能够毫无问题地完成前两种归纳情况：

reverse-++-distrib {A} [] ys

reverse-++-distrib xs []

但是第三步出现“终止检查失败”错误，我猜这意味着归纳步骤没有正确完成。

reverse-++-distrib {A} (x :: xs) ys =
  begin
    reverse ((x :: xs) ++ ys)
  ≡⟨⟩
    reverse (x :: (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨ cong ((reverse ys) ++_) (cong ((reverse xs) ++_) (sym (reverse-++-fixed-point {A} x))) ⟩
    (reverse ys) ++ (reverse xs ++ (reverse [ x ]))
  **≡⟨ cong ((reverse ys) ++_) (sym (reverse-++-distrib {A} (x :: []) xs)) ⟩**
    (reverse ys) ++ (reverse ([ x ] ++ xs))
  ≡⟨⟩
    (reverse ys) ++ (reverse (x :: ([] ++ xs)))
  ≡⟨ cong ((reverse ys) ++_) (cong reverse (cong (x ::_) (++-identityˡ xs))) ⟩
    (reverse ys) ++ (reverse (x :: xs))
  ∎

有问题的调用显然是这样的：

反向-++-分布 {A} (x :: []) xs

对我来说这看起来不错，因为第一个参数的长度是 1，小于或等于 x :: xs 的长度。并且只有当 xs 是空列表时才相等，在这种情况下它应该进入第二个模式匹配。那么为什么 agda 对此定义有问题呢？