Adventures in being construcively negative.

ConsNeg.idr

module ConsNeg

import Data.Nat

%default total

namespace PosNeg

  public export
  data Truth : Type where
    T : (p,n : Type) -> (no : p -> n -> Void) -> Truth

  public export
  Dec : Truth -> Type
  Dec (T p q no)
    = Either q p


  public export
  data IsPos : (t : Truth) -> PosNeg.Dec t -> Type where
    Pos : (val : p) -> IsPos (T p q no) (Right val)


  public export
  data IsNeg : (t : Truth) -> PosNeg.Dec t -> Type where
    Neg : (val : q) -> IsNeg (T p q no) (Left val)

  public export
  isWhat : {t : Truth} -> (r : PosNeg.Dec t) -> Either (IsNeg t r) (IsPos t r)
  isWhat {t = (T p n no)} (Left x) = Left (Neg x)
  isWhat {t = (T p n no)} (Right x) = Right (Pos x)

namespace DecEq

  public export
  prf : Equal x y -> Not (Equal x y) -> Void
  prf Refl no
    = no Refl

  public export
  EQ : (x,y : type) -> Truth
  EQ x y
    = T (Equal x y)
        (Not (Equal x y))
        prf

  public export
  interface DecEq type where
    decEq : (x,y : type)
                -> PosNeg.Dec (EQ x y)

namespace Elem
  public export
  data Elem : (x : type) -> (xs : List type) -> Type where
    H : Equal x y -> Elem x (y::xs)
    T : (no    : Not (Equal x y))
     -> (later : Elem x xs)
              -> Elem x (y::xs)

  public export
  data ElemNot : (x : type) -> (xs : List type) -> Type where
    Empty : ElemNot x Nil
    Extend : Not (Equal x y)
          -> ElemNot    x       xs
          -> ElemNot      x (y::xs)

  public export
  prf : Elem    x xs
     -> ElemNot x xs
     -> Void
  prf (H Refl) (Extend f y) = f Refl

  prf (T no later) (Extend f y) = prf later y

  public export
  ELEM : (x : type) -> (xs : List type) -> Truth
  ELEM x xs
    = T (Elem    x xs)
        (ElemNot x xs)
        prf

  export
  elem : DecEq type
      => (x : type)
      -> (xs : List type)
            -> Dec (ELEM x xs)
  elem x []
    = Left Empty
  elem x (y :: xs) with (decEq x y)
    elem x (x :: xs) | (Right Refl)
      = Right (H Refl)
    elem x (y :: xs) | (Left no) with (elem x xs)
      elem x (y :: xs) | (Left no) | (Left z)
        = Left (Extend no z)
      elem x (y :: xs) | (Left no) | (Right z)
        = Right (T no z)

namespace N

  public export
  prf : GT  x y
     -> LTE x y
     -> Void
  prf (LTESucc z) (LTESucc w)
    = prf z w

  public export
  GT : (x,y : Nat) -> Truth
  GT x y
    = T (GT  x y)
        (LTE x y)
        prf

  export
  isGT : (x,y : Nat) -> PosNeg.Dec (GT x y)
  isGT 0 0 = Left LTEZero
  isGT 0 (S k) = Left LTEZero
  isGT (S k) 0 = Right (LTESucc LTEZero)
  isGT (S k) (S j) with (N.isGT k j)
    isGT (S k) (S j) | (Left x) = Left (LTESucc x)
    isGT (S k) (S j) | (Right x) = Right (LTESucc x)


namespace All

  public export
  data All : (pred : (value : type)
                  -> Truth)
          -> (xs   : List type)
                  -> Type
    where
      Empty : All p Nil
      Extend : (evi  : Dec (p x))
            -> (prf : IsPos (p x) evi)
            -> (rest : All p     xs)
                    -> All p (x::xs)


  public export
  data Any : (pred : (value : type)
                    -> Truth)
             -> (xs   : List type)
                     -> Type
    where
      Here : (evi : Dec (p x))
          -> (prf : IsNeg (p x) evi)
                 -> Any p (x::xs)

      There : (evi  : Dec (p x))
           -> (prf  : IsPos (p x) evi)
           -> (rest : Any p     xs)
                   -> Any p (x::xs)

  public export
  prf : {xs  : List type}
     -> (p : type -> Truth)
     -> All    p xs
     -> Any p xs
     -> Void
  prf _ Empty (Here evi pN) impossible
  prf _ Empty (There evi pN rest) impossible

  prf {xs = (x :: xs)} p (Extend evi pP rest) (Here y pN) with (p x)
    prf {xs = (x :: xs)} p (Extend (Right val) (Pos val) rest) (Here (Left y) pN) | (T z n no)
      = no val y
    prf {xs = (x :: xs)} p (Extend (Right val) (Pos val) rest) (Here (Right y) (Neg pN)) | (T z n no) impossible

  prf {xs = (x :: xs)} p (Extend evi pP rest) (There y pN z) with (p x)
    prf {xs = (x :: xs)} p (Extend (Right val) (Pos val) rest) (There (Right v) (Pos v) z) | (T w n no) with (All.prf p rest z)
      prf {xs = (x :: xs)} p (Extend (Right val) (Pos val) rest) (There (Right v) (Pos v) z) | (T w n no) | boom = boom

  public export
  ALL : (p : type -> Truth) -> (xs : List type) -> Truth
  ALL p xs
    = T (All     p xs)
        (Any     p xs)
        (All.prf p)

  export
  all : {p : type -> Truth}
     -> (f  : (x : type) -> PosNeg.Dec (p x))
     -> (xs : List type)
           -> PosNeg.Dec (ALL p xs)
  all f []
    = Right Empty
  all {p} f (x :: xs) with (p x)
    all {p = p} f (x :: xs) | (T y n no) with (isWhat (f x))
      all {p = p} f (x :: xs) | (T y n no) | (Left z)
        = Left (Here (f x) z)
      all {p = p} f (x :: xs) | (T y n no) | (Right z) with (All.all f xs)
        all {p = p} f (x :: xs) | (T y n no) | (Right z) | (Left w)
          = Left (There (f x) z w)
        all {p = p} f (x :: xs) | (T y n no) | (Right z) | (Right w)
          = Right (Extend (f x) z w)

-- [ EOF ]

repl.txt

λΠ> All.all {p = GT 3} (N.isGT 3) [1,2,3]
Left (There (Right (LTESucc (LTESucc LTEZero))) (Pos (LTESucc (LTESucc LTEZero))) (There (Right (LTESucc (LTESucc (LTESucc LTEZero)))) (Pos (LTESucc (LTESucc (LTESucc LTEZero)))) (Here (Left (LTESucc (LTESucc (LTESucc LTEZero)))) (Neg (LTESucc (LTESucc (LTESucc LTEZero)))))))
λΠ> All.all {p = GT 3} (N.isGT 3) [4,5,6]
Left (Here (Left (LTESucc (LTESucc (LTESucc LTEZero)))) (Neg (LTESucc (LTESucc (LTESucc LTEZero)))))
λΠ> All.all {p = GT 3} (N.isGT 3) [1,2,1]
Right (Extend (Right (LTESucc (LTESucc LTEZero))) (Pos (LTESucc (LTESucc LTEZero))) (Extend (Right (LTESucc (LTESucc (LTESucc LTEZero)))) (Pos (LTESucc (LTESucc (LTESucc LTEZero)))) (Extend (Right (LTESucc (LTESucc LTEZero))) (Pos (LTESucc (LTESucc LTEZero))) Empty)))
λΠ>