FilterEtAl.agda

module FilterEtAl where

data Bool : Set where
  false : Bool
  true  : Bool

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

infixr 40 _∷_

data List (A : Set) : Set where
  []   : List A
  _∷_ : A → List A → List A

infix 20 _⊆_

data _⊆_ {A : Set} : List A → List A → Set where
  stop : [] ⊆ []
  discard : ∀ {xs y ys} → xs ⊆ ys → xs ⊆ y ∷ ys
  keep : ∀ {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys

-----------------------------------------
filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

-- доказываем, что результат фильтрации - подсписок исходного списка
filter⊆ : {A : Set}(p : A → Bool)(xs : List A) → filter p xs ⊆ xs
filter⊆ p [] = stop
filter⊆ p (x ∷ xs) with p x
... | true  = keep (filter⊆  p xs)
... | false = discard (filter⊆  p xs)

-------------------------------------------
take :  ∀ {A} → ℕ → List A → List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

-- доказываем, что результат take - подсписок исходного списка
take⊆ : {A : Set}(n : ℕ)(xs : List A) → take n xs ⊆ xs
take⊆ zero [] = stop
take⊆ zero (x ∷ xs) = discard (take⊆ zero xs)
take⊆ (suc n) [] = stop
take⊆ (suc n) (x ∷ xs) = keep (take⊆ n xs)

-------------------------------------------
drop : ∀ {A} → ℕ → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

-- доказываем, что результат drop - подсписок исходного списка
drop⊆ : {A : Set}(n : ℕ)(xs : List A) → drop n xs ⊆ xs
drop⊆ zero [] = stop
drop⊆ (suc n) [] = stop
drop⊆ zero (x ∷ xs) = keep (drop⊆ zero xs)
drop⊆ (suc n) (x ∷ xs) = discard (drop⊆ n xs)

-----------------------------------------
takeWhile : ∀ {A} → (A → Bool) → List A → List A
takeWhile p []       = []
takeWhile p (x ∷ xs) with p x
... | true  = x ∷ takeWhile p xs
... | false = []

-- доказываем, что результат takeWhile - подсписок исходного списка
-- нам понадобится <<лемма о подсписочности пустого списка>>
lem[]⊆xs : ∀ {A}(xs : List A) → [] ⊆ xs
lem[]⊆xs [] = stop
lem[]⊆xs (x ∷ xs) = discard (lem[]⊆xs xs)
-- теперь пройдёт
takeWhile⊆ : ∀ {A}(p : A → Bool)(xs : List A) → takeWhile p xs ⊆ xs
takeWhile⊆ p [] = stop
takeWhile⊆ p (x ∷ xs) with p x
... | true  = keep (takeWhile⊆ p xs)
... | false = discard (lem[]⊆xs xs)

-- другое доказательство, что результат take - подсписок исходного списка
-- (с помощью леммы lem[]⊆xs)
take⊆₁ : {A : Set}(n : ℕ)(xs : List A) → take n xs ⊆ xs
take⊆₁ zero [] = stop
take⊆₁ (suc n) [] = stop
take⊆₁ zero (x ∷ xs) = discard (lem[]⊆xs xs) -- discard (take⊆₁ zero xs)
take⊆₁ (suc n) (x ∷ xs) = keep (take⊆₁ n xs)

------------------------------------------------------

dropWhile : ∀ {A} → (A → Bool) → List A → List A
dropWhile p []       = []
dropWhile p (x ∷ xs) with p x
... | true  = dropWhile p xs
... | false = x ∷ xs

-- доказать, что результат dropWhile - подсписок исходного списка
dropWhile⊆ : ∀ {A}(p : A → Bool)(xs : List A) → dropWhile p xs ⊆ xs
dropWhile⊆ = {!!}