{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans

{-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans

{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans

{-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans

{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)

{-# OPTIONS --warning=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)

reverse-++-distrib : ∀ {A : Set} → (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-distrib [] ys = sym (++-identityʳ (reverse ys))
reverse-++-distrib (x ∷ xs) ys =
  begin
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (λ c → c ++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ reverse xs ++ [ x ]
  ∎

reverse-involutive : ∀ {A : Set} → (xs : List A) → reverse (reverse xs) ≡ xs
reverse-involutive [] = refl
reverse-involutive (x ∷ xs) =
  begin
    reverse (reverse xs ++ [ x ])
  ≡⟨ reverse-++-distrib (reverse xs) [ x ] ⟩
    reverse [ x ] ++ reverse (reverse xs)
  ≡⟨⟩
    x ∷ reverse (reverse xs)
  ≡⟨ cong (x ∷_) (reverse-involutive xs) ⟩
    x ∷ xs
  ∎

open import plfa.part1.Isomorphism using (extensionality)
map-distrib-∘ : ∀ {A B C : Set} → (f : A → B) → (g : B → C) → map (g ∘ f) ≡ map g ∘ map f
map-distrib-∘ {A} {B} {C} f g = extensionality (aux f g) where
  aux : (f : A → B) → (g : B → C) → (x : List A) → map (g ∘ f) x ≡ (map g ∘ map f) x
  aux _ _ [] = refl
  aux f g (x ∷ xs) =
    begin
      (g ∘ f) x ∷ map (g ∘ f) xs
    ≡⟨ cong ((g ∘ f) x ∷_) (aux f g xs) ⟩
      (map g ∘ map f) (x ∷ xs)
    ∎

map-++-distribute : ∀ {A B : Set} → (f : A → B) → (xs ys : List A) → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-distribute f [] _ = refl
map-++-distribute f (x ∷ xs) [] rewrite ++-identityʳ xs | ++-identityʳ (map f xs) = refl
map-++-distribute f (x ∷ xs) ys rewrite map-++-distribute f xs ys = refl

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 left b right) = node (map-Tree f g left) (g b) (map-Tree f g right)

product : List ℕ → ℕ
product = foldr _*_ 1
_ : product [ 1 , 2 , 3 , 4 ] ≡ 24
_ = refl

```agda
postulate
  foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
    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 = refl
foldr-++ _⊗_ e (x ∷ xs) ys rewrite foldr-++ _⊗_ e xs ys = refl

foldr-idenityˡ : ∀ {A : Set} → (xs : List A) → foldr _∷_ [] xs ≡ xs
foldr-idenityˡ [] = refl
foldr-idenityˡ (x ∷ xs) rewrite foldr-idenityˡ xs = refl
++-foldr-∷ : ∀ {A : Set} → (xs ys : List A) → xs ++ ys ≡ foldr _∷_ ys xs
++-foldr-∷ [] ys = refl
++-foldr-∷ (x ∷ xs) ys rewrite ++-foldr-∷ xs ys = refl

map-is-foldr : ∀ {A B : Set} → (f : A → B) → map f ≡ foldr (λ x xs → f x ∷ xs) []
map-is-foldr {A} {B} f = extensionality (aux f) where
  aux : (f : A → B) → (xs : List A) → map f xs ≡ foldr (λ x xs → f x ∷ xs) [] xs
  aux f [] = refl
  aux f (x ∷ xs) rewrite aux f xs = refl

fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
fold-Tree f _⊗_ (leaf a) = f a
fold-Tree f _⊗_ (node left b right) = _⊗_ (fold-Tree f _⊗_ left) b (fold-Tree f _⊗_ right)

map-is-foldr-Tree : ∀ {A B C D : Set} → (f : A → C) → (g : B → D) →
  map-Tree f g ≡ fold-Tree (λ a → leaf (f a)) (λ left b right → node left (g b) right)
map-is-foldr-Tree {A} {B} {C} {D} f g = extensionality (aux f g) where
  aux : (f : A → C) → (g : B → D) → (x : Tree A B) →
    map-Tree f g x ≡ fold-Tree (λ a → leaf (f a)) (λ left b → node left (g b)) x
  aux f g (leaf a) = refl
  aux f g (node left b right) rewrite aux f g left | aux f g right = refl

n-suc-n-∸1 : ∀ {n : ℕ} → n * suc (n ∸ 1) ≡ n * n
n-suc-n-∸1 {zero} = refl
n-suc-n-∸1 {suc n} = refl
open import Data.Nat.Properties using (*-distribʳ-+; *-distribˡ-+; *-identityʳ)
sum-n-*-2 : ∀ {n : ℕ} → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-n-*-2 {zero} = refl
sum-n-*-2 {suc n} =
  begin
    sum (n ∷ downFrom n) * 2
  ≡⟨⟩
    (n + sum (downFrom n)) * 2
  ≡⟨ *-distribʳ-+ 2 n (sum (downFrom n)) ⟩
    n * 2 + sum (downFrom n) * 2
  ≡⟨ cong (λ c → n * 2 + c) (sum-n-*-2 {n}) ⟩
    n * 2 + n * (n ∸ 1)
  ≡⟨ sym (*-distribˡ-+ n 2 (n ∸ 1)) ⟩
    n * (2 + (n ∸ 1))
  ≡⟨ cong (λ c → n * c) (+-assoc 1 1 (n ∸ 1)) ⟩
    n * (1 + (1 + (n ∸ 1)))
  ≡⟨ *-distribˡ-+ n 1 (1 + (n ∸ 1)) ⟩
    n * 1 + n * (1 + (n ∸ 1))
  ≡⟨ cong (λ c → c + n * (1 + (n ∸ 1))) (*-identityʳ n) ⟩
    n + n * (1 + (n ∸ 1))
  ≡⟨ cong (n +_) (n-suc-n-∸1 {n}) ⟩
    n + n * n
  ∎

foldl : ∀ {A B : Set} → (B → A → B) → B → List A → B
foldl _⊗_ e []        =  e
foldl _⊗_ e (x ∷ xs)  =  foldl _⊗_ (e ⊗ x) xs

foldl-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e →
  ∀ (xs : List A) (y : A) → foldl _⊗_ y xs ≡ y ⊗ foldl _⊗_ e xs
foldl-monoid _⊗_ e monoid-⊗ [] y = sym (identityʳ monoid-⊗ y)
foldl-monoid _⊗_ e monoid-⊗ (x ∷ xs) y =
  begin
    foldl _⊗_ y (x ∷ xs)
  ≡⟨⟩
    foldl _⊗_ (y ⊗ x) xs
  ≡⟨ foldl-monoid _⊗_ e monoid-⊗ xs (y ⊗ x) ⟩
    (y ⊗ x) ⊗ foldl _⊗_ e xs
  ≡⟨ assoc monoid-⊗ y x (foldl _⊗_ e xs) ⟩
    y ⊗ (x ⊗ foldl _⊗_ e xs)
  ≡⟨ cong (y ⊗_) (sym (foldl-monoid _⊗_ e monoid-⊗ xs x)) ⟩
    (y ⊗ foldl _⊗_ x xs)
  ≡⟨ cong (λ c → y ⊗ foldl _⊗_ c xs) (sym (identityˡ monoid-⊗ x)) ⟩
    (y ⊗ foldl _⊗_ (e ⊗ 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 monoid-⊗ [] = refl
foldr-monoid-foldl _⊗_ e monoid-⊗ (x ∷ xs) =
  begin
    (x ⊗ foldr _⊗_ e xs)
  ≡⟨ cong (λ c → x ⊗ c) (foldr-monoid-foldl _⊗_ e monoid-⊗ xs) ⟩
    (x ⊗ foldl _⊗_ e xs)
  ≡⟨ sym (foldl-monoid _⊗_ e monoid-⊗ xs x) ⟩
    foldl _⊗_ x xs
  ≡⟨ cong (λ c → foldl _⊗_ c xs) (sym (identityˡ monoid-⊗ x)) ⟩
    foldl _⊗_ (e ⊗ x) xs
  ∎

open import Data.Sum using (_⊎_; inj₁; inj₂)
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 p = inj₂ p
  to (x ∷ xs) ys (here p) = inj₁ (here p)
  to (x ∷ xs) ys (there p) with to xs ys p
  ...                         | inj₁ p = inj₁ (there p)
  ...                         | inj₂ p = inj₂ p
  from : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
    Any P xs ⊎ Any P ys → Any P (xs ++ ys)
  from [] ys (inj₂ p) = p
  from (x ∷ xs) ys (inj₁ (here x₁)) = here x₁
  from (x ∷ xs) ys (inj₁ (there p)) = there (from xs ys (inj₁ p))
  from (x ∷ xs) ys (inj₂ p) = there (from xs ys (inj₂ p))
∈-++ : ∀ {A : Set} (xs ys : List A) → (x : A) → (x ∈ (xs ++ ys)) ⇔ (x ∈ xs ⊎ x ∈ ys)
∈-++ xs ys x = Any-++-⇔ {P = x ≡_} xs ys

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) → (p : All P (xs ++ ys)) → (All P xs × All P ys)
    to xs ys = _⇔_.to (All-++-⇔ xs ys)
    from : ∀ {A : Set} {P : A → Set} → (xs ys : List A) → (p : (All P xs × All P ys)) → All P (xs ++ ys)
    from xs ys = _⇔_.from (All-++-⇔ xs ys)
    from∘to : ∀ {A : Set} {P : A → Set} → (xs ys : List A) → (p : All P (xs ++ ys)) → from xs ys (to xs ys p) ≡ p
    from∘to [] ys p = refl
    from∘to (x ∷ xs) ys (px ∷ pxs++ys) = cong (px ∷_) (from∘to xs ys pxs++ys)
    to∘from : ∀ {A : Set} {P : A → Set} → (xs ys : List A) → (p : All P xs × All P ys) → to xs ys (from xs ys p) ≡ p
    to∘from [] ys ⟨ [] , pys ⟩ = refl
    to∘from (x ∷ xs) ys ⟨ px ∷ pxs , pys ⟩ =
      begin
        to (x ∷ xs) ys (from (x ∷ xs) ys ⟨ px ∷ pxs , pys ⟩)
      ≡⟨ cong (λ (⟨ pxs , pys ⟩) → ⟨ px ∷ pxs , pys ⟩) (to∘from xs ys ⟨ pxs , pys ⟩) ⟩
        ⟨ px ∷ pxs , pys ⟩
      ∎

¬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) → (p : (¬_ ∘ Any P) xs) → All (¬_ ∘ P) xs
    to [] p = []
    to (x ∷ xs) p = (λ px → p (here px)) ∷ to xs (λ pxs → p (there pxs))
    from : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : All (¬_ ∘ P) xs) → (¬_ ∘ Any P) xs
    from [] p = λ ()
    from (x ∷ xs) (¬px ∷ ¬pxs) = λ { (here px) → ¬px px ; (there pxs) → (from xs ¬pxs) pxs}
-- Composition without polymorphic levels
_∘'_ : ∀ {A : Set} {B : A → Set} {C : {x : A} → B x → Set} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘' g = λ x → f (g x)
-- Without polymorphic levels we can `UnequalSorts` error, because P is dependent on A, so its level is in fn composition is actually `Set₁` and the level of the left side of composition has to be the same or higher
-- ¬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) → (p : (¬_ ∘' Any P) xs) → All (¬_ ∘' P) xs
--     to [] p = []
--     to (x ∷ xs) p = (λ px → p (here px)) ∷ to xs (λ pxs → p (there pxs))
--     from : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : All (¬_ ∘' P) xs) → (¬_ ∘' Any P) xs
--     from [] p = λ ()
--     from (x ∷ xs) (¬px ∷ ¬pxs) = λ { (here px) → ¬px px ; (there pxs) → (from xs ¬pxs) pxs}
-- `(¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs`
-- Doesn't hold because when `xs` is non-empty, from `¬ ∘ All` we know that there
-- is some element for which the predicate doesn't hold, but we don't know which
-- one.

¬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
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
  where
    to : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : (¬_ ∘ Any P) xs) → All (¬_ ∘ P) xs
    to [] p = []
    to (x ∷ xs) p = (λ px → p (here px)) ∷ to xs (λ pxs → p (there pxs))
    from : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : All (¬_ ∘ P) xs) → (¬_ ∘ Any P) xs
    from [] p = λ ()
    from (x ∷ xs) (¬px ∷ ¬pxs) = λ { (here px) → ¬px px ; (there pxs) → (from xs ¬pxs) pxs}
    from∘to : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : (¬_ ∘ Any P) xs) → from xs (to xs p) ≡ p
    from∘to xs p = refl
    to∘from : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : All (¬_ ∘ P) xs) → to xs (from xs p) ≡ p
    to∘from [] [] = refl
    to∘from (x ∷ xs) (px ∷ pxs) = cong (px ∷_) (to∘from xs pxs)

open import plfa.part1.Isomorphism using (∀-extensionality)
open import Data.Empty using (⊥-elim)
open Eq using (cong-app)
All-∀ : ∀ {A : Set} {P : A → Set} → (xs : List A) → All P xs ≃ ∀ x → x ∈ xs → P x
All-∀ xs =
  record
    { to = to xs
    ; from = from xs
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
  where
    to : ∀ {A : Set} {P : A → Set} → (xs : List A) → All P xs → (x : A) → x ∈ xs → P x
    to [] [] x ()
    to (x ∷ xs) (Px ∷ Pxs) a (here refl) = Px
    to (x ∷ xs) (Px ∷ Pxs) a (there Pa) = to xs Pxs a Pa
    from : ∀ {A : Set} {P : A → Set} → (xs : List A) → ((x : A) → x ∈ xs → P x) → All P xs
    from [] ∀Px = []
    from (x ∷ xs) ∀Px = ∀Px x (here refl) ∷ (from xs λ a a∈xs → ∀Px a (there a∈xs))
    from∘to : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : All P xs) → from xs (to xs p) ≡ p
    from∘to [] [] = refl
    from∘to (x ∷ xs) (Px ∷ Pxs) = cong (Px ∷_) (from∘to xs Pxs)
    to∘from : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : ((x : A) → x ∈ xs → P x)) → to xs (from xs p) ≡ p
    to∘from [] P = ∀-extensionality (λ a → extensionality λ ())
    to∘from (x ∷ xs) P = ∀-extensionality λ a → extensionality λ
      { (here refl) → refl
      ; (there a∈xs) →
          cong-app
            (cong-app
              (to∘from xs (λ a' a'∈xs → P a' (there a'∈xs)))
              a
            )
            a∈xs
      }

Any-∃ : ∀ {A : Set} {P : A → Set} → (xs : List A) → Any P xs ≃ ∃[ x ] (x ∈ xs × P x)
Any-∃ xs =
  record
    { to = to xs
    ; from = from xs
    ; from∘to = from∘to xs
    ; to∘from = to∘from xs
    }
  where
    to : ∀ {A : Set} {P : A → Set} → (xs : List A) → Any P xs → ∃[ x ] (x ∈ xs × P x)
    to [] ()
    to (x ∷ xs) (here Px) = ⟨ x , ⟨ here refl , Px ⟩ ⟩
    to (x ∷ xs) (there Pxs) with to xs Pxs
    ...                        | ⟨ a , ⟨ a∈as , Pa ⟩ ⟩ = ⟨ a , ⟨ there a∈as , Pa ⟩ ⟩
    from : ∀ {A : Set} {P : A → Set} → (xs : List A) → ∃[ x ] (x ∈ xs × P x) → Any P xs
    from [] ()
    from (x ∷ xs) ⟨ a , ⟨ here refl , Pa ⟩ ⟩ = here Pa
    from (x ∷ xs) ⟨ a , ⟨ there a∈xs , Pas ⟩ ⟩ with from xs ⟨ a , ⟨ a∈xs , Pas ⟩ ⟩
    ...                                           | P = there P
    from∘to : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : Any P xs) → from xs (to xs p) ≡ p
    from∘to (x ∷ xs) (here Px) = refl
    from∘to (x ∷ xs) (there Pxs) = cong there (from∘to xs Pxs)
    to∘from : ∀ {A : Set} {P : A → Set} → (xs : List A) → (p : ∃[ x ] (x ∈ xs × P x)) → to xs (from xs p) ≡ p
    to∘from [] ()
    to∘from xs ⟨ a , ⟨ here refl , Pa ⟩ ⟩ = refl
    to∘from (x ∷ xs) ⟨ a , ⟨ there a∈xs , Pa ⟩ ⟩ =
      cong
        (λ (⟨ a' , ⟨ a∈xs , Pa' ⟩ ⟩) → ⟨ a' , ⟨ there a∈xs , Pa' ⟩ ⟩)
        (to∘from xs ⟨ a , ⟨ a∈xs , Pa ⟩ ⟩)

any : ∀ {A : Set} → (A → Bool) → List A → Bool
any p  =  foldr _∨_ false ∘ map p
Any? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (Any P)
Any? P? [] = no λ ()
Any? P? (x ∷ xs) with P? x | Any? P? xs
... | yes Px | _ = yes (here Px)
... | no ¬Px | yes Pxs = yes (there Pxs)
... | no ¬Px | no ¬Pxs = no λ{ (here Px) → ¬Px Px ; (there Pxs) → ¬Pxs Pxs }

split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
  → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
split P? [] = ⟨ [] , ⟨ [] , ⟨ [] , ⟨ [] , [] ⟩ ⟩ ⟩ ⟩
split P? (z ∷ zs) with P? z | split P? zs
... | yes Pz | ⟨ xs , ⟨ ys , ⟨ merge , ⟨ ∀Pxs , ∀¬Pys ⟩ ⟩ ⟩ ⟩ =
               ⟨ z ∷ xs , ⟨ ys , ⟨ left-∷ merge , ⟨ Pz ∷ ∀Pxs , ∀¬Pys ⟩ ⟩ ⟩ ⟩
... | no ¬Pz | ⟨ xs , ⟨ ys , ⟨ merge , ⟨ ∀Pxs , ∀¬Pys ⟩ ⟩ ⟩ ⟩ =
               ⟨ xs , ⟨ z ∷ ys , ⟨ right-∷ merge , ⟨ ∀Pxs , ¬Pz ∷ ∀¬Pys ⟩ ⟩ ⟩ ⟩