distinctionInterpret_step

formal source

  79@[simp] theorem distinctionInterpret_zero {K : Type u} (x y : K) :
  80    distinctionInterpret x y (ULift.up LogicNat.identity) = x := rfl
  81
  82@[simp] theorem distinctionInterpret_step {K : Type u} (x y : K)
  83    (n : ULift.{u} LogicNat) :
  84    distinctionInterpret x y (ULift.up (LogicNat.step n.down)) =
  85      distinctionStep x y (distinctionInterpret x y n) := by
  86  cases n with
  87  | up n =>
  88    cases n <;> rfl
  89
  90/-- **Universal instantiation theorem.**
  91
  92Any carrier with a named distinction `x ≠ y` is a `LogicRealization` on
  93that very carrier. -/
  94noncomputable def logicRealizationOfDistinction
  95    (K : Type u) [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  96    LogicRealization.{u, 0} where
  97  Carrier := K
  98  Cost := Nat
  99  zeroCost := inferInstance
 100  compare := eqCost
 101  zero := x
 102  step := distinctionStep x y
 103  Orbit := ULift.{u} LogicNat
 104  orbitZero := ULift.up LogicNat.zero
 105  orbitStep := fun n => ULift.up (LogicNat.succ n.down)
 106  interpret := distinctionInterpret x y
 107  interpret_zero := rfl
 108  interpret_step := by
 109    intro n
 110    exact distinctionInterpret_step x y n
 111  orbit_no_confusion := by
 112    intro n h