Как сделать переписать в помещении?

Question

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 с идентификатором добавления здесь? Я полагаю, что вместо этого я мог бы переписать цель матча, но возможно ли сделать то же самое в предпосылке? Я чувствую, что позже будет более аккуратным.

Answer 1

Ах, похоже, мое предположение о том, как работает перезапись, было неверным.

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

Я не уверен, должно ли это быть настолько удивительным, но я не заметил этого, несмотря на то, что почти прошел весь том 1 книги PLFA. Это поведение отличается от переписывания Coq.