验证列表L ++ []≡L

如何填充下一个孔？

$ 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，但在这一刻，我没有看到它。

来源

2017-04-22 jonaprieto

你应该做的是对的隐含参数{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

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

来源

2017-04-23 11:59:42 Cactus

这已经足够了，谢谢，重写是新鲜事。 – jonaprieto

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

在这种情况下为p0很容易通过的_++_第二种情况下看到[ x ] == x :: []由定义的[_]，然后通过(x :: []) ++ [] == x :: ([] ++ [])1箱子_++_，和[] ++ [] == []。

案例p1已经需要通过归纳推理，并且由于最终您将需要通过归纳证明，无论如何，您自己都无法证明p1。

壳体p具有List构造，_::_[]和，以及从_++_箱子一个非平凡应用一个未知的嵌套。

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

来源

2017-04-23 07:24:12

验证列表L ++ []≡L

回答

相关问题