\import Data.Bool (Bool, So, false, not, true)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.Unique
\import Meta
\import Paths
\import Paths.Meta

\data Dec (E : \Prop)
  | yes E
  | no (Not E)
  \where {
    \use \level levelProp {E : \Prop} : isProp (Dec E)
      => isProp-prover

    \func rec {R : \Type} {E : \Prop} (y : E -> R) (n : Not E -> R) (d : Dec E) : R \elim d
      | yes e => y e
      | no q => n q
  }

\lemma negated-dec (E : \Prop) {P : NegatedProp} (f : Dec E -> P) : P
  => isNegated \lam g => g $ f $ no \lam e => g $ f (yes e)

\func decToBool {E : \Prop} (d : Dec E) : Bool
  | yes _ => true
  | no _ => false

\class Decide (E : \Prop)
  | decide : Dec E

\lemma dec_decide {E : \Prop} (d : Dec E) : Decide E \cowith
  | decide => d

\lemma dec_yes_reduce {E : \Prop} {d : Dec E} (e : E) : d = yes e
  => prop-pi

\lemma dec_no_reduce {E : \Prop} {d : Dec E} (q : Not E) : d = no q
  => prop-pi

\lemma Dec_|| {A B : \Prop} (d : Dec A) (e : Dec B) : Dec (A || B) \elim d, e
  | yes e, _ => yes (byLeft e)
  | _, yes e => yes (byRight e)
  | no q, no q' => no \case __ \with {
    | byLeft a => q a
    | byRight b => q' b
  }

\func SigmaDecide {A : Decide} (B : A -> Decide) : Decide (\Sigma (a : A) (B a)) \cowith
  | decide => \case A.decide \with {
    | yes a => \case decide {B a} \with {
      | yes b => yes (a,b)
      | no q => no \lam p => q $ transport (B __) prop-pi p.
    }
    | no q => no \lam p => q p.
  }

\instance ProductDecide (A B : Decide) : Decide => SigmaDecide {A} (\lam _ => B)

\lemma NotDec {P : \Prop} (d : Dec P) : Dec (Not P) \elim d
  | yes a => no \lam f => f a
  | no q => yes q

\instance NotDecide (A : Decide) : Decide (Not A)
  | decide => NotDec A.decide

\class BaseSet (E : \Set)

\class SubSet (S : BaseSet) (\classifying contains : S -> \Prop) {
  \func ISet : BaseSet \cowith
    | E => \Sigma (x : S) (contains x)
}

\class DecSubSet \extends SubSet
  | isDec (x : S) : Dec (contains x)
  \where {
    \func max {S : BaseSet} : DecSubSet S \cowith
      | contains _ => \Sigma
      | isDec _ => yes ()
  }

\class SeparatedSet \extends BaseSet
  | separatedEq {x y : E} : Not (Not (x = y)) -> x = y

-- | A set with a tight apartness relation.
\class Set# \extends SeparatedSet {
  | \infix  # : E -> E -> \Prop
  | #-irreflexive {x : E} : Not (x # x)
  | #-symmetric {x y : E} : x # y -> y # x
  | #-comparison (x y z : E) : x # z -> x # y || y # z
  | tightness {x y : E} : Not (x # y) -> x = y
  | separatedEq {x} ~~x=y => tightness (\lam x#y => ~~x=y (\lam x=y => #-irreflexive (transport (x #) (inv x=y) x#y)))

  \lemma apartNotEqual {x y : E} (x#y : x # y) : x /= y =>
    \lam x=y => #-irreflexive (transport (x #) (inv x=y) x#y)
}

\class DecSet \extends BaseSet, Set# {
  \field decideEq (x y : E) : Dec (x = y)
  | nonEqualApart {x y : E} : x /= y -> x # y
  | \infix  == : E -> E -> Bool
  | == x y => decToBool (decideEq x y)

  \default # x y : \Prop => x /= y
  \default nonEqualApart \as nonEqualApartImpl {x} {y} (p : x /= y) : x # y => p
  \default #-irreflexive {x} (x/=x : x # x) : Empty => x/=x idp
  \default #-symmetric {x} {y} (x/=y : x # y) : y # x => /=-sym x/=y
  \default #-comparison x y z (x/=z : x # z) : x # y || y # z => \case decideEq x y \with {
    | yes x=y => byRight (\lam y=z => x/=z (x=y *> y=z))
    | no x/=y => byLeft x/=y
  }
  \default tightness {x} {y} (x//=y : Not (x # y)) : x = y => \case decideEq x y \with {
    | yes x=y => x=y
    | no x/=y => absurd (x//=y x/=y)
  }
}

\func SigmaDecSet {A : DecSet} (B : A -> DecSet) : DecSet (\Sigma (a : A) (B a)) \cowith
  | decideEq p q => \case decideEq p. q. \with {
    | yes e => \case decideEq (transport (\lam a => B a) e p.) q. \with {
      | yes e' => yes (ext (e,e'))
      | no n => no (\lam e' => n (rewrite (prop-isProp e (pmap __. e')) (pmapd __. e')))
    }
    | no n => no (\lam e => n (pmap __. e))
  }

\func SubDecSet {A : DecSet} {B : A -> \Prop} : DecSet (\Sigma (a : A) (B a))
  => SigmaDecSet \lam a => \new DecSet (B a) {
    | decideEq b b' => yes prop-pi
  }

\instance DecBool : DecSet
  | E => Bool
  | decideEq x y => compare x y
  \where {
    \func compare (a b : Bool) : Dec (a = b)
      | false, false => yes idp
      | false, true => no contradiction
      | true, false => no contradiction
      | true, true => yes idp
  }

\instance ProductDecSet (A B : DecSet) : DecSet (\Sigma A B)
  => SigmaDecSet (\lam _ => B)

\instance EqualityDecide (A : DecSet) (a a' : A) : Decide (a = a')
  | decide => decideEq a a'

\instance ArrayDec (A : DecSet) (n : Nat) : DecSet (Array A n)
  | decideEq => aux
  \where {
    \private \func aux {n : Nat} (l l' : Array A n) : Dec (l = l') \elim n, l, l'
      | , nil, nil => yes idp
      | suc n, a :: l, a' :: l' => \case decideEq a a', aux l l' \with {
        | yes e, yes e' => yes $ pmap2 (::) e e'
        | _, no q => no \lam p => q \lam i => \new Array A n \lam j => p i (suc j)
        | no q, _ => no \lam p => q \lam i => p i 
      }
  }

\lemma decideEq=_reduce {A : DecSet} {x y : A} (p : x = y) : decideEq x y = yes p
  => prop-pi

\lemma decideEq/=_reduce {A : DecSet} {x y : A} (p : x /= y) : decideEq x y = no p
  => prop-pi

\lemma ==_= {A : DecSet} {a a' : A} (so : So (a == a')) : a = a'
  => unfold (==) at so $ mcases {decToBool} so _ \with {
    | yes p, _ => p
    | no n, ()
  }

\lemma =-dec {A : DecSet} {a a' : A} {so : So (a == a')} : a = a'
  => ==_= so

\lemma /=-dec {A : DecSet} {a a' : A} {so : So (not (a == a'))} : a /= a'
  => unfold (==) at so $ mcases {decToBool} so _ \with {
    | yes _, ()
    | no p, _ => p
  }

\truncated \data Trunc0 (A : \Type) : \Set
  | in0 A
  \where {
    \func map {A B : \Type} (t : Trunc0 A) (f : A -> B) : Trunc0 B \elim t
      | in0 a => in0 (f a)
  }