agda

Agda: Parse error when proving that ¬Any≃All¬

Im trying to prove

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

I have defined

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´}

The problem comes from trying to define

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

My idea is to write something like this:

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
  ∎

The problem I have is that I have a weird parse error:

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

located here:

    λ { (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´ }

I tried everything to see if I was missing some white space or the tabs were wrong or what have, but nothing. The problem appears when having two lambdas separated by a ≡⟨⟩.

Solution

  • Wrap the lambdas in parentheses:

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