------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the notion of Interleaving can be used
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module README.Data.List.Relation.Ternary.Interleaving where

open import Level
open import Data.List.Base hiding (filter)
open import Data.List.Relation.Unary.All
open import Function
open import Relation.Nullary
open import Relation.Unary

------------------------------------------------------------------------
-- Interleaving

-- In its most general form, `Interleaving` is parametrised by two
-- relations `L` (for Left) and `R` (for Right). Given three lists,
-- `xs`, `ys` and `zs`, a proof of `Interleaving xs ys zs` is
-- essentially a diagram explaining how `zs` can be pulled apart into
-- `xs` and `ys` in a way compatible with `L` and `R`. For instance:

-- xs               zs               ys
--
-- x₁ -- L x₁ z₁ -- z₁
-- x₂ -- L x₂ z₂ -- z₂
--                  z₃ -- R z₃ z₁ -- y₁
-- x₃ -- L x₃ z₄ -- z₄
--                  z₅ -- R z₅ y₂ -- y₂

open import Data.List.Relation.Ternary.Interleaving.Propositional

-- The special case we will focus on here is the propositional case: both
-- `L` and ̀R` are propositional equality. Rethinking our previous example,
-- this gives us the proof that [z₁, ⋯, z₅] can be partitioned into
-- [z₁, z₂, z₄] on the one hand and [z₃, z₅] in the other.

-- One possible use case for such a relation is the definition of a very
-- precise filter function. Provided a decidable predicate `P`, it will
-- prove not only that the retained values satisfy `P` but that the ones
-- that didn't make the cut satisfy the negation of P.

-- We can make this formal by defining the following record type:

infix  _≡_⊎_
record Filter {a p} {A : Set a} (P : Pred A p) (xs : List A) : Set (a ⊔ p) where
  constructor _≡_⊎_
  field
    -- The result of running filter is two lists:
    -- * the elements we have kept
    -- * and the ones we have thrown away
    -- We leave these implicit: they can be inferred from the rest
    {kept}   : List A
    {thrown} : List A
    -- There is a way for us to recover the original
    -- input by interleaving the two lists
    cover    : Interleaving kept thrown xs
    -- Finally, the partition was made according to the predicate
    allP     : All P kept
    all¬P    : All (∁ P) thrown

-- Once we have this type written down, we can write the function.
-- We use an anonymous module to clean up the function's type.

module _ {a p} {A : Set a} {P : Pred A p} (P? : Decidable P) where

  filter : ∀ xs → Filter P xs
  -- If the list is empty, we are done.
  filter []       = [] ≡ [] ⊎ []
  filter (x ∷ xs) =
    -- otherwise we start by running filter on the tail
    let xs′ ≡ ps ⊎ ¬ps = filter xs in
    -- And depending on whether `P` holds of the head,
    -- we cons it to the `kept` or `thrown` list.
    case P? x of λ where -- [1]
      (yes p) → consˡ xs′ ≡ p ∷ ps ⊎      ¬ps
      (no ¬p) → consʳ xs′ ≡     ps ⊎ ¬p ∷ ¬ps



-- [1] See the following module for explanations of `case_of_` and
--     pattern-matching lambdas
import README.Case