证明列表 L ++ [] ≡ L 的命题

Question

使用 agda 标准库 (v13)

我怎样才能填补下一个洞？

$ cat foo.aga
open import Data.List using
  ( List ; [] ; _∷_ ; _++_ ; [_] )
open import Relation.Binary.PropositionalEquality
  using ( _≡_; refl; cong; trans; sym)

p : ∀ {A : Set} {L : List A} → L ++ [] ≡ L
p = {!!}

婴儿步骤：

p0 : (x : Prop) → ([ x ]) ++ [] ≡ [ x ]
p0 = λ x → refl

p1 : (x y : Prop) → (x ∷ y ∷ []) ++ [] ≡ x ∷ y ∷ []
p1 = λ x y → refl

在洞里为什么反射镜不起作用？是由于第一个参数上∷的结构递归吗？

我认为做一些递归我可以通过查看 p0 和 p1 来证明 p，但目前我还没有看到它。

Answer 1

您需要查看 _++_ 是如何定义的。使用此处的定义：http://www.cse.chalmers.se/~nad/repos/lib/src/Data/List.agda Agda 能够得出结论 refl 适用于 p0.

在 p0 的情况下很容易看出 [ x ] == x :: [] 根据 [_] 的定义，然后 (x :: []) ++ [] == x :: ([] ++ []) 根据 _++_ 的定义， [] ++ [] == [] _++_.

的第二种情况

案例 p1 已经需要归纳推理，并且由于最终您无论如何都需要归纳证明，因此单独证明 p1 不会有任何收获。

案例 p 具有未知的 List 构造函数嵌套，_::_ 和 []，以及来自 _++_ 的案例的重要应用.

为了通过归纳法构造此问题的证明，您需要了解如何应用 cong 从关于较短列表的陈述中证明关于较长列表的陈述。

Answer 2

你应该做的是对隐式参数 {L} 进行模式匹配，这样你就可以为空列表和缺点列表逐个定义 p：

p : ∀ {A : Set} {L : List A} → L ++ [] ≡ L
p {L = []} = ?
p {L = x ∷ L} = ?

第一个洞的类型是

Goal: [] ≡ []

你应该能够很容易地证明这一点。

第二个洞的类型是

Goal: x ∷ L ++ [] ≡ x ∷ L

通过在现在更小的 L 上递归调用 p，我们可以重写该目标（因为 p {L = L} 证明了 L ++ [] ≡ L，我们可以替换 L ++ [] 在左侧只有 L):

p : ∀ {A : Set} {L : List A} → L ++ [] ≡ L
p {L = []} = ?
p {L = x ∷ L} rewrite p {L = L} = ?

给予

Goal: x ∷ L ≡ x ∷ L

如果您需要任何进一步的帮助，请在评论中告诉我。

证明列表 L ++ [] ≡ L 的命题

Proving a proposition of list L ++ [] ≡ L

agda