List inclusion predicate in Idris

inclusion.idr

module inclusion

import Data.List

%default total

-- List intersection
namespace intersect
  -- Intersection operation
  %hide List.intersect
  intersect : Eq a => List a -> List a -> List a
  intersect [] ys = []
  intersect (x :: xs) ys with (elem x ys)
    intersect (x :: xs) ys | True  = x :: (intersect xs ys)
    intersect (x :: xs) ys | False = intersect xs ys

  -- Some lemmas specifying the semantic of intersection
  lemma_intersectNil : Eq a => (s : List a) -> intersect s [] = []
  lemma_intersectNil []        = Refl
  lemma_intersectNil (x :: xs) = lemma_intersectNil xs

  postulate lemma_intersectReducX : Eq a => (xs, ys : List a) -> (z : a) ->
                                    (z = x -> Void) ->
                                    Elem z (intersect (x :: xs) ys) ->
                                    intersect (x :: xs) ys = intersect xs ys

  postulate lemma_intersectReducY : Eq a => (xs, ys : List a) -> (z : a) ->
                                    (z = y -> Void) ->
                                    Elem z (intersect xs (y :: ys)) ->
                                    intersect xs (y :: ys) = intersect xs ys

  -- In intersection predicate
  InIntersection : a -> List a -> List a -> Type
  InIntersection z xs ys = (Elem z xs, Elem z ys)

  -- Decides whether an element is in the intersection of two list or not
  inIntersection : DecEq a => (z : a) -> (xs : List a) -> (ys : List a) ->
                   Dec (InIntersection z xs ys)
  inIntersection z xs ys with (isElem z xs)
    inIntersection z xs ys | (Yes zinxs) with (isElem z ys)
      inIntersection z xs ys | (Yes zinxs) | (Yes zinys) =
                                           Yes (zinxs, zinys)
      inIntersection z xs ys | (Yes zinxs) | (No zninys) =
                                           No (\(_,zinys) => zninys zinys)
    inIntersection z xs ys | (No zninxs) = No (\(zinxs,_) => zninxs zinxs)

  -- z ∈ (xs ∩ ys) ⇒ z ∈ xs ∧ z ∈ ys
  elemInter : (Eq a, DecEq a) => (xs, ys : List a) -> (z : a) ->
              Elem z (intersect xs ys) -> InIntersection z xs ys
  elemInter xs ys z zInZs = let zInXs = elemInterXs xs ys z zInZs in
                            let zInYs = elemInterYs xs ys z zInZs in
                            (zInXs, zInYs)
    where
    elemInterXs : (Eq a, DecEq a) => (xs, ys : List a) -> (z : a) ->
                  Elem z (intersect xs ys) -> Elem z xs
    elemInterXs []        _  z zInZs = zInZs
    elemInterXs (x :: xs) ys z zInZs with (decEq z x)
      elemInterXs (z :: xs) _  z zInZs  | (Yes Refl)  = Here
      elemInterXs (x :: xs) ys z zInZs  | (No contra) =
                                let zInZsReduc = ?zInZsReducX in
                                let zInXs = elemInterXs xs ys z zInZsReduc in
                                There zInXs

    elemInterYs : (Eq a, DecEq a) => (xs, ys : List a) -> (z : a) ->
                  Elem z (intersect xs ys) -> Elem z ys
    elemInterYs xs []        z zInZs =
                                rewrite sym $ lemma_intersectNil xs in zInZs
    elemInterYs xs (y :: ys) z zInZs with (decEq z y)
      elemInterYs xs (z :: ys) z zInZs | (Yes Refl) = Here
      elemInterYs xs (y :: ys) z zInZs | (No contra) =
                                let zInZsReduc = ?zInZsReducY in
                                let zInYs = elemInterYs xs ys z zInZsReduc in
                                There zInYs

-- Inclusion predicate
--
-- Asserts that the elements of the first list are elements of the
-- second list.
Include : List a -> List a -> Type
Include xs ys = (z : _) -> Elem z xs -> Elem z ys

-- Reduction of the Include predicate
includeReduc : Include (x :: xs) ys -> Include xs ys
includeReduc xxsIncYs = \z,zInXs => xxsIncYs z (There zInXs)

-- Being an element of a singleton list implies to be that singleton
elemSingleton : Elem z [x] -> z = x
elemSingleton Here           = Refl
elemSingleton (There zInNil) = absurd zInNil

-- Being an element of a not empty list and not being the fisrt
-- element implies to be an element of the tail.
elemTail : (z = hd -> Void) -> Elem z (hd :: tl) -> Elem z tl
elemTail nzIsHd zInHdTl   {tl = []} = let zIsHd = elemSingleton zInHdTl in
                                      void $ nzIsHd zIsHd
elemTail nzIsHd Here      {tl}      = void $ nzIsHd Refl
elemTail nzIsHd (There p) {tl}      = p

-- Are the elements of the first list are elements of the second
-- list.
isIncluded : DecEq a => (xs : List a) -> (ys : List a) ->
             Dec (Include xs ys)
-- This definition seems correct since I cannot provide any `z` due
-- to the empty `xs`.
isIncluded []        ys         = Yes (\z,zInXs => absurd zInXs)
isIncluded (x :: xs) ys with (isIncluded xs ys)
  isIncluded (x :: xs) ys | (No nxsIncYs) =
                             No $ notTailInc nxsIncYs
    where
    notTailInc : (Include xs ys -> Void) -> Include (x :: xs) ys -> Void
    notTailInc nxsIncYs xxsIncYs = nxsIncYs (\z,zInXs =>
                                               xxsIncYs z (There zInXs))

  isIncluded (x :: xs) ys | (Yes xsIncYs) with (isElem x ys)
    isIncluded (x :: xs) ys | (Yes xsIncYs) | (Yes xInYs) =
                             Yes $ headInTailInc xInYs xsIncYs
      where
      headInTailInc : Elem x ys -> Include xs ys -> Include (x :: xs) ys
      headInTailInc xInYs xsIncYs = \z,zInXxs => case decEq z x of
                       No nzIsX => let zInXs = elemTail nzIsX zInXxs in
                                   xsIncYs z zInXs
                       Yes zIsX => rewrite zIsX in xInYs

    isIncluded (x :: xs) ys | (Yes xsIncYs) | (No nxInYs) =
                             No $ notHeadIn nxInYs
      where
      notHeadIn : (Elem x ys -> Void) -> Include (x :: xs) ys -> Void
      notHeadIn nxInYs xxsIncYs = let xInYs = xxsIncYs x Here in
                                  nxInYs xInYs

-- The result of the intersection between two list `xs` and `ys` is
-- both included in `xs` and `ys`.
intersectIncluded : (Eq a, DecEq a) => (xs, ys : List a) ->
                    (Include (intersect xs ys) xs,
                     Include (intersect xs ys) ys)
intersectIncluded xs ys =
  let zsIncXs = \z,zInZs => fst $ elemInter xs ys z zInZs in
  let zsIncYs = \z,zInZs => snd $ elemInter xs ys z zInZs in
  (zsIncXs, zsIncYs)


---------- Proofs ----------

inclusion.intersect.zInZsReducX = proof
  intros
  rewrite lemma_intersectReducX xs ys z contra zInZs
  exact zInZs


inclusion.intersect.zInZsReducY = proof
  intros
  rewrite lemma_intersectReducY xs ys z contra zInZs
  exact zInZs