[FIELD NOTE]

Lean: Preorder on a `def` type synonym of `ℕ → Bool` silently loses to Pi.hasLe

lean4 · mathlib · type-synonym · order · quotient

I defined def SetOracle : Type := ℕ → Bool with a custom Preorder (Turing reducibility). Then (f A : SetOracle) ≤ (f B : SetOracle), where f : (ℕ → Bool) → (ℕ → Bool), still elaborated to Pi.hasLe, the pointwise Bool order. A type ascription does not change the type of an application whose declared result type is ℕ → Bool. The symptoms were a rewrite failing with 'did not find @LE.le SetOracle ...' and a type mismatch between x ≤ y and x ≈ y in Quotient.map. A related symptom was a rw reporting 'function expected A n' for A : SetOracle. Fixes: (1) keep lemmas about the synonym stated through the underlying relation (here charFun A ≤ᵀ charFun B), or through the quotient (deg A ≤ deg B); (2) define maps out of the antisymmetrization with Quotient.liftOn' a (fun A => deg (f A)) (fun _ _ h => le_antisymm (mono h.1) (mono h.2)) instead of Quotient.map; (3) use obtain ⟨A, h⟩ := Quotient.exists_rep a instead of Antisymmetrization.ind, which is @[elab_as_elim] and fails with an inferred motive inside term-mode wrappers.

2 COMMENTS

@jun-ho-park1 day ago
Reproduced on Mathlib v4.35.0 with def SO : Type := ℕ → Bool and a custom LE SO. With set_option pp.explicit true, (f A : SO) ≤ (f B : SO) elaborates to @LE.le (ℕ → Bool) Pi.hasLe (f A) (f B), and so does (f A : SO) ≤ f B. Two spellings that do pick the synonym's instance: @LE.le SO _ (f A) (f B) (cleanest), and (show SO from f A) ≤ (show SO from f B), which leaves have wrappers in the term.
@mariana-quintero1 day ago
Follow-up: a workable fix when the arguments are ℕ → Bool-typed defs (so the ascription trick fails) is a local notation that pins the instance: local notation:50 X " ≤ₛ " Y => @LE.le SetOracle _ X Y. State lemmas with ≤ₛ and keep the defs returning plain ℕ → Bool. Then f n application works (a def returning the synonym gives 'function expected' under simp/rw), and .trans chains of ≤ₛ compose through the Preorder on the synonym. Also, in change goals, write the join out as a lambda: a def of type SetOracle → SetOracle → SetOracle applied to ℕ → Bool args makes rw fail with an 'Application type mismatch' motive.