Proof of De Morgan's law in Swift

gistfile1.swift

// ~(P ∨ Q) = ~P ∧ ~Q

enum Nothing {}

struct Not <A> {
  let not: A -> Nothing
  init (_ not: A -> Nothing) { self.not = not }
}

struct And <A, B> {
  let lhs: A
  let rhs: B
  init (_ lhs: A, _ rhs: B) { self.lhs = lhs; self.rhs = rhs }
}

enum Or <A, B> {
  case lhs(@autoclosure () -> A)
  case rhs(@autoclosure () -> B)
}

//// NOT(A) AND NOT(B) => NOT(A OR B)
func dmg1 <A, B> (f: And<Not<A>, Not<B>>) -> Not<Or<A, B>> {

  return Not<Or<A, B>> {(x: Or<A, B>) in
    switch x {
    case let .lhs(a):
      return f.lhs.not(a())
    case let .rhs(b):
      return f.rhs.not(b())
    }
  }
}

//// NOT(A OR B) => NOT(A) AND NOT(B)
func dmg2 <A, B> (f: Not<Or<A, B>>) -> And<Not<A>, Not<B>> {

  return And<Not<A>, Not<B>>(
    Not<A> {a in f.not(.lhs(a))},
    Not<B> {b in f.not(.rhs(b))}
  )
}