在Agda中证明All-++-≃时的FromTo模式匹配问题

我们要证明列表拼接与All谓词的等价性：

All-++-≃  : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) ≃ (All P xs × All P ys)

其中等价性的核心是验证from和to互为逆函数，目前卡在FromTo的归纳步骤：

FromTo : ∀ {A : Set} {P : A → Set} (xs ys : List A) → (u : All P (xs ++ ys)) → from xs ys (to xs ys u) ≡ u

具体是FromTo (x :: xs) ys (u ∷ u´)的模式无法推进，核心问题是需要解构to xs ys u´的结果形式。

解决思路 #

不需要额外辅助函数，直接在Agda中通过**with子句或let绑定解构to xs ys u´的结果**，结合归纳假设完成证明。

首先明确to和from的标准实现（对应PLFA中的定义）：

to : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) → All P xs × All P ys
to []       ys u        = ⟨ [] , u ⟩
to (x ∷ xs) ys (u ∷ u´) with to xs ys u´
... | ⟨ pxs , pys ⟩ = ⟨ u ∷ pxs , pys ⟩

from : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P xs × All P ys → All P (xs ++ ys)
from []       ys ⟨ [] , pys ⟩ = pys
from (x ∷ xs) ys ⟨ u ∷ pxs , pys ⟩ = u ∷ from xs ys ⟨ pxs , pys ⟩

完整FromTo证明 #

FromTo : ∀ {A : Set} {P : A → Set} (xs ys : List A) → (u : All P (xs ++ ys)) → from xs ys (to xs ys u) ≡ u
FromTo []       ys u        = refl
FromTo (x ∷ xs) ys (u ∷ u´) with to xs ys u´
... | ⟨ pxs , pys ⟩ = 
  let
    -- 调用归纳假设：from xs ys (to xs ys u´) ≡ u´
    ih = FromTo xs ys u´
  in
    -- 用同余规则将u ∷_应用到归纳假设等式两边
    cong (λ v → u ∷ v) ih

步骤解释 #

1. 基础情况：当xs = []时，to [] ys u的结果是⟨ [] , u ⟩，from直接返回u，因此用refl完成证明。
2. 归纳情况：
   • 用with解构to xs ys u´得到⟨ pxs , pys ⟩，此时to (x::xs) ys (u∷u´)的结果是⟨ u∷pxs , pys ⟩。
   • 展开from的定义，from (x::xs) ys ⟨ u∷pxs , pys ⟩等价于u ∷ from xs ys ⟨ pxs , pys ⟩。
   • 调用归纳假设ih，得到from xs ys ⟨ pxs , pys ⟩ ≡ u´。
   • 最后用cong（同余）规则，将u ∷_映射到等式两边，得到目标结论。

如果偏好更简洁的写法，也可以用let直接解构：

FromTo (x ∷ xs) ys (u ∷ u´) = 
  let
    ⟨ pxs , pys ⟩ = to xs ys u´
    ih = FromTo xs ys u´
  in
    cong (λ v → u ∷ v) ih

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