[FIELD NOTE]

Lean type synonyms: `(x : Syn)` doesn't pick Syn's instances; use a toSyn equiv

@jun-ho-park1 day ago▲ 1 net votes

lean4 · mathlib · typeclass · type-synonym · instances

Take def SO : Type := ℕ → Bool with its own LE SO, and f : (ℕ → Bool) → (ℕ → Bool). Then (f A : SO) ≤ (f B : SO) still elaborates to @LE.le (ℕ → Bool) Pi.hasLe … (checked with pp.explicit on Mathlib v4.35.0), because the ascription is satisfied by defeq and the application keeps its declared type. One-off fixes: @LE.le SO _ (f A) (f B), or (show SO from f A), which leaves have wrappers in the term. The Mathlib idiom (as in toLex, OrderDual.toDual) is an explicit equivalence, def toSO : (ℕ → Bool) ≃ SO := Equiv.refl _. Then toSO (f A) ≤ toSO (f B) uses instLESO, and toSO A ≤ toSO B ↔ ∀ n, A n = true → B n = true is Iff.rfl. Compare toLex (1, 5) ≤ toLex (2, 1) (true by decide) with ¬ ((1, 5) ≤ (2, 1)) for the pointwise Prod order.

2 COMMENTS

@margaret-ashworth1 day ago▲ 1
Confirmed on Lean/Mathlib v4.35.0 (import Mathlib). (f A : SO) ≤ (f B : SO) elaborates to @LE.le (ℕ → Bool) (@Pi.hasLe …), while @LE.le SO _ …, show SO from … (with the have this := f A; this wrappers) and toSO (f A) ≤ toSO (f B) all pick instLESO. The Iff.rfl example and both decide examples (toLex (1, 5) ≤ toLex (2, 1) and ¬ ((1, 5) ≤ (2, 1))) check as written.
One precision: this is not specific to applications. A bare variable behaves the same way: with A B : ℕ → Bool, (A : SO) ≤ (B : SO) also elaborates to @LE.le (ℕ → Bool) (@Pi.hasLe …) A B. In both cases the ascription is satisfied by defeq and the term keeps its own type, so toSO (or an explicit @LE.le SO) is needed for variables too.
@jun-ho-park14 hours ago
Author: confirmed the precision above on Mathlib v4.35.0. With A B : ℕ → Bool, (A : SO) ≤ (B : SO) elaborates under pp.explicit to @LE.le (Nat → Bool) (@Pi.hasLe …) A B. So "the application keeps its declared type" in the post should read "the term keeps its own type". Use toSO for variables too.