Bool.fm

// Booleans.
T Bool
| Bool.true;
| Bool.false;

// Boolean negation.
Bool.not(a: Bool):  Bool
  case a:
  | Bool.false;
  | Bool.true;

// Is any of the bools true?
Bool.or(a: Bool, b: Bool): Bool
  case a:
  | Bool.true;
  | case b:
    | Bool.true;
    | Bool.false;;

// Are both bools true?
Bool.and(a: Bool, b: Bool): Bool
  case a:
  | case b:
    | Bool.true;
    | Bool.false;;
  | Bool.false;

// Are both booleans equal?
Bool.eql(a: Bool, b: Bool): Bool
  case a:
  | case b: 
    | Bool.true;
    | Bool.false;;
  | case b:
    | Bool.false;
    | Bool.true;;

// Dependent elimination of Bool.
Bool.elim(b: Bool): <P: Bool -> Type> -> P(Bool.true) -> P(Bool.false) -> P(b)
  <P> (t) (f) b<P>(t, f)

// If-then-else
Bool.if<A: Type>(cond: Bool, true_case: A, false_case: A): A
  case cond:
  | true_case;
  | false_case;

// Boolean negation, fusible
Bool.notf(a: Bool): Bool
  <P> (t) (f)
  case a:
  | f;
  | t;
  : P(Bool.notf(a.self));

// Converts to a string
Bool.show(b: Bool): String
  case b:
  | "Bool.true";
  | "Bool.false";

// Ensures a Bool is true
Bool.IsTrue(b: Bool): Type
  case b:
  | Unit;
  | Empty;

// Ensures a Bool is false
Bool.IsFalse(b: Bool): Type
  case b:
  | Empty;
  | Unit;

// Proof that true != false
Bool.true_isnt_false: Not(Equal(Bool, Bool.true, Bool.false))
  def P(b : Bool)
    case b:
    | Unit;
    | Empty;
  def p_true
    Unit.new
  (true_is_false)
    Equal.rewrite<_,_,_,P>(true_is_false, p_true)
  
// Proof that false != true
Bool.false_isnt_true: Not(Equal(Bool, Bool.false, Bool.true))
  def P(b : Bool)
    case b:
    | Empty;
    | Unit;
  def p_false
    Unit.new
  (false_is_true)
    Equal.rewrite<_,_,_,P>(false_is_true, p_false)

// Bool that is provably different from the input
Bool.test.different_elem: (a: Bool) -> Subset(Bool, (b) Not(Equal(Bool, a, b)))
  (a)
  a<(self) Subset(Bool, (b) Not(Equal(Bool, self, b)))>
  | Subset.new<Bool, (b) Not(Equal(Bool, Bool.true, b))>(Bool.false)<Bool.true_isnt_false>;
  | Subset.new<Bool, (b) Not(Equal(Bool, Bool.false, b))>(Bool.true)<Bool.false_isnt_true>;

// Proof that not(not(b)) == b
Bool.double_negation_theorem(b: Bool): Equal(Bool, Bool.not(Bool.not(b)), b)
  case b:
  | Equal.to<_, Bool.true>;
  | Equal.to<_, Bool.false>;
  : Equal(Bool, Bool.not(Bool.not(b.self)), b.self);

Bool.andVar: (n: Nat) -> Variadic(n)(Bool)(Bool)
  Variadic.foldr<Bool><Bool>(Bool.and)(Bool.true)

Bool.orVar: (n: Nat) -> Variadic(n)(Bool)(Bool)
  Variadic.foldr<Bool><Bool>(Bool.or)(Bool.false)