open import Data.Bool using (T; not)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List hiding (downFrom; reverse; product; foldl; merge)
import Data.List.Properties as List
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Nat as ℕ using (ℕ; zero; suc; _+_; _*_; _∸_)
import Data.Nat.Properties as ℕ
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (∃-syntax; _×_; _,_; Σ; proj₁; proj₂)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function using (_∘_)
open ≡-Reasoning
-- Context ---------------------------------------------------------------------
reverse : ∀ {A : Set} → List A → List A
reverse [] = []
reverse (x ∷ xs) = reverse xs ++ [ x ]
record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where
field
assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z)
identityˡ : ∀ (x : A) → e ⊗ x ≡ x
identityʳ : ∀ (x : A) → x ⊗ e ≡ x
open IsMonoid
infix 0 _⇔_
record _⇔_ (A B : Set) : Set where
field
to : A → B
from : B → A
open _⇔_
infix 0 _≃_
record _≃_ (A B : Set) : Set where
field
to : A → B
from : B → A
from∘to : ∀ (x : A) → from (to x) ≡ x
to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_
-- Exercise reverse-++-distrib (recommended) -----------------------------------
-- Show that the reverse of one list appended to another is the reverse of the
-- second appended to the reverse of the first:
xs++[]≡xs : ∀ {A : Set} (xs : List A) →
xs ++ [] ≡ xs
xs++[]≡xs [] = refl
xs++[]≡xs (x ∷ xs) rewrite xs++[]≡xs xs = refl
reverse-++-distrib : ∀ {A : Set} (xs ys : List A) →
reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-distrib [] ys =
reverse ([] ++ ys) ≡⟨ refl ⟩
reverse ys ≡⟨ sym (xs++[]≡xs (reverse ys)) ⟩
reverse ys ++ [] ≡⟨ refl ⟩
reverse ys ++ reverse [] ∎
reverse-++-distrib (x ∷ xs) ys =
reverse (x ∷ xs ++ ys) ≡⟨ refl ⟩
reverse (xs ++ ys) ++ [ x ] ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
(reverse ys ++ reverse xs) ++ [ x ] ≡⟨ List.++-assoc (reverse ys) (reverse xs) ([ x ]) ⟩
reverse ys ++ (reverse xs ++ [ x ]) ≡⟨ refl ⟩
reverse ys ++ reverse (x ∷ xs) ∎
-- Exercise reverse-involutive (recommended) -----------------------------------
-- A function is an involution if when applied twice it acts as the identity
-- function. Show that reverse is an involution:
reverse-involutive : ∀ {A : Set} (xs : List A) →
reverse (reverse xs) ≡ xs
reverse-involutive [] =
reverse (reverse []) ≡⟨ refl ⟩
[] ∎
reverse-involutive (x ∷ xs) =
reverse (reverse (x ∷ xs)) ≡⟨ refl ⟩
reverse (reverse xs ++ [ x ]) ≡⟨ reverse-++-distrib (reverse xs) ([ x ]) ⟩
reverse ([ x ]) ++ reverse (reverse xs) ≡⟨ refl ⟩
x ∷ reverse (reverse xs) ≡⟨ cong (x ∷_) (reverse-involutive xs) ⟩
x ∷ xs ∎
-- Exercise map-compose (practice) ---------------------------------------------
-- Prove that the map of a composition is equal to the composition of two maps:
-- map (g ∘ f) ≡ map g ∘ map f
-- The last step of the proof requires extensionality.
postulate
fun-ext : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x} → (∀ a → f a ≡ g a) → f ≡ g
map-dist-∘' : ∀ {A B C : Set} (f : A → B) (g : B → C) (xs : List A) → map (g ∘ f) xs ≡ (map g ∘ map f) xs
map-dist-∘' f g [] =
map (g ∘ f) [] ≡⟨ refl ⟩
[] ≡⟨ refl ⟩
(map g ∘ map f) [] ∎
map-dist-∘' f g (x ∷ xs) =
map (g ∘ f) (x ∷ xs) ≡⟨ refl ⟩
(g ∘ f) x ∷ map (g ∘ f) xs ≡⟨ cong ((g ∘ f) x ∷_) (map-dist-∘' f g xs) ⟩
(g ∘ f) x ∷ (map g ∘ map f) xs ≡⟨ refl ⟩
(map g ∘ map f) (x ∷ xs) ∎
map-dist-∘ : ∀ {A B C : Set} (f : A → B) (g : B → C) → map (g ∘ f) ≡ map g ∘ map f
map-dist-∘ f g = fun-ext (map-dist-∘' f g)
-- Exercise map-++-distribute (practice) ---------------------------------------
-- Prove the following relationship between map and append:
map-dist-++ : ∀ {A B : Set} (f : A → B) (xs ys : List A) →
map f (xs ++ ys) ≡ map f xs ++ map f ys
map-dist-++ f [] ys = refl
map-dist-++ f (x ∷ xs) ys rewrite map-dist-++ f xs ys = refl
-- Exercise map-Tree (practice) ------------------------------------------------
-- Define a type of trees with leaves of type A and internal nodes of type B:
data Tree (A B : Set) : Set where
leaf : A → Tree A B
node : Tree A B → B → Tree A B → Tree A B
-- Define a suitable map operator over trees:
map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
map-Tree f g (leaf a) = leaf (f a)
map-Tree f g (node t₁ b t₂) = node (map-Tree f g t₁) (g b) (map-Tree f g t₂)
-- Exercise product (recommended) ----------------------------------------------
-- Use fold to define a function to find the product of a list of numbers.
-- For example:
-- product [ 1 , 2 , 3 , 4 ] ≡ 24
product : List ℕ → ℕ
product = foldr _*_ 1
_ : product (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡ 24
_ = refl
-- Exercise foldr-++ (recommended) ---------------------------------------------
-- Show that fold and append are related as follows:
-- foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
foldr-++ _⊗_ e [] ys =
foldr _⊗_ e ([] ++ ys) ≡⟨ refl ⟩
foldr _⊗_ e ys ≡⟨ refl ⟩
foldr _⊗_ (foldr _⊗_ e ys) [] ∎
foldr-++ _⊗_ e (x ∷ xs) ys =
foldr _⊗_ e (x ∷ xs ++ ys) ≡⟨ refl ⟩
x ⊗ foldr _⊗_ e (xs ++ ys) ≡⟨ cong (x ⊗_) (foldr-++ _⊗_ e xs ys) ⟩
x ⊗ foldr _⊗_ (foldr _⊗_ e ys) (xs) ≡⟨ refl ⟩
foldr _⊗_ (foldr _⊗_ e ys) (x ∷ xs) ∎
-- Exercise foldr-∷ (practice) -------------------------------------------------
-- Show
-- foldr _∷_ [] xs ≡ xs
-- Show as a consequence of foldr-++ above that
-- xs ++ ys ≡ foldr _∷_ ys xs
foldr-∷ : ∀ {A : Set} (xs : List A) → foldr _∷_ [] xs ≡ xs
foldr-∷ [] = refl
foldr-∷ (x ∷ xs) rewrite foldr-∷ xs = refl
foldr-++-∷ : ∀ {A : Set} (xs ys : List A) → xs ++ ys ≡ foldr _∷_ ys xs
foldr-++-∷ xs ys =
xs ++ ys ≡⟨ sym (foldr-∷ (xs ++ ys)) ⟩
foldr _∷_ [] (xs ++ ys) ≡⟨ foldr-++ _∷_ [] xs ys ⟩
foldr _∷_ (foldr _∷_ [] ys) xs ≡⟨ cong (λ Z → foldr _∷_ Z xs) (foldr-∷ ys) ⟩
foldr _∷_ ys xs ∎
-- Exercise map-is-foldr (practice) --------------------------------------------
-- Show that map can be defined using fold:
-- map f ≡ foldr (λ x xs → f x ∷ xs) []
-- The proof requires extensionality.
map-is-foldr' : ∀ {A B : Set} (f : A → B) (ys : List A) →
map f ys ≡ foldr (λ x xs → f x ∷ xs) [] ys
map-is-foldr' f [] = refl
map-is-foldr' f (y ∷ ys) rewrite map-is-foldr' f ys = refl
map-is-foldr : ∀ {A B : Set} (f : A → B) →
map f ≡ foldr (λ x xs → f x ∷ xs) []
map-is-foldr f = fun-ext (map-is-foldr' f)
-- Exercise fold-Tree (practice) -----------------------------------------------
-- Define a suitable fold function for the type of trees given earlier:
fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
fold-Tree f g (leaf a) = f a
fold-Tree f g (node t₁ b t₂) = g (fold-Tree f g t₁) b (fold-Tree f g t₂)
-- Exercise map-is-fold-Tree (practice) ----------------------------------------
-- Demonstrate an analogue of map-is-foldr for the type of trees.
map-Tree-is-fold-Tree' : ∀ {A B C D : Set} (f : A → C) (g : B → D) (t : Tree A B) →
map-Tree f g t ≡ fold-Tree (λ a → leaf (f a)) (λ t₁ b t₂ → node t₁ (g b) t₂) t
map-Tree-is-fold-Tree' f g (leaf a) = refl
map-Tree-is-fold-Tree' f g (node t₁ b t₂)
rewrite map-Tree-is-fold-Tree' f g t₁
| map-Tree-is-fold-Tree' f g t₂ = refl
map-Tree-is-fold-Tree : ∀ {A B C D : Set} (f : A → C) (g : B → D) →
map-Tree f g ≡ fold-Tree (λ a → leaf (f a)) (λ t₁ b t₂ → node t₁ (g b) t₂)
map-Tree-is-fold-Tree f g = fun-ext (map-Tree-is-fold-Tree' f g)
-- Exercise sum-downFrom (stretch) ---------------------------------------------
-- Define a function that counts down as follows:
downFrom : ℕ → List ℕ
downFrom zero = []
downFrom (suc n) = n ∷ downFrom n
-- For example:
_ : downFrom 3 ≡ 2 ∷ 1 ∷ 0 ∷ []
_ = refl
-- Prove that the sum of the numbers (n - 1) + ⋯ + 0 is equal to n * (n ∸ 1) / 2:
lemma : ∀ n →
suc (n ∸ 1) * n ≡ n * n
lemma zero = refl
lemma (suc n) = refl
sum-downFrom : ∀ n →
sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom zero =
sum (downFrom 0) * 2 ≡⟨ refl ⟩
0 ≡⟨ refl ⟩
0 * (0 ∸ 1) ∎
sum-downFrom (suc n) =
sum (downFrom (suc n)) * 2 ≡⟨ refl ⟩
(n + sum (downFrom n)) * 2 ≡⟨ ℕ.*-distribʳ-+ 2 n (sum (downFrom n)) ⟩
n * 2 + sum (downFrom n) * 2 ≡⟨ cong (n * 2 +_) (sum-downFrom n) ⟩
n * 2 + n * (n ∸ 1) ≡⟨ cong (_+ n * (n ∸ 1)) (ℕ.*-comm n 2) ⟩
(n + (n + 0)) + n * (n ∸ 1) ≡⟨ cong (_+ n * (n ∸ 1)) (cong (n +_) (ℕ.+-identityʳ n)) ⟩
(n + n) + n * (n ∸ 1) ≡⟨ ℕ.+-assoc n n (n * (n ∸ 1)) ⟩
n + (n + n * (n ∸ 1)) ≡⟨ cong (n +_) (cong (n +_) (ℕ.*-comm n (n ∸ 1))) ⟩
n + (n + (n ∸ 1) * n) ≡⟨ refl ⟩
n + (suc (n ∸ 1) * n) ≡⟨ cong (n +_) (lemma n) ⟩
n + n * n ≡⟨ refl ⟩
suc n * (suc n ∸ 1) ∎
-- Exercise foldl (practice) ---------------------------------------------------
-- Define a function foldl which is analogous to foldr, but where operations
-- associate to the left rather than the right. For example:
-- foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
-- foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
foldl : ∀ {A B : Set} → (A → B → A) → A → List B → A
foldl c n [] = n
foldl c n (x ∷ xs) = foldl c (c n x) xs
-- As a comparison, here is the definition of `foldr` again:
foldr' : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr' c n [] = n
foldr' c n (x ∷ xs) = c x (foldr' c n xs)
-- Exercise foldr-monoid-foldl (practice) --------------------------------------
-- Show that if _⊗_ and e form a monoid, then foldr _⊗_ e and foldl _⊗_ e always
-- compute the same result.
foldl-⊗ :
∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
∀ (xs : List A) (x : A) →
x ⊗ foldl _⊗_ e xs ≡ foldl _⊗_ (e ⊗ x) xs
foldl-⊗ _⊗_ e [⊗,e]-monoid [] x =
x ⊗ foldl _⊗_ e [] ≡⟨ refl ⟩
x ⊗ e ≡⟨ identityʳ [⊗,e]-monoid x ⟩
x ≡⟨ sym (identityˡ [⊗,e]-monoid x) ⟩
e ⊗ x ≡⟨ refl ⟩
foldl _⊗_ (e ⊗ x) [] ∎
foldl-⊗ _⊗_ e [⊗,e]-monoid (x' ∷ xs) x =
x ⊗ foldl _⊗_ e (x' ∷ xs) ≡⟨ refl ⟩
x ⊗ foldl _⊗_ (e ⊗ x') xs ≡⟨ cong (x ⊗_) (sym (foldl-⊗ _⊗_ e [⊗,e]-monoid xs x')) ⟩
x ⊗ (x' ⊗ foldl _⊗_ e xs) ≡⟨ sym (assoc [⊗,e]-monoid x x' (foldl _⊗_ e xs)) ⟩
(x ⊗ x') ⊗ foldl _⊗_ e xs ≡⟨ foldl-⊗ _⊗_ e [⊗,e]-monoid xs (x ⊗ x') ⟩
foldl _⊗_ (e ⊗ (x ⊗ x')) xs ≡⟨ cong (λ X → foldl _⊗_ X xs) (sym (assoc [⊗,e]-monoid e x x')) ⟩
foldl _⊗_ ((e ⊗ x) ⊗ x') xs ≡⟨ refl ⟩
foldl _⊗_ (e ⊗ x) (x' ∷ xs) ∎
foldr-monoid-foldl :
∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
∀ (xs : List A) →
foldr _⊗_ e xs ≡ foldl _⊗_ e xs
foldr-monoid-foldl _⊗_ e [⊗,e]-monoid [] =
foldr _⊗_ e [] ≡⟨ refl ⟩
e ≡⟨ refl ⟩
foldl _⊗_ e [] ∎
foldr-monoid-foldl _⊗_ e [⊗,e]-monoid (x ∷ xs) =
foldr _⊗_ e (x ∷ xs) ≡⟨ refl ⟩
x ⊗ foldr _⊗_ e xs ≡⟨ cong (x ⊗_) (foldr-monoid-foldl _⊗_ e [⊗,e]-monoid xs) ⟩
x ⊗ foldl _⊗_ e xs ≡⟨ foldl-⊗ _⊗_ e [⊗,e]-monoid xs x ⟩
foldl _⊗_ (e ⊗ x) xs ≡⟨ refl ⟩
foldl _⊗_ e (x ∷ xs) ∎
-- Exercise Any-++-⇔ (recommended) ---------------------------------------------
-- Prove a result similar to All-++-⇔, but with Any in place of All, and a
-- suitable replacement for _×_.
Any-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
Any P (xs ++ ys) ⇔ (Any P xs ⊎ Any P ys)
Any-++-⇔ xs ys =
record
{ to = to' xs ys
; from = from' xs ys
}
where
to' : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
Any P (xs ++ ys) → (Any P xs ⊎ Any P ys)
to' [] ys any-P-ys = inj₂ any-P-ys
to' (x ∷ xs) ys (here px) = inj₁ (here px)
to' (x ∷ xs) ys (there any-P-xs++ys) with to' xs ys any-P-xs++ys
... | inj₁ any-P-xs = inj₁ (there any-P-xs)
... | inj₂ any-P-ys = inj₂ any-P-ys
from' : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
Any P xs ⊎ Any P ys → Any P (xs ++ ys)
from' [] ys (inj₂ any-P-ys) = any-P-ys
from' (x ∷ xs) ys (inj₁ (here px)) = here px
from' (x ∷ xs) ys (inj₁ (there any-P-x∷xs)) = there (from' xs ys (inj₁ any-P-x∷xs))
from' (x ∷ xs) ys (inj₂ any-P-ys) = there (from' xs ys (inj₂ any-P-ys))
-- For comparison, here's the definition of `All-++-⇔`:
All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
All P (xs ++ ys) ⇔ (All P xs × All P ys)
All-++-⇔ xs ys =
record
{ to = to' xs ys
; from = from' xs ys
}
where
to' : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
All P (xs ++ ys) → (All P xs × All P ys)
to' [] ys Pys = ([] , Pys)
to' (x ∷ xs) ys (Px ∷ Pxs++ys) = let (Pxs , Pys) = to' xs ys Pxs++ys in
(Px ∷ Pxs , Pys)
from' : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
All P xs × All P ys → All P (xs ++ ys)
from' [] ys ([] , Pys) = Pys
from' (x ∷ xs) ys (Px ∷ Pxs , Pys) = Px ∷ from' xs ys (Pxs , Pys)
-- As a consequence, demonstrate an equivalence relating _∈_ and _++_.
∈-++-⇔ : ∀ {A : Set} (xs ys : List A) (x : A) →
x ∈ (xs ++ ys) ⇔ (x ∈ xs ⊎ x ∈ ys)
∈-++-⇔ xs ys x = Any-++-⇔ {P = λ y → x ≡ y} xs ys
-- Exercise All-++-≃ (stretch) -------------------------------------------------
-- Show that the equivalence All-++-⇔ can be extended to an isomorphism.
All-++-≃ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
All P (xs ++ ys) ≃ (All P xs × All P ys)
All-++-≃ xs ys =
record
{ to = to' xs ys
; from = from' xs ys
; from∘to = from∘to' xs ys
; to∘from = to∘from' xs ys
}
where
to' : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
All P (xs ++ ys) → (All P xs × All P ys)
to' [] ys Pys = ([] , Pys)
to' (x ∷ xs) ys (Px ∷ Pxs++ys) = let (Pxs , Pys) = to' xs ys Pxs++ys in
(Px ∷ Pxs , Pys)
from' : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
All P xs × All P ys → All P (xs ++ ys)
from' [] ys ([] , Pys) = Pys
from' (x ∷ xs) ys (Px ∷ Pxs , Pys) = Px ∷ from' xs ys (Pxs , Pys)
from∘to' : ∀ {A : Set} {P : A → Set} (xs ys : List A) (x : All P (xs ++ ys)) →
from' xs ys (to' xs ys x) ≡ x
from∘to' [] ys [] = refl
from∘to' [] ys (px ∷ p) = refl
from∘to' (x ∷ xs) ys (Px ∷ Pxs++ys) rewrite from∘to' xs ys Pxs++ys = refl
to∘from' : ∀ {A : Set} {P : A → Set} (xs ys : List A) (x : All P xs × All P ys) →
to' xs ys (from' xs ys x) ≡ x
to∘from' [] ys ([] , Pys) = refl
to∘from' (x ∷ xs) ys (Px ∷ Pxs , Pys) rewrite to∘from' xs ys (Pxs , Pys) = refl
-- Exercise ¬Any⇔All¬ (recommended) --------------------------------------------
-- > Show that Any and All satisfy a version of De Morgan’s Law:
-- >
-- > (¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs
lookup-Any-All : ∀ {A : Set} {P Q : A → Set} {xs : List A} →
Any P xs → All Q xs → ∃[ x ] (P x × Q x)
lookup-Any-All (here {x = x} px) (qx ∷ _ ) = x , (px , qx)
lookup-Any-All (there any) (_ ∷ all) = lookup-Any-All any all
¬Any⇔All¬ : ∀ {A : Set} {P : A → Set} (xs : List A) →
(¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs
¬Any⇔All¬ xs = record
{ to = to' xs
; from = from' xs
}
where
to' : ∀ {A : Set} {P : A → Set} (xs : List A) →
(¬_ ∘ Any P) xs → All (¬_ ∘ P) xs
to' [] _ = []
to' (x ∷ xs) ¬AnyP[x∷xs] = let ¬AnyP[xs] = λ AnyP[xs] → ¬AnyP[x∷xs] (there AnyP[xs]) in
(λ Px → ¬AnyP[x∷xs] (here Px)) ∷ to' xs ¬AnyP[xs]
from' : ∀ {A : Set} {P : A → Set} (xs : List A) →
All (¬_ ∘ P) xs → (¬_ ∘ Any P) xs
from' [] _ ()
from' (x ∷ xs) All¬P[x∷xs] AnyP[x∷xs] = let x , Px , ¬Px = lookup-Any-All AnyP[x∷xs] All¬P[x∷xs] in
¬Px Px
-- > (Can you see why it is important that here _∘_ is generalised to
-- > arbitrary levels, as described in the section on universe
-- > polymorphism?)
--
-- If we look at two functions `f g : ℕ → ℕ`, then the domain `ℕ` and codomain `ℕ`
-- have type `Set₀`
--
-- But in `¬_ ∘ Any P` we're composing a function `¬_ : Set₀ → Set₀`,
-- where the domain `Set₀` and codomain `Set₀` have type `Set₁`.
--
-- To allow the composition `_∘_` to be used in both cases, we need
-- to be polymorphic over the universe level used for the types of domain and codomain,
-- i.e. allow them to have type `Set ℓ` for any universe level `ℓ`.
-- > Do we also have the following?
-- >
-- > (¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs
-- >
-- > If so, prove; if not, explain why.
--
-- The statement does not hold, since it would require us to come up
-- with a proof for some `P x` out of thin air.
--
-- In particular we get stuck in the following definition:
--
-- to' : ∀ {A : Set} {P : A → Set} (xs : List A) →
-- (¬_ ∘ All P) xs → Any (¬_ ∘ P) xs
-- to' [] ¬AllP[[]] = ⊥-elim (¬AllP[[]] [])
-- to' (x ∷ xs) ¬AllP[x∷xs] with to' xs (λ { AllP[xs] → ¬AllP[x∷xs] ({!nope :