boolCost

formal source

  12namespace DiscreteLogicRealization
  13
  14/-- Boolean comparison cost: zero for equality, one for distinction. -/
  15def boolCost (p q : Bool) : Nat :=
  16  if p = q then 0 else 1
  17
  18@[simp] theorem boolCost_self (p : Bool) : boolCost p p = 0 := by
  19  simp [boolCost]
  20
  21theorem boolCost_symm (p q : Bool) : boolCost p q = boolCost q p := by
  22  by_cases h : p = q
  23  · subst h
  24    simp [boolCost]
  25  · have h' : q ≠ p := by intro hqp; exact h hqp.symm
  26    simp [boolCost, h, h']
  27
  28/-- Interpret the free step orbit in the Boolean carrier by parity. -/
  29def boolOrbitInterpret : ArithmeticFromLogic.LogicNat → Bool
  30  | ArithmeticFromLogic.LogicNat.identity => false
  31  | ArithmeticFromLogic.LogicNat.step n => Bool.not (boolOrbitInterpret n)
  32
  33/-- The discrete propositional Law-of-Logic realization. -/
  34def boolRealization : LogicRealization where
  35  Carrier := Bool
  36  Cost := Nat
  37  zeroCost := inferInstance
  38  compare := boolCost
  39  zero := false
  40  step := Bool.not
  41  Orbit := ArithmeticFromLogic.LogicNat
  42  orbitZero := ArithmeticFromLogic.LogicNat.zero
  43  orbitStep := ArithmeticFromLogic.LogicNat.succ
  44  interpret := boolOrbitInterpret
  45  interpret_zero := rfl