Lean4
/-- Checks if the theorem is suitable for the `pull` tactic. That is,
check if it is of the form `x = f ...` where `x` contains the head `f`,
but `f` is not the head of `x`.
-/
def isPullThm (declName : Name) (inv : Bool) : MetaM (Option Head) := do
let cinfo ← getConstInfo declName
forallTelescope cinfo.type fun _ type => do
let some (lhs, rhs) := type.eqOrIff? |
return none
let (lhs, rhs) := if inv then (rhs, lhs) else (lhs, rhs)
let some head := Head.ofExpr? rhs |
return none
if Head.ofExpr? lhs != some head && containsHead lhs head then
return head
return none
where/-- Checks if the expression has the head in any subexpression.
We don't need to check this for `.lambda`, because the term being a function
is sufficient for `pull fun _ ↦ _` to be applicable. -/
containsHead (e : Expr) : Head → Bool
| .const c => e.containsConst (· == c)
| .lambda => true
| .forall => (e.find? (· matches .forallE ..)).isSome
