证明列表 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

在洞里为什么不起作用 refl？ 它是由第一个参数上的 ∷ 的结构递归引起的吗？

我认为做一些递归我可以证明 p 查看 p0 和 p1，但此刻，我看不到它。

Answer 1

你需要看看_++_是如何定义的。使用这里的定义：http://www.cse.chalmers.se/~nad/repos/lib/src/Data/List.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

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