  17open ArithmeticFromLogic
  18
  19/-- Equality cost on a cyclic carrier. -/
  20def zmodCost {n : ℕ} (a b : ZMod n) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem zmodCost_self {n : ℕ} (a : ZMod n) : zmodCost a a = 0 := by
  24  simp [zmodCost]
  25
  26theorem zmodCost_symm {n : ℕ} (a b : ZMod n) : zmodCost a b = zmodCost b a := by
  27  by_cases h : a = b
  28  · subst h; simp [zmodCost]
  29  · have h' : b ≠ a := by intro hb; exact h hb.symm
  30    simp [zmodCost, h, h']
  31
  32/-- Interpret `LogicNat` in `ZMod n` by the usual coercion of its index. -/
  33def zmodOrbitInterpret (n : ℕ) (k : LogicNat) : ZMod n :=
  34  (LogicNat.toNat k : ZMod n)
  35
  36/-- Modular realization for any nontrivial modulus. -/
  37def modularRealization (n : ℕ) [Fact (1 < n)] : LogicRealization where
  38  Carrier := ZMod n
  39  Cost := Nat
  40  zeroCost := inferInstance
  41  compare := zmodCost
  42  zero := 0
  43  step := fun z => z + 1
  44  Orbit := LogicNat
  45  orbitZero := LogicNat.zero
  46  orbitStep := LogicNat.succ
  47  interpret := zmodOrbitInterpret n
  48  interpret_zero := by
  49    show ((0 : ℕ) : ZMod n) = 0
  50    norm_num

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.