Skip to content

Commit c07cc9e

Browse files
timotree3timotree3
committed
fix(DiscrTree): remove special handling of numerals
Fixes #2867 by removing special handling of `OfNat.ofNat` numerals from `DiscrTree`. The special handling was added in 2b8e55c to fix a bug represented in the test `tests/lean/run/bugNatLitDiscrTree.lean`, but with #2916 fixed, that test case passes without the special handling. Some special handling of `Nat.zero` and `Nat.succ` remains.
1 parent e61d082 commit c07cc9e

File tree

2 files changed

+168
-30
lines changed

2 files changed

+168
-30
lines changed

‎src/Lean/Meta/DiscrTree.lean

+24-30
Original file line numberDiff line numberDiff line change
@@ -198,30 +198,27 @@ private partial def isNumeral (e : Expr) : Bool :=
198198
else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
199199
else false
200200

201-
private partial def toNatLit? (e : Expr) : Option Literal :=
202-
if isNumeral e then
203-
if let some n := loop e then
204-
some (.natVal n)
205-
else
206-
none
201+
/-- Returns `some k` if `e` consists of `Nat.zero` followed by `k` applications of `Nat.succ`.-/
202+
private partial def natConst? (e : Expr) : Option Nat :=
203+
match_expr e with
204+
| Nat.zero => some 0
205+
| Nat.succ e' => (· + 1) <$> natConst? e'
206+
| _ => none
207+
208+
/-- If `e` consists of `Nat.zero` followed by `k` applications of `Nat.succ`,
209+
returns `OfNat.ofNat (nat_lit k)`. Otherwise, returns `e` unchanged.
210+
211+
Remark:
212+
We need to ensure that `Nat.zero` and `0` (i.e. `OfNat.ofNat (nat_lit 0)`) are keyed the same way
213+
because unification sometimes converts the former into the latter.
214+
215+
For example, the unification problem `Nat.zero =?= ?n + 0` is resolved by setting `?n := 0`,
216+
*not* `?n := Nat.zero`-/
217+
private def normalizeNatConst (e : Expr) : Expr :=
218+
if let some n := natConst? e then
219+
mkNatLit n
207220
else
208-
none
209-
where
210-
loop (e : Expr) : OptionT Id Nat := do
211-
let f := e.getAppFn
212-
match f with
213-
| .lit (.natVal n) => return n
214-
| .const fName .. =>
215-
if fName == ``Nat.succ && e.getAppNumArgs == 1 then
216-
let r ← loop e.appArg!
217-
return r+1
218-
else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
219-
loop (e.getArg! 1)
220-
else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
221-
return 0
222-
else
223-
failure
224-
| _ => failure
221+
e
225222

226223
private def isNatType (e : Expr) : MetaM Bool :=
227224
return (← whnf e).isConstOf ``Nat
@@ -310,7 +307,10 @@ where
310307

311308
/-- whnf for the discrimination tree module -/
312309
def reduceDT (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM Expr :=
313-
if root then reduceUntilBadKey e config else reduce e config
310+
if root then
311+
reduceUntilBadKey e config
312+
else
313+
normalizeNatConst <$> reduce e config
314314

315315
/- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
316316

@@ -350,8 +350,6 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
350350
return (.lit v, todo)
351351
| .const c _ =>
352352
unless root do
353-
if let some v := toNatLit? e then
354-
return (.lit v, todo)
355353
if (← shouldAddAsStar c e) then
356354
return (.star, todo)
357355
let nargs := e.getAppNumArgs
@@ -468,10 +466,6 @@ def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : W
468466

469467
private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
470468
let e ← reduceDT e root config
471-
unless root do
472-
-- See pushArgs
473-
if let some v := toNatLit? e then
474-
return (.lit v, #[])
475469
match e.getAppFn with
476470
| .lit v => return (.lit v, #[])
477471
| .const c _ =>

‎tests/lean/run/discrTreeNumeral.lean

+144
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
/-!
2+
# Simp lemmas can match numerals and constant offsets
3+
-/
4+
5+
def MyProp (_ : Nat) : Prop := True
6+
7+
variable (n : Nat)
8+
9+
theorem myProp_zero : MyProp 0 = True := rfl
10+
theorem myProp_add_one : MyProp (n + 1) = True := rfl
11+
theorem myProp_ofNat : MyProp (OfNat.ofNat n) = True := rfl
12+
theorem myProp_ofNat_add_one : MyProp (OfNat.ofNat (n + 1)) = True := rfl
13+
14+
/-- Lemmas about a specific numeral match that numeral. -/
15+
example : MyProp 0 := by
16+
dsimp only [myProp_zero]
17+
18+
/-- Lemmas about all numerals match a specific numeral.
19+
20+
(Regression test for https://github.com/leanprover/lean4/issues/2867)-/
21+
example : MyProp 0 := by
22+
dsimp only [myProp_ofNat]
23+
24+
/-- Lemmas about any natural number plus a constant offset match their left-hand side. -/
25+
example : MyProp (n + 1) := by
26+
dsimp only [myProp_add_one]
27+
28+
/-- Lemmas about any natural number plus a constant offset match a larger offset. -/
29+
example : MyProp (n + 2) := by
30+
dsimp only [myProp_add_one]
31+
32+
/-- Lemmas about any natural number plus a constant offset match the constant offset. -/
33+
example : MyProp 1 := by
34+
dsimp only [myProp_add_one]
35+
36+
/-- Lemmas about any natural number plus a constant offset match constants exceeding the offset. -/
37+
example : MyProp 2 := by
38+
dsimp only [myProp_add_one]
39+
40+
/-- Lemmas about numerals that express a lower-bound
41+
through a constant offset match their left-hand side.-/
42+
example : MyProp (OfNat.ofNat (n + 1)) := by
43+
dsimp only [myProp_ofNat_add_one]
44+
45+
/-- Lemmas about numerals that express a lower-bound
46+
through a constant offset match a larger offset.-/
47+
example : MyProp (OfNat.ofNat (n + 2)) := by
48+
dsimp only [myProp_ofNat_add_one]
49+
50+
/-- Lemmas about numerals that express a lower-bound
51+
through a constant offset match the constant offset.-/
52+
example : MyProp 1 := by
53+
dsimp only [myProp_ofNat_add_one]
54+
55+
/-- Lemmas about numerals that express a lower-bound
56+
through a constant offset match numerals exceeding the constant offset.-/
57+
example : MyProp 2 := by
58+
dsimp only [myProp_ofNat_add_one]
59+
60+
/-- Lemmas about `0` match `Nat.zero` since `Nat.zero = 0` is in the default simp set.-/
61+
example : MyProp Nat.zero := by
62+
dsimp [myProp_zero]
63+
64+
/-- Lemmas about `0` match `nat_lit 0` since `nat_lit 0 = 0` is in the default simp set.-/
65+
example : MyProp (nat_lit 0) := by
66+
dsimp [myProp_zero]
67+
68+
/-- Lemmas about any natural number plus a constant offset match their LHS in terms of `Nat.succ`
69+
since `Nat.succ n = n + 1` is in the default simp set. -/
70+
example : MyProp (Nat.succ n) := by
71+
dsimp [myProp_add_one]
72+
73+
/-- If a general lemma about numerals is specialized to a particular one, it still applies.
74+
75+
This is a tricky case because it results in nested `OfNat.ofNat`.
76+
For example, `(myProp_ofNat 0 : MyProp (OfNat.ofNat (OfNat.ofNat (nat_lit 0)))`.
77+
78+
This currently works because we're passing an expression instead of a declaration name,
79+
so `simp` considers it a local hypothesis and bypasses precise discrimination tree matching.
80+
-/
81+
example : MyProp 0 := by
82+
dsimp only [myProp_ofNat 0]
83+
84+
/-- If a general lemma about natural numbers plus a constant offset is specialized
85+
to a constant base, it still applies.
86+
87+
This is a tricky case because it results in a non-simp-normal lemma statement.
88+
For example, `(myProp_add_one 0 : MyProp (0 + 1))` can be simplified to `MyProp 1`.-/
89+
example : MyProp 1 := by
90+
dsimp only [myProp_add_one 0]
91+
92+
/-- If a general lemma about numerals that expresses a lower-bound
93+
through a constant offset is specialized to a constant base, it still applies.-/
94+
example : MyProp 1 := by
95+
dsimp only [myProp_ofNat_add_one 0]
96+
97+
class MyClass (n : Nat) : Prop where
98+
99+
instance myClass_succ [MyClass n] : MyClass (n.succ) := ⟨⟩
100+
101+
section BaseZero
102+
103+
local instance myClass_nat_zero : MyClass (Nat.zero) := ⟨⟩
104+
105+
/-- A base instance for `P Nat.zero` and a step instance for `P n → P (n.succ)` can combine to reach any
106+
sequence of `Nat.zero...succ.succ`.
107+
108+
Because the kernel has special handling for unifying `Nat.succ`,
109+
this requires that they can also combine to reach any numeral.
110+
111+
For example, to reach `P (Nat.zero.succ.succ)`,
112+
the first recursive step contains the unification problem `P (Nat.zero.succ.succ) =?= P (?n.succ)`,
113+
which the kernel solves by setting `?n := 1`, *not* `?n := Nat.zero.succ`.
114+
Thereafter, we need to be able to reach the numeral `1`. -/
115+
example : MyClass (Nat.zero.succ.succ) :=
116+
inferInstance
117+
118+
#check show Nat.zero.succ.succ = Nat.succ _ from rfl -- Nat.zero.succ.succ = Nat.succ 1
119+
120+
example : MyClass 1 :=
121+
inferInstance
122+
123+
example : MyClass 0 :=
124+
inferInstance
125+
126+
end BaseZero
127+
128+
section BaseOne
129+
130+
local instance myClass_succ_nat_zero : MyClass (Nat.zero.succ) := ⟨⟩
131+
132+
/-- A base instance for `P Nat.zero.succ`
133+
and a step instance for `P n → P (n.succ)` can combine
134+
to reach any sequence of `Nat.zero.succ...succ.succ`.
135+
136+
Because the kernel has special handling for unifying `Nat.succ`,
137+
this requires that they can also combine to reach any numeral greater than `0`.-/
138+
example : MyClass (Nat.zero.succ.succ) :=
139+
inferInstance
140+
141+
example : MyClass 1 :=
142+
inferInstance
143+
144+
end BaseOne

0 commit comments

Comments
 (0)