eqCost_self

formal source

  44def eqCost {K : Type u} [DecidableEq K] (a b : K) : Nat :=
  45  if a = b then 0 else 1
  46
  47theorem eqCost_self {K : Type u} [DecidableEq K] (a : K) :
  48    eqCost a a = 0 := by
  49  simp [eqCost]
  50
  51theorem eqCost_symm {K : Type u} [DecidableEq K] (a b : K) :
  52    eqCost a b = eqCost b a := by
  53  unfold eqCost
  54  by_cases h : a = b
  55  · subst h
  56    simp
  57  · have hba : ¬ b = a := fun hb => h hb.symm
  58    simp [h, hba]
  59
  60theorem eqCost_ne_one {K : Type u} [DecidableEq K] {a b : K} (h : a ≠ b) :
  61    eqCost a b = 1 := by
  62  simp [eqCost, h]
  63
  64/-! ## Instantiating `LogicRealization` on K -/
  65
  66/-- The canonical interpretation of a lifted `LogicNat` into a carrier with a
  67named base point `x` and a named distinct point `y`: zero maps to `x`, every
  68successor maps to `y`. The `ULift` lets the orbit live in the same universe as
  69the arbitrary carrier. -/
  70def distinctionInterpret {K : Type u} (x y : K) : ULift.{u} LogicNat → K
  71  | ⟨LogicNat.identity⟩ => x
  72  | ⟨LogicNat.step _⟩ => y
  73
  74/-- The step map induced by a single distinction: every state advances to the
  75distinguished second point. This gives a total endomap on `K`. -/
  76def distinctionStep {K : Type u} (_x y : K) : K → K :=
  77  fun _ => y