Werner Germán Busch's questions

Estou tentando provar

¬Any≃All¬ : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs

Eu defini

to [] t = []
to (x :: xs) v = (v ∘ here) ∷ to xs (v ∘ there)

from [] [] ()
from (x :: xs´) (¬Px ∷ ¬Pxs´) = λ { (here Px) → ¬Px Px ; (there Pxs´) → (from xs´ ¬Pxs´) Pxs´}

O problema vem da tentativa de definir

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v 

Minha ideia é escrever algo assim:

FromTo [] t = extensionality (λ {()})
FromTo (x :: xs´) v =
  begin
    ((from (x :: xs´)) ∘ (to (x :: xs´))) v 
  ≡⟨⟩
    (from (x :: xs´))(to (x :: xs´) v)
  ≡⟨⟩
    (from (x :: xs´))((v ∘ here) ∷ (to xs´ (v ∘ there)))
  ≡⟨⟩
    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩ -- PARSE ERROR
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨ FromTo xs´ (λ u → v (there u)) ⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (v ∘ there) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → v (there Pxs´) }
  ≡⟨⟩
    v
  ∎

O problema que tenho é que tenho um erro de análise estranho:

 Parse error
≡⟨⟩<ERROR>
        λ { (here Px´) → v (h...

localizado aqui:

    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }

Tentei de tudo para ver se estava faltando algum espaço em branco ou se as tabulações estavam erradas ou o que quer que seja, mas nada. O problema aparece quando há duas lambdas separadas por um ≡⟨⟩.

Eu estava fazendo um exercício de código em Agda do PLFA, para implementar uma prova de que "o reverso de uma lista anexada a outra é o reverso da segunda anexada ao reverso da primeira".

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

Consegui fazer os dois primeiros casos de indução sem problemas:

reverse-++-distrib {A} [] ys

reverse-++-distrib xs []

mas o terceiro passo tem um erro "Falha na verificação de terminação", o que eu acho que significa que o passo indutivo não foi feito corretamente.

reverse-++-distrib {A} (x :: xs) ys =
  begin
    reverse ((x :: xs) ++ ys)
  ≡⟨⟩
    reverse (x :: (xs ++ ys))
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨ cong ((reverse ys) ++_) (cong ((reverse xs) ++_) (sym (reverse-++-fixed-point {A} x))) ⟩
    (reverse ys) ++ (reverse xs ++ (reverse [ x ]))
  **≡⟨ cong ((reverse ys) ++_) (sym (reverse-++-distrib {A} (x :: []) xs)) ⟩**
    (reverse ys) ++ (reverse ([ x ] ++ xs))
  ≡⟨⟩
    (reverse ys) ++ (reverse (x :: ([] ++ xs)))
  ≡⟨ cong ((reverse ys) ++_) (cong reverse (cong (x ::_) (++-identityˡ xs))) ⟩
    (reverse ys) ++ (reverse (x :: xs))
  ∎

A chamada problemática aparentemente é esta:

reverso-++-distribuição {A} (x :: []) xs

Para mim, isso parece bom porque o comprimento do primeiro argumento é 1, que é menor ou igual ao comprimento de x :: xs. E só é igual se xs for a lista vazia, caso em que deve entrar no segundo padrão de correspondência. Então, por que agda está tendo problemas com essa definição?