From 342a26a0233cafb85fe70e6091eeccecb87714db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 23 Apr 2022 18:05:18 -0700 Subject: [PATCH] feat: `dsimp` tactic --- src/Init/Meta.lean | 15 ++++++++ src/Init/Notation.lean | 6 +++ src/Lean/Elab/Tactic/Simp.lean | 60 ++++++++++++++++++++++------- src/Lean/Meta/Tactic/Simp/Main.lean | 39 ++++++++++++++++++- tests/lean/run/dsimp1.lean | 18 +++++++++ 5 files changed, 124 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/dsimp1.lean diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 3df22cb834..faf799c1b8 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -994,6 +994,21 @@ inductive TransparencyMode where | all | default | reducible | instances deriving Inhabited, BEq, Repr +namespace DSimp + +structure Config where + zeta : Bool := true + beta : Bool := true + eta : Bool := true + etaStruct : Bool := true + iota : Bool := true + proj : Bool := true + decide : Bool := true + autoUnfold : Bool := false + deriving Inhabited, BEq, Repr + +end DSimp + namespace Simp def defaultMaxSteps := 100000 diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 49fa5a5df3..c0c400b60d 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -450,6 +450,12 @@ Only non-dependent propositional hypotheses are considered. -/ syntax (name := simpAll) "simp_all " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic +/-- +The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but only applies theorems that hold by +reflexivity. Thus, the result is guaranteed to be definitionally equal to the input. +-/ +syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic + /-- Delta expand the given definition. This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean. -/ diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 1de98f92b5..8c14277c29 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -16,6 +16,13 @@ open Meta declare_config_elab elabSimpConfigCore Meta.Simp.Config declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx +declare_config_elab elabDSimpConfigCore Meta.DSimp.Config + +inductive SimpKind where + | simp + | simpAll + | dsimp + deriving Inhabited, BEq /-- Implement a `simp` discharge function using the given tactic syntax code. @@ -72,12 +79,12 @@ private def mkDischargeWrapper (optDischargeSyntax : Syntax) : TacticM Simp.Disc /- `optConfig` is of the form `("(" "config" ":=" term ")")?` - If `ctx == false`, the argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. -/ -def elabSimpConfig (optConfig : Syntax) (ctx : Bool) : TermElabM Meta.Simp.Config := do - if ctx then - return (← elabSimpConfigCtxCore optConfig).toConfig - else - elabSimpConfigCore optConfig +-/ +def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.Config := do + match kind with + | .simp => elabSimpConfigCore optConfig + | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig + | .dsimp => return { (← elabDSimpConfigCore optConfig) with } private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post : Bool) (inv : Bool) : MetaM Meta.SimpTheorems := do if e.isConst then @@ -189,11 +196,17 @@ structure MkSimpContextResult where fvarIdToLemmaId : FVarIdToLemmaId /-- - If `ctx == false`, the config argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. - If `ctx == false`, the `discharge` option must be none -/ -def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do - if ctx && !stx[2].isNone then - throwError "'simp_all' tactic does not support 'discharger' option" + Create the `Simp.Context` for the `simp`, `dsimp`, and `simp_all` tactics. + If `kind != SimpKind.simp`, the `discharge` option must be `none` + + TODO: generate error message if non `rfl` theorems are provided as arguments to `dsimp`. +-/ +def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do + if !stx[2].isNone then + if kind == SimpKind.simpAll then + throwError "'simp_all' tactic does not support 'discharger' option" + if kind == SimpKind.dsimp then + throwError "'dsimp' tactic does not support 'discharger' option" let dischargeWrapper ← mkDischargeWrapper stx[2] let simpOnly := !stx[3].isNone let simpTheorems ← @@ -203,7 +216,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarA getSimpTheorems let congrTheorems ← getSimpCongrTheorems let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) { - config := (← elabSimpConfig stx[1] (ctx := ctx)) + config := (← elabSimpConfig stx[1] (kind := kind)) simpTheorems := #[simpTheorems], congrTheorems } if !r.starArg || ignoreStarArg then @@ -266,9 +279,30 @@ where simpLocation ctx discharge? fvarIdToLemmaId (expandOptLocation stx[5]) @[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do - let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (ctx := true) (ignoreStarArg := true) + let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true) match (← simpAll (← getMainGoal) ctx) with | none => replaceMainGoal [] | some mvarId => replaceMainGoal [mvarId] +def dsimpLocation (ctx : Simp.Context) (fvarIdToSimp : FVarIdToLemmaId := {}) (loc : Location) : TacticM Unit := do + match loc with + | Location.targets hyps simplifyTarget => + withMainContext do + let fvarIds ← getFVarIds hyps + go fvarIds simplifyTarget fvarIdToSimp + | Location.wildcard => + withMainContext do + go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) fvarIdToSimp +where + go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToSimp : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do + let mvarId ← getMainGoal + let result? ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) + match result? with + | none => replaceMainGoal [] + | some mvarId => replaceMainGoal [mvarId] + +@[builtinTactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do + let { ctx, fvarIdToLemmaId, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp) + dsimpLocation ctx fvarIdToLemmaId (expandOptLocation stx[5]) + end Lean.Elab.Tactic diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 88232379e1..0448d75462 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -688,6 +688,13 @@ def main (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Result := catch ex => if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex +def dsimpMain (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Expr := do + withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do + try + dsimp e methods ctx |>.run' {} + catch ex => + if ex.isMaxHeartbeat then throwNestedTacticEx `dsimp ex else throw ex + partial def isEqnThmHypothesis (e : Expr) : Bool := e.isForall && go e where @@ -750,6 +757,9 @@ def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := | none => Simp.main e ctx (methods := Simp.DefaultMethods.methods) | some d => Simp.main e ctx (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d }) +def dsimp (e : Expr) (ctx : Simp.Context) : MetaM Expr := do profileitM Exception "dsimp" (← getOptions) do + Simp.dsimpMain e ctx (methods := Simp.DefaultMethods.methods) + /-- Auxiliary method. Given the current `target` of `mvarId`, apply `r` which is a new target and proof that it is equaal to the current one. @@ -878,7 +888,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di -- Reason: it introduces a `mkExpectedTypeHint` mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr replaced := replaced.push fvarId - if simplifyTarget then + if simplifyTarget then match (← simpTarget mvarId ctx discharge?) with | none => return none | some mvarIdNew => mvarId := mvarIdNew @@ -902,4 +912,31 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S else return TacticResultCNM.modified mvarId' +def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do + withMVarContext mvarId do + checkNotAssigned mvarId `simp + let mut mvarId := mvarId + for fvarId in fvarIdsToSimp do + let localDecl ← getLocalDecl fvarId + let type ← instantiateMVars localDecl.type + let typeNew ← dsimp type ctx + if typeNew.isConstOf ``False then + assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId)) + return none + if typeNew != type then + mvarId ← replaceLocalDeclDefEq mvarId fvarId typeNew + if simplifyTarget then + let target ← getMVarType mvarId + let targetNew ← dsimp target ctx + if targetNew.isConstOf ``True then + assignExprMVar mvarId (mkConst ``True.intro) + return none + if let some (_, lhs, rhs) := targetNew.eq? then + if (← isDefEq lhs rhs) then + assignExprMVar mvarId (← mkEqRefl lhs) + return none + if target != targetNew then + mvarId ← replaceTargetDefEq mvarId targetNew + return some mvarId + end Lean.Meta diff --git a/tests/lean/run/dsimp1.lean b/tests/lean/run/dsimp1.lean new file mode 100644 index 0000000000..0e93bed5c3 --- /dev/null +++ b/tests/lean/run/dsimp1.lean @@ -0,0 +1,18 @@ +def Nat.isZero (x : Nat) : Bool := + match x with + | 0 => true + | x+1 => false + +example (x : Nat) : (1 + id x.succ.pred).isZero = false := by + dsimp + trace_state + simp [Nat.succ_add] + dsimp [Nat.isZero] + +@[simp] theorem isZero_succ (x : Nat) : (x + 1).isZero = false := + rfl + +theorem ex1 (x : Nat) : (id x.succ.succ.pred).isZero = false := by + dsimp + +#print ex1