Distinction

formal source

  57/-- A **distinction predicate** on a carrier `K` is a binary predicate
  58that detects whether two elements are distinguishable. The canonical
  59example is the equality test, available on any type. -/
  60def Distinction (K : Type*) : Type _ := K → K → Prop
  61
  62/-- The canonical distinction induced by equality: two elements are
  63distinct iff they are not equal. This is the most primitive distinction
  64on any type and exists for every type without further structure. -/
  65def equalityDistinction (K : Type*) : Distinction K :=
  66  fun x y => x ≠ y
  67
  68/-- Reflexivity of the canonical distinction: an element is not distinct
  69from itself. This is reflexivity of equality, a definitional fact of any
  70type theory. -/
  71theorem equalityDistinction_irrefl (K : Type*) :
  72    ∀ x : K, ¬ equalityDistinction K x x := by
  73  intro x h
  74  exact h rfl
  75
  76/-- Symmetry of the canonical distinction: distinguishability does not
  77depend on argument order. This is symmetry of disequality, derived from
  78the symmetric definition of equality. -/
  79theorem equalityDistinction_symm (K : Type*) :
  80    ∀ x y : K, equalityDistinction K x y ↔ equalityDistinction K y x := by
  81  intro x y
  82  unfold equalityDistinction
  83  exact ⟨fun h heq => h heq.symm, fun h heq => h heq.symm⟩
  84
  85/-! ## The Equality-Induced Cost -/
  86
  87/-- The **canonical cost induced by equality**: assigns 0 to identical
  88pairs and a positive weight to distinct pairs. This is a function on
  89pairs whose form is determined entirely by the equality predicate. -/
  90noncomputable def equalityCost (K : Type*) (weight : ℝ) : K → K → ℝ :=