From 8225be2f0ee9acc743fd04cec37ecc141d1efa15 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Nov 2022 16:39:38 -0800 Subject: [PATCH] feat: ensure projections are not reducing at `DiscrTree V (simpleReduce := true)` Now, the `simp` discrimination tree does not perform `iota` nor reduce projections. --- src/Lean/Meta/DiscrTree.lean | 27 ++++++-------------- src/Lean/Meta/WHNF.lean | 42 ++++++++++++++++++-------------- tests/lean/973.lean.expected.out | 2 -- tests/lean/run/946.lean | 2 +- 4 files changed, 33 insertions(+), 40 deletions(-) diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index ac69df5ff1..53d67e8199 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -225,23 +225,12 @@ def hasNoindexAnnotation (e : Expr) : Bool := /-- Reduction procedure for the discrimination tree indexing. -It only unfolds reducible definitions, and does not perform iota reduction. - -We disable iota reduction because of simp theorems such as -``` -@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) : - Quot.liftOn (Quot.mk r a) f h = f a := rfl -``` -If we use iota, the lhs becomes `f a` - -We have considered disabling other reductions (e.g., projection reduction), but -we could not even compile `Init` with this setup. - -Remark: rnote it is not sufficient to just unfold reducible definitions and perform -beta-reduction, we must also instantiate assgined metavariables, and perform zeta-reduction. +The parameter `simpleReduce` controls how aggressive the term is reduced. +The parameter at type `DiscrTree` controls this value. +See comment at `DiscrTree`. -/ partial def reduce (e : Expr) (simpleReduce : Bool) : MetaM Expr := do - let e ← whnfCore e (iota := !simpleReduce) + let e ← whnfCore e (simpleReduceOnly := simpleReduce) match (← unfoldDefinition? e) with | some e => reduce e simpleReduce | none => match e.etaExpandedStrict? with @@ -267,21 +256,21 @@ private def isBadKey (fn : Expr) : Bool := Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term is a bad key (see comment at `isBadKey`). We use this method instead of `reduce` for root terms at `pushArgs`. -/ -private partial def reduceUntilBadKey (e : Expr) : MetaM Expr := do +private partial def reduceUntilBadKey (e : Expr) (simpleReduce : Bool) : MetaM Expr := do let e ← step e match e.etaExpandedStrict? with - | some e => reduceUntilBadKey e + | some e => reduceUntilBadKey e simpleReduce | none => return e where step (e : Expr) := do - let e ← whnfCore e (iota := false) + let e ← whnfCore e (simpleReduceOnly := simpleReduce) match (← unfoldDefinition? e) with | some e' => if isBadKey e'.getAppFn then return e else step e' | none => return e /-- whnf for the discrimination tree module -/ def reduceDT (e : Expr) (root : Bool) (simpleReduce : Bool) : MetaM Expr := - if root then reduceUntilBadKey e else reduce e simpleReduce + if root then reduceUntilBadKey e simpleReduce else reduce e simpleReduce /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/ diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 3ee8da403b..faadca91fe 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -485,14 +485,17 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) := return none /-- - Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction, - expand let-expressions, expand assigned meta-variables. +Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction, +expand let-expressions, expand assigned meta-variables. - The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`, - then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`. - We only set this flag to `false` when implementing `isDefEq`. +The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`, +then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`. +We only set this flag to `false` when implementing `isDefEq`. + +If `simpleReduceOnly`, then `iota` and projection reduction are not performed. +Note that the value of `deltaAtProj` is irrelevant if `simpleReduceOnly = true`. -/ -partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) (iota := true) : MetaM Expr := +partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) (simpleReduceOnly := false) : MetaM Expr := go e where go (e : Expr) : MetaM Expr := @@ -511,14 +514,14 @@ where go eNew else let e := if f == f' then e else e.updateFn f' - match (← reduceMatcher? e) with - | ReduceMatcherResult.reduced eNew => go eNew - | ReduceMatcherResult.partialApp => pure e - | ReduceMatcherResult.stuck _ => pure e - | ReduceMatcherResult.notMatcher => - if !iota then - return e - else + if simpleReduceOnly then + return e + else + match (← reduceMatcher? e) with + | ReduceMatcherResult.reduced eNew => go eNew + | ReduceMatcherResult.partialApp => pure e + | ReduceMatcherResult.stuck _ => pure e + | ReduceMatcherResult.notMatcher => matchConstAux f' (fun _ => return e) fun cinfo lvls => match cinfo with | ConstantInfo.recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) go @@ -530,10 +533,13 @@ where return e | _ => return e | Expr.proj _ i c => - let c ← if deltaAtProj then whnf c else whnfCore c - match (← projectCore? c i) with - | some e => go e - | none => return e + if simpleReduceOnly then + return e + else + let c ← if deltaAtProj then whnf c else whnfCore c + match (← projectCore? c i) with + | some e => go e + | none => return e | _ => unreachable! /-- diff --git a/tests/lean/973.lean.expected.out b/tests/lean/973.lean.expected.out index a56dc3b7b1..e69de29bb2 100644 --- a/tests/lean/973.lean.expected.out +++ b/tests/lean/973.lean.expected.out @@ -1,2 +0,0 @@ -973.lean:4:2-4:6: error: invalid `simp` theorem, equation is equivalent to - x = x diff --git a/tests/lean/run/946.lean b/tests/lean/run/946.lean index 5d89516eb4..e47a678ac4 100644 --- a/tests/lean/run/946.lean +++ b/tests/lean/run/946.lean @@ -76,7 +76,7 @@ theorem consistentConcatOfConsistentRow match df with | ⟨_, rows, hr⟩ => by induction rows with - | nil => simp [hc] -- breaks here + | nil => simp at hc; simp [hc] | cons _ _ hi => exact ⟨hr.1, hi hr.2 hc⟩ def addRow (df : DataFrame) (row : List DataEntry)