Skip to content

Commit

Permalink
feat: dsimprocs for ite and dite (leanprover#4430)
Browse files Browse the repository at this point in the history
  • Loading branch information
leodemoura authored Jun 11, 2024
1 parent ab73ac9 commit ce6ebd1
Show file tree
Hide file tree
Showing 4 changed files with 74 additions and 1 deletion.
41 changes: 40 additions & 1 deletion src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
return .visit { expr := eb, proof? := pr }
return .continue

builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
builtin_simproc ↓ [simp, seval] reduceDIte (dite _ _ _) := fun e => do
let_expr f@dite α c i tb eb ← e | return .continue
let r ← simp c
if r.expr.isTrue then
Expand All @@ -36,3 +36,42 @@ builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_false f.constLevels!) α c i tb eb) pr
return .visit { expr := eNew, proof? := prNew }
return .continue

builtin_dsimproc ↓ [simp, seval] dreduceIte (ite _ _ _) := fun e => do
unless (← inDSimp) do
-- If `simp` is not in `dsimp` mode, we should use `reduceIte`
return .continue
let_expr ite _ c i tb eb ← e | return .continue
/-
We don't want to use `whnfD i` directly because it is potentially too expensive.
We considered using `whnfI i`, but it is too inconvenient for users.
They would have to list auxiliary functions used to establish that a proposition
is decidable as `reducible` and/or list them to be unfolded by `simp`.
Thus, we are currently using the following "filter": if `simp` reduces the
condition to `True` or `False`, we execute `whnfD i` and check whether it
reduces `i` to `Decidable.isTrue` or `Decidable.isFalse`.
Recall that all declarations defined by well-founded recursion are
now marked as `[irreducible]`. Thus, we will not timeout trying to
reduce them using the default reduction mode.
-/
let r ← simp c
if r.expr.isTrue || r.expr.isFalse then
match_expr (← whnfD i) with
| Decidable.isTrue _ _ => return .visit tb
| Decidable.isFalse _ _ => return .visit eb
| _ => return .continue
return .continue

builtin_dsimproc ↓ [simp, seval] dreduceDIte (dite _ _ _) := fun e => do
unless (← inDSimp) do
-- If `simp` is not in `dsimp` mode, we should use `reduceDIte`
return .continue
let_expr dite _ c i tb eb ← e | return .continue
-- See comment at `dreduceIte`
let r ← simp c
if r.expr.isTrue || r.expr.isFalse then
match_expr (← whnfD i) with
| Decidable.isTrue _ h => return .visit (mkApp tb h).headBeta
| Decidable.isFalse _ h => return .visit (mkApp eb h).headBeta
| _ => return .continue
return .continue
1 change: 1 addition & 0 deletions src/Lean/Meta/Tactic/Simp/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -459,6 +459,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
let m ← getMethods
let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
let post := m.dpost >> dsimpReduce
withTheReader Simp.Context (fun ctx => { ctx with inDSimp := true }) do
transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)

def visitFn (e : Expr) : SimpM Result := do
Expand Down
12 changes: 12 additions & 0 deletions src/Lean/Meta/Tactic/Simp/Types.lean
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,11 @@ structure Context where
invalidating the cache.
-/
lctxInitIndices : Nat := 0
/--
If `inDSimp := true`, then `simp` is in `dsimp` mode, and only applying
transformations that presereve definitional equality.
-/
inDSimp : Bool := false
deriving Inhabited

def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
Expand Down Expand Up @@ -312,6 +317,13 @@ def getSimpTheorems : SimpM SimpTheoremsArray :=
def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
return (← readThe Context).congrTheorems

/--
Returns `true` if `simp` is in `dsimp` mode.
That is, only transformations that preserve definitional equality should be applied.
-/
def inDSimp : SimpM Bool :=
return (← readThe Context).inDSimp

@[inline] def withPreservedCache (x : SimpM α) : SimpM α := do
-- Recall that `cache.map₁` should be used linearly but `cache.map₂` is great for copies.
let savedMap₂ := (← get).cache.map₂
Expand Down
21 changes: 21 additions & 0 deletions tests/lean/run/ite_dsimproc.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
open BitVec

example (x : BitVec n) : zeroExtend (if 1#1 = 1#1 then 128 else 64) x = zeroExtend 128 x := by
simp

example (x : BitVec n) : zeroExtend (if 1#1 = 0#1 then 128 else 64) x = zeroExtend 64 x := by
simp

abbrev f (_ : 1#1 = 1#1) := 128

example (h' : 128 = n) : (if h : 1#1 = 1#1 then f h else 20) = n := by
dsimp [-dite_eq_ite]
guard_target = f _ = n
exact h'

abbrev g (_ : 1#10#1) := 128

example (h' : 128 = m) : (if h : 1#1 = 0#1 then 10 else g h) = m := by
dsimp [-dite_eq_ite]
guard_target = g _ = m
exact h'

0 comments on commit ce6ebd1

Please sign in to comment.