From the PLFA I'm trying to prove All-++-≃, that is, that
All-++-≃ : ∀ {A : Set} {P : A → Set} (xs ys : List A) → All P (xs ++ ys) ≃ (All P xs × All P ys)
My problem is with
FromTo : ∀ {A : Set} {P : A → Set} (xs ys : List A) → (u : All P (xs ++ ys)) → from xs ys (to xs ys u) ≡ u
I proved the simple base cases, but I'm having problems with this pattern:
FromTo (x :: xs) ys (u ∷ u´) = ?
The basic problem is that I need to assume that to xs ys u´ has a certain shape
to xs ys u´ = ⟨ Pxs , Pys ⟩
because that allows me to use the definition of
to (x :: xs) ys (u ∷ u´)
and I can go from there. The problem is that I don't know how to write that. Is a syntactical problem if you wish. I tried using a helper function:
helper : ∀ {A : Set} {P : A → Set} (x : A) → (xs ys : List A) → (u : P x) → (u´ : All P (xs ++ ys)) → (All P xs × All P ys) → from (x :: xs) ys (to (x :: xs) ys (u ∷ u´)) ≡ (u ∷ u´)
and then
FromTo (x :: xs) ys (u ∷ u´) = helper x xs ys u u´ (to xs ys u´)
but also I couldn't write the definition of the helper function. So my problem is basically how to write in agda the proof that in paper looks so simple. I just need to write that I assume that to xs ys u´ has some pattern ⟨ Pxs , Pys ⟩ and use that.
I can't really tell what you're asking and I suspect you've identified the wrong problem, but that case is solved by a recursive call:
FromTo (x ∷ xs) ys (u ∷ u′) = cong (u ∷_) (FromTo xs ys u′)
Agda already knows that to (x ∷ xs) ys (u ∷ u′) is of the form ⟨ Pxs , Pys ⟩ in that branch, so the first "layer" computes away and you just need to use the induction hypothesis.