Skip to content

Commit 2002920

Browse files
JovanGerbJovanGerb
committed
feat: don't delaborate to ⊔ or ⊓ if we have a LinearOrder (#23558)
This PR changes the `⊔` and `⊓` notations to only be used by the delaborator if the type in question is not a linear order. This was suggested here [#mathlib4 > max and min delaborators @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/max.20and.20min.20delaborators/near/500701449)
1 parent 72dd74b commit 2002920

File tree

3 files changed

+162
-9
lines changed

3 files changed

+162
-9
lines changed

‎Mathlib/Lean/PrettyPrinter/Delaborator.lean‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ import Lean.PrettyPrinter.Delaborator.Basic
1212

1313
namespace Lean.PrettyPrinter.Delaborator
1414

15-
open Lean.Meta Lean.SubExpr SubExpr
15+
open SubExpr
1616

1717
/-- Assuming the current expression in a lambda or pi,
1818
descend into the body using an unused name generated from the binder's name.
@@ -31,4 +31,17 @@ def OptionsPerPos.setBool (opts : OptionsPerPos) (p : SubExpr.Pos) (n : Name) (v
3131
let e := opts.findD p {} |>.setBool n v
3232
opts.insert p e
3333

34+
/-- Annotates `stx` with the go-to-def information of `target`. -/
35+
def annotateGoToDef (stx : Term) (target : Name) : DelabM Term := do
36+
let module := (← findModuleOf? target).getD (← getEnv).mainModule
37+
let some range ← findDeclarationRanges? target | return stx
38+
let stx ← annotateCurPos stx
39+
let location := { module, range := range.selectionRange }
40+
addDelabTermInfo (← getPos) stx (← getExpr) (location? := some location)
41+
return stx
42+
43+
/-- Annotates `stx` with the go-to-def information of the notation used in `stx`. -/
44+
def annotateGoToSyntaxDef (stx : Term) : DelabM Term := do
45+
annotateGoToDef stx stx.raw.getKind
46+
3447
end Lean.PrettyPrinter.Delaborator

‎Mathlib/Order/Notation.lean‎

Lines changed: 84 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Yury Kudryashov, Yaël Dillies
55
-/
6+
import Qq
7+
import Mathlib.Lean.PrettyPrinter.Delaborator
68
import Mathlib.Tactic.TypeStar
79
import Mathlib.Tactic.Simps.NotationClass
810

@@ -13,17 +15,22 @@ In this file we introduce typeclasses and definitions for lattice operations.
1315
1416
## Main definitions
1517
16-
* the `⊔` notation is used for `Max` since November 2024
17-
* the `⊓` notation is used for `Min` since November 2024
1818
* `HasCompl`: type class for the `ᶜ` notation
1919
* `Top`: type class for the `⊤` notation
2020
* `Bot`: type class for the `⊥` notation
2121
2222
## Notations
2323
24-
* `x ⊔ y`: lattice join operation;
25-
* `x ⊓ y`: lattice meet operation;
2624
* `xᶜ`: complement in a lattice;
25+
* `x ⊔ y`: supremum/join, which is notation for `max x y`;
26+
* `x ⊓ y`: infimum/meet, which is notation for `min x y`;
27+
28+
We implement a delaborator that pretty prints `max x y`/`min x y` as `x ⊔ y`/`x ⊓ y`
29+
if and only if the order on `α` does not have a `LinearOrder α` instance (where `x y : α`).
30+
31+
This is so that in a lattice we can use the same underlying constants `max`/`min`
32+
as in linear orders, while using the more idiomatic notation `x ⊔ y`/`x ⊓ y`.
33+
Lemmas about the operators `⊔` and `⊓` should use the names `sup` and `inf` respectively.
2734
2835
-/
2936

@@ -54,11 +61,80 @@ class Inf (α : Type*) where
5461

5562
attribute [ext] Min Max
5663

57-
@[inherit_doc]
58-
infixl:68 " ⊔ " => Max.max
64+
/--
65+
The supremum/join operation: `x ⊔ y`. It is notation for `max x y`
66+
and should be used when the type is not a linear order.
67+
-/
68+
syntax:68 term:68 " ⊔ " term:69 : term
5969

60-
@[inherit_doc]
61-
infixl:69 " ⊓ " => Min.min
70+
/--
71+
The infimum/meet operation: `x ⊓ y`. It is notation for `min x y`
72+
and should be used when the type is not a linear order.
73+
-/
74+
syntax:69 term:69 " ⊓ " term:70 : term
75+
76+
macro_rules
77+
| `($a ⊔ $b) => `(Max.max $a $b)
78+
| `($a ⊓ $b) => `(Min.min $a $b)
79+
80+
namespace Mathlib.Meta
81+
82+
open Lean Meta PrettyPrinter Delaborator SubExpr Qq
83+
84+
-- irreducible to not confuse Qq
85+
@[irreducible] private def linearOrderExpr (u : Level) : Q(Type u → Type u) :=
86+
.const `LinearOrder [u]
87+
private def linearOrderToMax (u : Level) : Q((a : Type u) → $(linearOrderExpr u) a → Max a) :=
88+
.const `LinearOrder.toMax [u]
89+
private def linearOrderToMin (u : Level) : Q((a : Type u) → $(linearOrderExpr u) a → Min a) :=
90+
.const `LinearOrder.toMin [u]
91+
92+
/--
93+
Return `true` if `LinearOrder` is imported and `inst` comes from a `LinearOrder e` instance.
94+
95+
We use a `try catch` block to make sure there are no surprising errors during delaboration.
96+
-/
97+
private def hasLinearOrder (u : Level) (α : Q(Type u)) (cls : Q(Type u → Type u))
98+
(toCls : Q((α : Type u) → $(linearOrderExpr u) α → $cls α)) (inst : Q($cls $α)) :
99+
MetaM Bool := do
100+
try
101+
withNewMCtxDepth do
102+
-- `isDefEq` may call type class search to instantiate `mvar`, so we need the local instances
103+
-- In Lean 4.19 the pretty printer clears local instances, so we re-add them here.
104+
-- TODO(Jovan): remove
105+
withLocalInstances (← getLCtx).decls.toList.reduceOption do
106+
let mvar ← mkFreshExprMVarQ q($(linearOrderExpr u) $α) (kind := .synthetic)
107+
let inst' : Q($cls $α) := q($toCls $α $mvar)
108+
isDefEq inst inst'
109+
catch _ =>
110+
-- For instance, if `LinearOrder` is not yet imported.
111+
return false
112+
113+
/-- Delaborate `max x y` into `x ⊔ y` if the type is not a linear order. -/
114+
@[delab app.Max.max]
115+
def delabSup : Delab := do
116+
let_expr f@Max.max α inst _ _ := ← getExpr | failure
117+
have u := f.constLevels![0]!
118+
if ← hasLinearOrder u α q(Max) q($(linearOrderToMax u)) inst then
119+
failure -- use the default delaborator
120+
let x ← withNaryArg 2 delab
121+
let y ← withNaryArg 3 delab
122+
let stx ← `($x ⊔ $y)
123+
annotateGoToSyntaxDef stx
124+
125+
/-- Delaborate `min x y` into `x ⊓ y` if the type is not a linear order. -/
126+
@[delab app.Min.min]
127+
def delabInf : Delab := do
128+
let_expr f@Min.min α inst _ _ := ← getExpr | failure
129+
have u := f.constLevels![0]!
130+
if ← hasLinearOrder u α q(Min) q($(linearOrderToMin u)) inst then
131+
failure -- use the default delaborator
132+
let x ← withNaryArg 2 delab
133+
let y ← withNaryArg 3 delab
134+
let stx ← `($x ⊓ $y)
135+
annotateGoToSyntaxDef stx
136+
137+
end Mathlib.Meta
62138

63139
/-- Syntax typeclass for Heyting implication `⇨`. -/
64140
@[notation_class]

‎MathlibTest/Delab/SupInf.lean‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
import Mathlib
2+
3+
4+
/-- info: max 1 2 : ℕ -/
5+
#guard_msgs in
6+
#check max (1 : ℕ) 2
7+
8+
/-- info: max 1 2 : ℝ -/
9+
#guard_msgs in
10+
#check max (1 : ℝ) 2
11+
12+
/-- info: ({0} ⊔ {1} ⊔ ({2} ⊔ {3})) ⊓ ({4} ⊔ {5}) ⊔ {6} ⊓ {7} ⊓ ({8} ⊓ {9}) : Set ℕ -/
13+
#guard_msgs in
14+
#check (max (min (max (max {0} {1}) (max {2} {3})) (max {4} {5})) (min (min {6} {7}) (min {8} {9})) : Set ℕ)
15+
16+
17+
section
18+
19+
variable {α : Type*} (a b : α)
20+
21+
variable [Lattice α] in
22+
/-- info: a ⊔ b : α -/
23+
#guard_msgs in
24+
#check max a b
25+
26+
variable [LinearOrder α] in
27+
/-- info: max a b : α -/
28+
#guard_msgs in
29+
#check max a b
30+
31+
variable [CompleteLinearOrder α] in
32+
/-- info: max a b : α -/
33+
#guard_msgs in
34+
#check max a b
35+
36+
variable [ConditionallyCompleteLinearOrder α] in
37+
/-- info: max a b : α -/
38+
#guard_msgs in
39+
#check max a b
40+
41+
end
42+
43+
universe u
44+
45+
/-- info: fun α [Lattice α] a b => a ⊔ b : (α : Type u) → [inst : Lattice α] → α → α → α -/
46+
#guard_msgs in
47+
#check fun (α : Type u) [Lattice α] (a b : α) => max a b
48+
49+
/-- info: fun α [LinearOrder α] a b => max a b : (α : Type u) → [inst : LinearOrder α] → α → α → α -/
50+
#guard_msgs in
51+
#check fun (α : Type u) [LinearOrder α] (a b : α) => max a b
52+
53+
/--
54+
info: fun α [CompleteLinearOrder α] a b => max a b : (α : Type u) → [inst : CompleteLinearOrder α] → α → α → α
55+
-/
56+
#guard_msgs in
57+
#check fun (α : Type u) [CompleteLinearOrder α] (a b : α) => max a b
58+
59+
/--
60+
info: fun α [ConditionallyCompleteLinearOrder α] a b =>
61+
max a b : (α : Type u) → [inst : ConditionallyCompleteLinearOrder α] → α → α → α
62+
-/
63+
#guard_msgs in
64+
#check fun (α : Type u) [ConditionallyCompleteLinearOrder α] (a b : α) => max a b

0 commit comments

Comments
 (0)