Cubical Agda中有限多重集右单位元直接证明受阻求解

你的初始证明思路是正确的：基础情况（[]）和构造子情况（y ∷ ys）的处理完全符合归纳证明的逻辑。问题出在comm和trunc构造子对应的路径构造上，下面一步步帮你修正和完成：

1. 修正comm构造子的证明 #

当处理comm x y xs i时，我们需要构造路径：(comm x y xs i) ++ [] ≡ comm x y xs i。

根据++的定义，左边(comm x y xs i) ++ []等价于comm x y (xs ++ []) i。而我们已经通过递归得到了unitr-++ xs : xs ++ [] ≡ xs，只需要把这个路径代入comm x y _ i的第三个参数位置，就能得到左右两边的相等性。

修正后的代码：

unitr-++ (comm x y xs i) = cong (λ z → comm x y z i) (unitr-++ xs)

这里cong (λ z → comm x y z i)的作用是：把xs ++ [] ≡ xs这个路径，映射为comm x y (xs ++ []) i ≡ comm x y xs i，正好是我们需要的目标路径。

2. 完成trunc构造子的证明 #

trunc构造子保证了FMSet A是一个集合（Set），即任意两个元素之间的所有路径都相等（恒等类型是命题）。我们需要利用这个性质来填充2-路径的证明。

首先，根据++的定义，(trunc xs1 xs2 p q i j) ++ []等价于：

trunc (xs1 ++ []) (xs2 ++ []) (cong (_++ []) p) (cong (_++ []) q) i j

我们需要证明这个元素等于trunc xs1 xs2 p q i j。因为FMSet A是集合，任意两个元素的恒等类型是命题，所以我们可以用trunc本身来构造这个2-路径——把xs1 ++ []和xs2 ++ []之间的2-路径，通过unitr-++的递归结果转换为xs1和xs2之间的2-路径。

完成后的代码（需要导入路径相关的语法）：

open import Cubical.Foundations.Path

unitr-++ (trunc xs1 xs2 p q i j) = trunc (xs1 ++ []) (xs2 ++ []) (cong (_++ []) p) (cong (_++ []) q) i j
                                   ≡⟨ trunc _ _ (λ k → unitr-++ (p k)) (λ k → unitr-++ (q k)) i j ⟩
                                   trunc xs1 xs2 p q i j
                                   ∎

这里的核心逻辑是：

• λ k → unitr-++ (p k)表示路径p上每个点的unitr-++证明，连接了xs1 ++ [] ≡ xs1和xs2 ++ [] ≡ xs2
• trunc _ _ ... i j利用集合的性质，把xs1 ++ []与xs2 ++ []之间的2-路径，转换为xs1与xs2之间的2-路径

额外：用标准库的FMSetElimProp简化证明 #

你提到的FMSetElimProp.f是针对命题值性质的消除原理，它可以自动处理trunc构造子的证明（因为命题的恒等类型是Prop，无需手动填充2-路径）。用它简化后的证明如下：

open import Cubical.Data.FMSet.Base
open import Cubical.Foundations.Isomorphism

unitr-++ : ∀ {A : Set} (ys : FMSet A) → ys ++ [] ≡ ys
unitr-++ = FMSetElimProp.f _
  (λ ys → ys ++ [] ≡ ys)  -- 命题族：每个FMSet元素满足ys++[]≡ys
  refl                    -- []的情况
  (λ x xs ih → cong (x ∷_) ih)  -- x∷xs的情况，递归利用ih
  (λ x y xs → isProp→PathP (λ i → trunc _ _ _) (cong (λ z → comm x y z i) ih) refl)
  -- comm构造子的情况：因为目标是命题，两个路径必然相等

内容的提问来源于stack exchange，提问作者Bob