基于PLFA证明¬Any≃All¬时FromTo空列表基例报错问题

我正在遵循PLFA的内容尝试证明以下定理：

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

当前在实现FromTo函数时遇到问题，函数定义如下：

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

当处理xs ≡ []的基例时，我认为¬ Any P []是不可居的，于是尝试用FromTo [] ()编写基例，但收到Agda报错：

(¬_ ∘ Any P) [] should be empty, but that's not obvious to me
when checking the clause left hand side
FromTo [] ()

解决方法 #

问题在于Agda无法自动推导¬ Any P []是空类型，需要你显式证明这一点，或者让Agda直接看到Any P []没有构造子。

方法1：添加辅助引理

先定义一个引理证明¬ Any P []不可居：

¬AnyNil : ∀ {A : Set} {P : A → Set} → ¬ Any P []
¬AnyNil ()

然后在FromTo的基例中使用这个引理：

FromTo [] v = ⊥-elim (¬AnyNil v)

方法2：直接展开应用

也可以直接在基例里将v应用到空构造子，让Agda明确识别空类型：

FromTo [] v = v ()

这两种方式都能让Agda确认xs ≡ []时(¬_ ∘ Any P) xs没有居民，从而通过类型检查。

内容的提问来源于stack exchange，提问作者Werner Germán Busch