时间戳

首页 > 解决方案 > 如何在前提下进行重写？

agda - 如何在前提下进行重写？

问题描述

Any-comm : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
           Any P (xs ++ ys) → Any P (ys ++ xs)
Any-comm xs [] prf = {!!}

Goal: Any P xs
————————————————————————————————————————————————————————————
prf : Any P (xs ++ [])
xs  : List A
P   : A → Set  (not in scope)
A   : Set  (not in scope)

如何prf在此处使用附加标识重写？我想我可以改写目标以匹配，但是在前提下是否可以这样做？我觉得后面会更整洁。

标签： agda

解决方案

啊，看来我对重写如何工作的假设是错误的。

Any-comm xs [] prf rewrite sym (++-identityʳ xs) = {!!}

Goal: Any P (xs ++ [])
————————————————————————————————————————————————————————————
prf : Any P ((xs ++ []) ++ [])
P   : A → Set  (not in scope)
xs  : List A
A   : Set  (not in scope)

当我尝试上述方法时，我惊讶地发现它重写了目标和前提。因此，从那里重写前提的方式是。

Any-comm xs [] prf rewrite ++-identityʳ xs = prf

我不确定这是否应该如此令人惊讶，但尽管我几乎阅读了 PLFA 书的第 1 卷的全部内容，但我并没有注意到这一点。这种行为与 Coq 的重写不同。

推荐阅读