在证明身份时使用论证具有一定的模式

Question

从PLFA我试图证明All-++-≃，也就是说，

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

我的问题是

  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´ 具有一定的形状

to xs ys u´ = ⟨ Pxs , Pys ⟩

因为这让我可以使用

的定义

to (x :: xs) ys (u ∷ u´)

我可以从那里开始。问题是我不知道怎么写。如果你愿意的话，这是一个语法问题。我尝试使用辅助函数：

  helper : ∀ {A : Set} {P : A → Set} (x : A) → (xs ys : List A) → (u : P x) → (u´ : All P (xs ++ ys)) → (All P xs × All P ys) → from (x :: xs) ys (to (x :: xs) ys (u ∷ u´)) ≡ (u ∷ u´)

然后

  FromTo (x :: xs) ys (u ∷ u´) = helper x xs ys u u´ (to xs ys u´)

但我也无法编写辅助函数的定义。所以我的问题基本上是如何在 agda 中编写纸上看起来如此简单的证明。我只需要写下我假设 xs ys u´ 有某种模式 ⟨ Pxs ， Pys ⟩ 并使用它。

Answer 1

我真的无法告诉你你在问什么，我怀疑你发现了错误的问题，但这种情况是通过递归调用解决的：

  FromTo (x ∷ xs) ys (u ∷ u′) = cong (u ∷_) (FromTo xs ys u′)

Agda 已经知道

to (x ∷ xs) ys (u ∷ u′)

在该分支中具有

⟨ Pxs , Pys ⟩

的形式，因此第一个“层”计算完毕，您只需要使用归纳假设即可。

Answer 2

我能弄清楚的是这个。

第一次尝试会是这样的。假设“xs ys u´ = ⟨ Pxs , Pys ⟩”

  helper : ∀ {A : Set} {P : A → Set} (x : A) → (xs ys : List A) → (u : P x) → (u´ : All P (xs ++ ys)) → (from xs ys (to xs ys u´) ≡ u´) → from (x :: xs) ys (to (x :: xs) ys (u ∷ u´)) ≡ (u ∷ u´)
  helper x xs ys u u´ q =
    begin
          from (x :: xs) ys (to (x :: xs) ys (u ∷ u´))
        ≡⟨⟩
          from (x :: xs) ys (⟨ u ∷ Pxs , Pys ⟩)
        ≡⟨⟩
          u ∷ from xs ys (⟨ Pxs , Pys ⟩)
        ≡⟨⟩
          u ∷ from xs ys (to xs ys u´)
        ≡⟨ cong (u ∷_) q ⟩
          u ∷ u´
    ∎

  FromTo (x :: xs) ys (u ∷ u´) = helper x xs ys u u´ (FromTo xs ys u´)

问题当然是变量Pxs和Pys不存在。但由于我们在中间的“≡⟨⟩”步骤中没有使用任何假设，因此我们可以删除这些步骤：

  helper : ∀ {A : Set} {P : A → Set} (x : A) → (xs ys : List A) → (u : P x) → (u´ : All P (xs ++ ys)) → (from xs ys (to xs ys u´) ≡ u´) → from (x :: xs) ys (to (x :: xs) ys (u ∷ u´)) ≡ (u ∷ u´)
  helper x xs ys u u´ q =
    begin
          from (x :: xs) ys (to (x :: xs) ys (u ∷ u´))
        ≡⟨ cong (u ∷_) q ⟩
          u ∷ u´
    ∎

这有效。这个证明就是 cong (u ∷_) (FromTo xs ys u´)。 @Naïm Favier 这就是我得出这个结论的方式，简单地写“cong (u ∷_) (FromTo xs ys u′)”对我来说有点太间接了:)。