IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean
   2
   3/-!
   4  Strict/Ordered.lean
   5
   6  Strict ordered realization on `ℤ` with equality cost and unit translation.
   7-/
   8
   9namespace IndisputableMonolith
  10namespace Foundation
  11namespace UniversalForcing
  12namespace Strict
  13namespace Ordered
  14
  15def intCost (a b : ℤ) : Nat :=
  16  if a = b then 0 else 1
  17
  18@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
  19  simp [intCost]
  20
  21theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  22  by_cases h : a = b
  23  · subst h
  24    simp [intCost]
  25  · have h' : b ≠ a := by intro hb; exact h hb.symm
  26    simp [intCost, h, h']
  27
  28/-- Strict ordered integer realization. -/
  29def strictOrderedRealization : StrictLogicRealization where
  30  Carrier := ℤ
  31  Cost := Nat
  32  zeroCost := inferInstance
  33  compare := intCost
  34  compose := fun a b => a + b
  35  one := 0
  36  generator := 1
  37  identity_law := intCost_self
  38  non_contradiction_law := intCost_symm
  39  excluded_middle_law := True
  40  composition_law := True
  41  invariance_law := True
  42  nontrivial_law := by
  43    simp [intCost]
  44
  45def strictOrdered_arith_equiv_logicNat :
  46    (StrictLogicRealization.arith strictOrderedRealization).peano.carrier
  47      ≃ ArithmeticFromLogic.LogicNat :=
  48  (StrictLogicRealization.toLightweight strictOrderedRealization).orbitEquivLogicNat
  49
  50end Ordered
  51end Strict
  52end UniversalForcing
  53end Foundation
  54end IndisputableMonolith
  55