propToDeMorgan.idr

%default total

data Prop = Var String 
          | Not Prop 
          | And Prop Prop 
          | Or Prop Prop 
          | Impl Prop Prop
          | Equiv Prop Prop

data Lit = Stmt String | Neg String

-- V OR
data Clause = Bot | Disj Lit Clause

-- ^ AND
data CNF = Top | Conj Clause CNF

data ConjForm = LitC String
              | NotC ConjForm
              | AndC ConjForm ConjForm
              | OrC ConjForm ConjForm

pureClause : String -> Clause
pureClause x = Disj (Stmt x) Bot

pureCNF : String -> CNF
pureCNF x = Conj (pureClause x) Top


toConjForm' : (p: Prop) -> ConjForm
toConjForm' (Var x) = LitC x
toConjForm' (Not x) = NotC (toConjForm' x)
toConjForm' (And x y) = AndC (toConjForm' x) (toConjForm' y)
toConjForm' (Or x y) = OrC (toConjForm' x) (toConjForm' y)
toConjForm' (Impl x y) = OrC (NotC (toConjForm' x)) (toConjForm' y)
toConjForm' (Equiv x y) with ((toConjForm' x), (toConjForm' y))
  toConjForm' (Equiv x y) | (a, b) = AndC (OrC (NotC a) b) (OrC (NotC b) a)

data DeMorganStmt = LitD String | NegD DeMorganStmt

data DeMorgan : Type where
  StmtD : DeMorganStmt -> DeMorgan
  AndD : DeMorgan -> DeMorgan -> DeMorgan
  OrD : DeMorgan -> DeMorgan -> DeMorgan

toDeMorgan : ConjForm -> DeMorgan
toDeMorgan (LitC x) = StmtD (LitD x)
toDeMorgan (NotC x) with (toDeMorgan x)
  toDeMorgan (NotC x) | (StmtD y) = StmtD (NegD y)
  toDeMorgan (NotC x) | (AndD y z) = AndD (?toDeMorgan_rhs_2) ?And_morgan_rhs
  toDeMorgan (NotC x) | (OrD y z) = ?toDeMorgan_rhs_5
toDeMorgan (AndC x y) = AndD (toDeMorgan x) (toDeMorgan y)
toDeMorgan (OrC x y) = OrD (toDeMorgan x) (toDeMorgan y)