From 0041de5d1d1a192540cd34d9ad02fa2323aa314f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Oct 2022 07:24:27 -0700 Subject: [PATCH] fix: congr tactic should not try to synthesize instance implicit arguments that have been inferred when applying congr theorem see #1711 --- src/Lean/Meta/CongrTheorems.lean | 2 +- src/Lean/Meta/Tactic/Apply.lean | 51 +++++++++++++++++++------------- src/Lean/Meta/Tactic/Congr.lean | 2 +- tests/lean/run/1711.lean | 28 ++++++++++++++++++ 4 files changed, 61 insertions(+), 22 deletions(-) create mode 100644 tests/lean/run/1711.lean diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 3bea8f865b..3bf34d0e3d 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -30,7 +30,7 @@ inductive CongrArgKind where For congr-simp theorems only. Indicates a decidable instance argument. The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/ | subsingletonInst - deriving Inhabited + deriving Inhabited, Repr structure CongrTheorem where type : Expr diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index a42de3520b..b6ff612de8 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -9,6 +9,23 @@ import Lean.Meta.CollectMVars import Lean.Meta.Tactic.Util namespace Lean.Meta +/-- Controls which new mvars are turned in to goals by the `apply` tactic. +- `nonDependentFirst` mvars that don't depend on other goals appear first in the goal list. +- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list. +- `all` all unassigned mvars are added to the goal list. +-/ +inductive ApplyNewGoals where + | nonDependentFirst | nonDependentOnly | all + +/-- Configures the behaviour of the `apply` tactic. -/ +structure ApplyConfig where + newGoals := ApplyNewGoals.nonDependentFirst + /-- + 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 + one inferred. The `congr` tactic sets this flag to false. + -/ + synthAssignedInstances := true /-- Compute the number of expected arguments and whether the result type is of the form @@ -25,14 +42,15 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α := throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}" -def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := +def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances : Bool) : MetaM Unit := newMVars.size.forM fun i => do if binderInfos[i]!.isInstImplicit then let mvar := newMVars[i]! - let mvarType ← inferType mvar - let mvarVal ← synthInstance mvarType - unless (← isDefEq mvar mvarVal) do - throwTacticEx tacticName mvarId "failed to assign synthesized instance" + if synthAssignedInstances || !(← mvar.mvarId!.isAssigned) then + let mvarType ← inferType mvar + let mvarVal ← synthInstance mvarType + unless (← isDefEq mvar mvarVal) do + throwTacticEx tacticName mvarId "failed to assign synthesized instance" def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do let parentTag ← mvarId.getTag @@ -48,8 +66,13 @@ def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Arr let currTag ← mvarIdNew.getTag mvarIdNew.setTag (appendTag parentTag currTag) -def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do - synthAppInstances tacticName mvarId newMVars binderInfos +/-- +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 +one inferred. The `congr` tactic sets this flag to false. +-/ +def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances := true) : MetaM Unit := do + synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances -- TODO: default and auto params appendParentTag mvarId newMVars binderInfos @@ -71,14 +94,6 @@ private def partitionDependentMVars (mvars : Array Expr) : MetaM (Array MVarId else return (nonDeps.push currMVarId, deps) -/-- Controls which new mvars are turned in to goals by the `apply` tactic. -- `nonDependentFirst` mvars that don't depend on other goals appear first in the goal list. -- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list. -- `all` all unassigned mvars are added to the goal list. --/ -inductive ApplyNewGoals where - | nonDependentFirst | nonDependentOnly | all - private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MVarId) | ApplyNewGoals.nonDependentFirst => do let (nonDeps, deps) ← partitionDependentMVars mvars @@ -88,10 +103,6 @@ private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MV return nonDeps.toList | ApplyNewGoals.all => return mvars.toList.map Lean.Expr.mvarId! -/-- Configures the behaviour of the `apply` tactic. -/ -structure ApplyConfig where - newGoals := ApplyNewGoals.nonDependentFirst - /-- Close the given goal using `apply e`. -/ @@ -106,7 +117,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := numArgs := numArgs - targetTypeNumArgs let (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType (some numArgs) unless (← isDefEq eType targetType) do throwApplyError mvarId eType targetType - postprocessAppMVars `apply mvarId newMVars binderInfos + postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances let e ← instantiateMVars e mvarId.assign (mkAppN e newMVars) let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned diff --git a/src/Lean/Meta/Tactic/Congr.lean b/src/Lean/Meta/Tactic/Congr.lean index 4752528d03..81545f2fec 100644 --- a/src/Lean/Meta/Tactic/Congr.lean +++ b/src/Lean/Meta/Tactic/Congr.lean @@ -33,7 +33,7 @@ Return the `fvarId` for the new hypothesis and the new subgoals. private def applyCongrThm? (mvarId : MVarId) (congrThm : CongrTheorem) : MetaM (List MVarId) := do let mvarId ← mvarId.assert (← mkFreshUserName `h_congr_thm) congrThm.type congrThm.proof let (fvarId, mvarId) ← mvarId.intro1P - let mvarIds ← mvarId.apply (mkFVar fvarId) + let mvarIds ← mvarId.apply (mkFVar fvarId) { synthAssignedInstances := false } mvarIds.mapM fun mvarId => mvarId.tryClear fvarId /-- diff --git a/tests/lean/run/1711.lean b/tests/lean/run/1711.lean new file mode 100644 index 0000000000..1af73a4353 --- /dev/null +++ b/tests/lean/run/1711.lean @@ -0,0 +1,28 @@ +class One (α : Type u) where + one : α + +instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where + ofNat := ‹One α›.1 + +class MulOneClass (M : Type u) extends One M, Mul M where + one_mul : ∀ a : M, 1 * a = a + mul_one : ∀ a : M, a * 1 = a + +theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁.one = m₂.one → m₁ = m₂ := by + intro m₁ m₂ + cases m₁ with + | @mk one₁ mul₁ one_mul₁ mul_one₁ => + cases one₁ with | mk one₁ => + cases mul₁ with | mk mul₁ => + cases m₂ with + | @mk one₂ mul₂ one_mul₂ mul_one₂ => + cases one₂ with | mk one₂ => + cases mul₂ with | mk mul₂ => + simp + intro h + simp [toMul, Mul.mul] at h -- h : mul₁ = mul₂ + cases h + intro h + simp [toOne, One.one] at h -- h : one₁ = one₂ + cases h + congr