Example for sorting pairs with custom comparator

Changes

1 changed files (+21/-0)

• Sort.lean
  • @@ -75,3 +75,24 @@ theorem sorted : ICan'tBelieveItCanSort.{0} A |>.Pairwise (· ≤ ·) := by
    theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A ∧ (ICan'tBelieveItCanSort.{0} A).Pairwise (· ≤ ·) := ⟨perm A, sorted A⟩ + + -- Not sure why this needs so much boilerplate + @[reducible] + def le (a : (ℕ × String)) (b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) + + instance : LE (ℕ × String) where le := le + + instance {a : (ℕ × String)} {b : (ℕ × String)} : Decidable (a ≤ b) := + inferInstanceAs (Decidable (le a b)) + + @[grind] + lemma le_def {a : (ℕ × String)} {b : (ℕ × String)} : a ≤ b ↔ le a b := .rfl + + instance : LinearOrder (ℕ × String) where + le_refl := by grind + le_trans := by grind + le_antisymm := by grind + le_total := by grind + toDecidableLE := inferInstanceAs _ + + #eval ICan'tBelieveItCanSort #[(69, "hi"), (1729, "blah"), (13, "a"), (420, "a"), (420, "meow")]