test: for rw with nonDependentFirst

- `getFVarId` will create an exception.
- `optional` will save, and then restore the state.

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -269,13 +269,15 @@ def elabTermForApply (stx : Syntax) (mayPostpone := true) : TacticM Expr := do
   -/
   withoutRecover <| elabTerm stx none mayPostpone
 
+/--
+Elaborate `id`, if the result is a free variable `x`, return `some x`, otherwise throw exception.
+-/
 def getFVarId (id : Syntax) : TacticM FVarId := withRef id do
   -- use apply-like elaboration to suppress insertion of implicit arguments
-  let e ← withMainContext do
-    elabTermForApply id (mayPostpone := false)
-  match e with
-  | Expr.fvar fvarId => return fvarId
-  | _                => throwError "unexpected term '{e}'; expected single reference to variable"
+  let e ← withMainContext do elabTermForApply id (mayPostpone := false)
+  let .fvar fvarId := e
+    | throwError "unexpected term '{e}'; expected single reference to variable"
+  return fvarId
 
 def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
   withMainContext do ids.mapM getFVarId

src/Lean/Elab/Tactic/Rewrite.lean

@@ -45,20 +45,23 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
       withRef rule do
         let symm := !rule[0].isNone
         let term := rule[1]
-        let processId (id : Syntax) : TacticM Unit := do
+        let processId (id : TSyntax `ident) : TacticM Unit := do
           -- See if we can interpret `id` as a hypothesis first.
-          if (← optional <| getFVarId id).isSome then
+          if let some _ ← withMainContext <| Term.isLocalIdent? id then
             x symm term
           else
-            -- Try to get equation theorems for `id`.
             let declName ← try realizeGlobalConstNoOverload id catch _ => return (← x symm term)
-            let some eqThms ← getEqnsFor? declName (nonRec := true) | x symm term
-            let rec go : List Name →  TacticM Unit
-              | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
-              -- Remark: we prefix `eqThm` with `_root_` to ensure it is resolved correctly.
-              -- See test: `rwPrioritizesLCtxOverEnv.lean`
-              | eqThm::eqThms => (x symm (mkIdentFrom id (`_root_ ++ eqThm))) <|> go eqThms
-            go eqThms.toList
+            if let some eqThms ← getEqnsFor? declName (nonRec := true) then
+              -- Try to get equation theorems for `id`.
+              let rec go : List Name →  TacticM Unit
+                | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
+                -- Remark: we prefix `eqThm` with `_root_` to ensure it is resolved correctly.
+                -- See test: `rwPrioritizesLCtxOverEnv.lean`
+                | eqThm::eqThms => (x symm (mkIdentFrom id (`_root_ ++ eqThm))) <|> go eqThms
+              go eqThms.toList
+            else
+              -- Treat identifier as `@id`. We use this approach in `simp`. See issue #2736
+              x symm (← `(@$id))
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
         match term with
         | `($id:ident)  => processId id

src/Lean/Meta/Tactic/Apply.lean

@@ -56,6 +56,20 @@ def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Arr
             let currTag ← mvarIdNew.getTag
             mvarIdNew.setTag (appendTag parentTag currTag)
 
+/--
+Discharge goals of the form `optParam P p`.
+-/
+def synthDefaultParams (mvarId : MVarId) (tacticName : Name) (newMVars : Array Expr) (allowFailures : Bool) : MetaM Unit := do
+  for mvar in newMVars do
+    unless (← mvar.mvarId!.isAssigned) do
+      let mvarType ← inferType mvar
+      try
+        if let some defValue := mvarType.getOptParamDefault? then
+          unless (← isDefEq mvar defValue) do
+            throwTacticEx tacticName mvarId "failed to use default value for optional parameter"
+      catch e =>
+          unless allowFailures do throw e
+
 /--
 If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
 even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
@@ -64,7 +78,8 @@ one inferred. The `congr` tactic sets this flag to false.
 def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
     (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
   synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
-  -- TODO: default and auto params
+  synthDefaultParams mvarId tacticName newMVars allowSynthFailures
+  -- Auto params should not be handled here. The require us to use the tactic interpreter that is in `TacticM`
   appendParentTag mvarId newMVars binderInfos
 
 private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
@@ -85,14 +100,14 @@ private def partitionDependentMVars (mvars : Array Expr) : MetaM (Array MVarId
     else
       return (nonDeps.push currMVarId, deps)
 
-private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MVarId)
-  | ApplyNewGoals.nonDependentFirst => do
+def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MVarId)
+  | .nonDependentFirst => do
       let (nonDeps, deps) ← partitionDependentMVars mvars
       return nonDeps.toList ++ deps.toList
-  | ApplyNewGoals.nonDependentOnly => do
+  | .nonDependentOnly => do
       let (nonDeps, _) ← partitionDependentMVars mvars
       return nonDeps.toList
-  | ApplyNewGoals.all => return mvars.toList.map Lean.Expr.mvarId!
+  | .all => return mvars.toList.map Lean.Expr.mvarId!
 
 /-- Custom `isDefEq` for the `apply` tactic -/
 private def isDefEqApply (cfg : ApplyConfig) (a b : Expr) : MetaM Bool := do
@@ -154,8 +169,8 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     let e ← instantiateMVars e
     mvarId.assign (mkAppN e newMVars)
     let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
-    let otherMVarIds ← getMVarsNoDelayed e
     let newMVarIds ← reorderGoals newMVars cfg.newGoals
+    let otherMVarIds ← getMVarsNoDelayed e
     let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId
     let result := newMVarIds ++ otherMVarIds.toList
     result.forM (·.headBetaType)

src/Lean/Meta/Tactic/Rewrite.lean

@@ -56,11 +56,12 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
             (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
-          let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
+          let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
+          let newMVarIds ← reorderGoals newMVars config.newGoals
           let otherMVarIds ← getMVarsNoDelayed heqIn
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
-          let newMVarIds := newMVarIds ++ otherMVarIds
-          pure { eNew := eNew, eqProof := eqPrf, mvarIds := newMVarIds.toList }
+          let newMVarIds := newMVarIds ++ otherMVarIds.toList
+          pure { eNew := eNew, eqProof := eqPrf, mvarIds := newMVarIds }
         match symm with
         | false => cont heq heqType lhs rhs
         | true  => do

tests/lean/run/2736.lean

@@ -0,0 +1,61 @@
+set_option autoImplicit true
+
+section Mathlib.Init.ZeroOne
+
+class One (α : Type) where
+  one : α
+
+instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+
+end Mathlib.Init.ZeroOne
+
+section Mathlib.Algebra.Group.Defs
+
+class MulOneClass (M : Type) extends One M, Mul M where
+  one_mul : ∀ a : M, 1 * a = a
+
+export MulOneClass (one_mul)
+
+end Mathlib.Algebra.Group.Defs
+
+section Mathlib.Algebra.Ring.Defs
+
+class Distrib (R : Type) extends Mul R, Add R where
+  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+
+class RightDistribClass (R : Type) [Mul R] [Add R] : Prop where
+  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+
+instance Distrib.rightDistribClass (R : Type) [Distrib R] : RightDistribClass R :=
+  ⟨Distrib.right_distrib⟩
+
+theorem add_mul [Mul R] [Add R] [RightDistribClass R] (a b c : R) :
+    (a + b) * c = a * c + b * c :=
+  RightDistribClass.right_distrib a b c
+
+theorem add_one_mul [Add α] [MulOneClass α] [RightDistribClass α] (a b : α) :
+    (a + 1) * b = a * b + b := by
+  rw [add_mul, one_mul]; done
+
+class Semiring (R : Type) extends Distrib R, MulOneClass R
+
+end Mathlib.Algebra.Ring.Defs
+
+section Mathlib.Data.Nat.Basic
+
+instance : Semiring Nat where
+  add := Nat.add
+  mul := Nat.mul
+  one := Nat.succ Nat.zero
+  one_mul := sorry
+  right_distrib := sorry
+
+end Mathlib.Data.Nat.Basic
+
+#synth MulOneClass Nat       -- works
+#synth RightDistribClass Nat -- works
+
+example {a b : Nat} : (a + 1) * b = a * b + b :=
+  have := add_one_mul a b -- works
+  by rw [add_one_mul]     -- should not produce: failed to synthesize instance: RightDistribClass ?m

tests/lean/run/rwOptParam.lean

@@ -0,0 +1,9 @@
+axiom P : Prop
+axiom p : P
+axiom f : P → Nat
+axiom Q : Nat → Prop
+axiom q : ∀ n, Q n
+theorem r (p : P := p) : 0 = f p := sorry
+example : Q 0 := by
+  rw [r]
+  apply q

tests/lean/run/rw_nondepFirst.lean

@@ -0,0 +1,14 @@
+def Set (ι : Type) := ι → Prop
+
+namespace Set
+
+def univ : Set ι := fun _ => True
+def empty : Set ι := fun _ => False
+
+def pi {ι : Type} {α : ι → Type} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := sorry
+
+theorem univ_pi_eq_empty (ht : t i = empty) : Set.pi univ t = empty := sorry
+
+example (i : ι) (h : t i = empty) : Set.pi univ t = empty := by
+  rw [univ_pi_eq_empty]
+  · exact h