hand-written-dual

A Lean theorem that states another's order dual, written by hand.

Group

Lean proofs

Runs

Optional: run it with ur lint --rule hand-written-dual

Level

warning

Reads

Every file

Fix

None: whether to generate the dual or keep it is the author's to decide

Why

The two theorems state each other's order dual: reversing every ≤ and < of one, exchanging ⊔ and ⊓, ⊤ and ⊥, and ⨆ and ⨅, and translating the names it reads with Mathlib's dual dictionary, as le_sup_left becomes inf_le_left, gives the other. Mathlib's @[to_dual] attribute generates a theorem's dual, or with existing records that one is the other's, so the pair need not be proved, named, and kept in step twice. Only theorems about an order are compared: those that assume an order class, such as Preorder or SemilatticeSup, and no class but those and classes that say nothing of an order, since @[to_dual] makes no dual of a statement about ℝ or an ordered ring. Ur does not elaborate, so a constant whose dual the dictionary guesses wrongly, or that has no dual, can join a pair that @[to_dual] would not make.

The fix, as Ur suggests it: add @[to_dual] to the first theorem and delete the second, or @[to_dual existing] to keep both.

For agents

State a Lean theorem about an order once and generate its order dual with @[to_dual], or mark the dual with @[to_dual existing].

theorem le_sup_of_le_left' {α : Type*} [SemilatticeSup α] {a b c : α}
    (h : c ≤ a) : c ≤ a ⊔ b :=
  le_trans h le_sup_left

theorem inf_le_of_le_left' {α : Type*} [SemilatticeInf α] {a b c : α}
    (h : a ≤ c) : a ⊓ b ≤ c :=
  le_trans inf_le_left h

$ ur lint --rule hand-written-dual
warning[hand-written-dual]: `inf_le_of_le_left'` states the order dual of `le_sup_of_le_left'`, which `@[to_dual]` can generate
  --> ./Order.lean:5:9-6 `inf_le_of_le_left'`
  --> ./Order.lean:1:9-2 `le_sup_of_le_left'`
  = assumes: names-resolve-alike
  = hint: add `@[to_dual]` to the first theorem and delete the second, or `@[to_dual existing]` to keep both
0 clone classes and 1 proof finding in 1 file