Lean4
/-- Does `Lean.MVarId.intros` but then cleans up the introduced hypotheses, removing anything
that is trivial. If there are any patterns in the current `CongrMetaM` state then instead
of `Lean.MVarId.intros` it does `Lean.Elab..Tactic.RCases.rintro`.
Cleaning up includes:
- deleting hypotheses of the form `x ≍ x`, `x = x`, and `x ↔ x`.
- deleting Prop hypotheses that are already in the local context.
- converting `x ≍ y` to `x = y` if possible.
- converting `x = y` to `x ↔ y` if possible.
-/
partial def introsClean (mvarId : MVarId) : CongrMetaM (List MVarId) :=
loop mvarId
where
heqImpOfEqImp (mvarId : MVarId) : MetaM (Option MVarId) :=
observing? <|
withReducible
(do
let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``heq_imp_of_eq_imp) |
failure
return mvarId)
eqImpOfIffImp (mvarId : MVarId) : MetaM (Option MVarId) :=
observing? <|
withReducible
(do
let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``eq_imp_of_iff_imp) |
failure
return mvarId)
loop (mvarId : MVarId) : CongrMetaM (List MVarId) :=
mvarId.withContext
(do
let ty ← withReducible <| mvarId.getType'
if ty.isForall then
let mvarId := (← heqImpOfEqImp mvarId).getD mvarId
let mvarId := (← eqImpOfIffImp mvarId).getD mvarId
let ty ← withReducible <| mvarId.getType'
if ty.isArrow then
if
←
(isTrivialType ty.bindingDomain! <||>
(← getLCtx).anyM
(fun decl => do
return (← Lean.instantiateMVars decl.type) == ty.bindingDomain!)) then
-- Don't intro, clear it
let mvar ← mkFreshExprSyntheticOpaqueMVar ty.bindingBody! (← mvarId.getTag)
mvarId.assign <| .lam .anonymous ty.bindingDomain! mvar .default
return ← loop mvar.mvarId!
if let some patt← CongrMetaM.nextPattern then
let gs ← Term.TermElabM.run' <| Lean.Elab.Tactic.RCases.rintro #[patt] none mvarId
List.flatten <$> gs.mapM loop
else
let (_, mvarId) ← mvarId.intro1
loop mvarId
else
return [mvarId])
isTrivialType (ty : Expr) : MetaM Bool := do
unless ← Meta.isProp ty do
return false
let ty ← Lean.instantiateMVars ty
if let some (lhs, rhs) := ty.eqOrIff? then
if lhs.cleanupAnnotations == rhs.cleanupAnnotations then
return true
if let some (α, lhs, β, rhs) := ty.heq? then
if α.cleanupAnnotations == β.cleanupAnnotations && lhs.cleanupAnnotations == rhs.cleanupAnnotations then
return true
return false
