module Base

/*
  Core propositional facts used throughout the standard library.

  This file deliberately stays small and dependency-free: it gives
  reusable lemmas about booleans, negation, implication, iff, and
  common proof patterns such as contrapositive reasoning.
*/

// Eliminate the left side of a disjunction when it is known false.
theorem or_not: all P:bool, Q:bool.
  if (P or Q) and not P
  then Q
proof
  arbitrary P:bool, Q:bool
  suppose prem
  cases conjunct 0 of prem
  case p {
    conclude false  by apply (conjunct 1 of prem) to p
  }
  case q {
    q
  }
end

// Boolean excluded middle: every boolean is either true or false.
theorem ex_mid: all b:bool. b or not b
proof
  arbitrary b:bool
  switch b {
    case true { . }
    case false { . }
  }
end

// Disjunction is symmetric.
theorem or_sym: all P:bool, Q:bool.  (P or Q) = (Q or P)
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Disjunction is associative.
theorem or_assoc: all P:bool, Q:bool, R:bool.
  (P or (Q or R)) = ((P or Q) or R)
proof
  arbitrary P:bool, Q:bool, R:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Disjunction is idempotent.
theorem or_idempotent: all P:bool. (P or P) = P
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Disjoining with true yields true.
theorem or_true: all P:bool. (P or true) = true
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// false is the identity for disjunction.
theorem or_false: all P:bool. (P or false) = P
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Conjunction is symmetric.
theorem and_sym: all P:bool, Q:bool.  (P and Q) = (Q and P)
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Conjunction is associative.
theorem and_assoc: all P:bool, Q:bool, R:bool.
  (P and (Q and R)) = ((P and Q) and R)
proof
  arbitrary P:bool, Q:bool, R:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Conjunction is idempotent.
theorem and_idempotent: all P:bool. (P and P) = P
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// true is the identity for conjunction.
theorem and_true: all P:bool. (P and true) = P
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Conjoining with false yields false.
theorem and_false: all P:bool. (P and false) = false
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Conjunction distributes over disjunction on the left.
theorem and_or_distrib: all P:bool, Q:bool, R:bool.
  (P and (Q or R)) = ((P and Q) or (P and R))
proof
  arbitrary P:bool, Q:bool, R:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Disjunction distributes over conjunction on the left.
theorem or_and_distrib: all P:bool, Q:bool, R:bool.
  (P or (Q and R)) = ((P or Q) and (P or R))
proof
  arbitrary P:bool, Q:bool, R:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Absorption: a conjunction is dominated by a disjunct it contains.
theorem and_or_absorb: all P:bool, Q:bool. (P and (P or Q)) = P
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Absorption: a disjunction is dominated by a conjunct it contains.
theorem or_and_absorb: all P:bool, Q:bool. (P or (P and Q)) = P
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// De Morgan's law for conjunction.
theorem not_and: all P:bool, Q:bool.
  (not (P and Q)) = ((not P) or (not Q))
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// De Morgan's law for disjunction.
theorem not_or: all P:bool, Q:bool.
  (not (P or Q)) = ((not P) and (not Q))
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Relate a proposition to equality with the boolean value true.
theorem eq_true: all P:bool. P ⇔ (P = true)
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Relate negation to equality with the boolean value false.
theorem eq_false: all P:bool. not P ⇔ P = false
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

// Convert a logical iff into boolean equality.
theorem iff_equal: all P:bool, Q:bool.
  if (P ⇔ Q)  
  then P = Q
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true {
      suppose q
      simplify with q.
    }
    case false {
      suppose not_q
      simplify with not_q.
    }
  }
end

theorem iff_symm: all P:bool, Q:bool.
  if (P ⇔ Q) then (Q ⇔ P)
proof
  arbitrary P:bool, Q:bool
  assume: P ⇔ Q
  have fwd: if Q then P by assume: Q apply (recall P ⇔ Q) to (recall Q)
  have bkwd: if P then Q by assume: P apply (recall P ⇔ Q) to (recall P)
  fwd, bkwd
end

theorem iff_trans: all P:bool, Q:bool, R:bool.
  if (P ⇔ Q) and (Q ⇔ R) then (P ⇔ R)
proof
  arbitrary P:bool, Q:bool, R:bool
  assume prem: (P ⇔ Q) and (Q ⇔ R)
  have fwd: if P then R by {
    assume: P
    have: Q by apply prem to recall P
    conclude R by apply prem to recall Q
  }
  have bkwd: if R then P by {
    assume: R
    have: Q by apply prem to recall R
    conclude P by apply prem to recall Q
  }
  fwd, bkwd
end

// Reflexivity of iff.
theorem iff_refl: all P:bool. P ⇔ P
proof
  arbitrary P:bool
  have fwd: if P then P by { assume p p }
  fwd, fwd
end

theorem contrapositive: all P : bool, Q : bool.
  if (if P then Q) and not Q then not P
proof
  arbitrary P : bool, Q : bool
  switch Q {
    case true { . }
    case false { . }
  }
end

// Reflexivity of implication.
theorem implies_refl: all P:bool. if P then P
proof
  arbitrary P:bool
  assume p
  p
end

// Transitivity of implication.
theorem implies_trans: all P:bool, Q:bool, R:bool.
  if (if P then Q) and (if Q then R) then (if P then R)
proof
  arbitrary P:bool, Q:bool, R:bool
  assume prem
  assume p
  have q: Q by apply (conjunct 0 of prem) to p
  apply (conjunct 1 of prem) to q
end

// Modus ponens as a theorem (operationally available via `apply ... to ...`).
theorem modus_ponens: all P:bool, Q:bool.
  if (if P then Q) and P then Q
proof
  arbitrary P:bool, Q:bool
  assume prem
  apply (conjunct 0 of prem) to (conjunct 1 of prem)
end

theorem double_neg: all P: bool.
  (not (not P)) = P
proof
  arbitrary P:bool
  switch P {
    case true {
      evaluate
    }
    case false {
      evaluate
    }
  }
end

fun xor(x : bool, y : bool) {
  if x then not y
  else y
}

theorem xor_true: all b:bool. xor(true, b) = not b
proof
  arbitrary b:bool
  switch b {
    case true {
      evaluate
    }
    case false {
      evaluate
    }
  }
end

theorem xor_false: all b:bool. xor(false, b) = b
proof
  arbitrary b:bool
  switch b {
    case true { evaluate }
    case false { evaluate }
  }
end

theorem xor_commute: all a:bool, b:bool. xor(a,b) = xor(b,a)
proof
  arbitrary a:bool, b:bool
  switch a {
    case true {
      switch b {
        case true { evaluate }
        case false { evaluate }
      }
    }
    case false {
      switch b {
        case true { evaluate }
        case false { evaluate }
      }
    }
  }
end

// xor of a value with itself is false.
theorem xor_self: all a:bool. xor(a, a) = false
proof
  arbitrary a:bool
  switch a {
    case true { evaluate }
    case false { evaluate }
  }
end

// xor of a value with its negation is true.
theorem xor_neg: all a:bool. xor(a, not a) = true
proof
  arbitrary a:bool
  switch a {
    case true { evaluate }
    case false { evaluate }
  }
end

// xor is associative.
theorem xor_assoc: all a:bool, b:bool, c:bool.
  xor(a, xor(b, c)) = xor(xor(a, b), c)
proof
  arbitrary a:bool, b:bool, c:bool
  switch a {
    case true {
      switch b {
        case true {
          switch c {
            case true { evaluate }
            case false { evaluate }
          }
        }
        case false {
          switch c {
            case true { evaluate }
            case false { evaluate }
          }
        }
      }
    }
    case false {
      switch b {
        case true {
          switch c {
            case true { evaluate }
            case false { evaluate }
          }
        }
        case false {
          switch c {
            case true { evaluate }
            case false { evaluate }
          }
        }
      }
    }
  }
end