Lean4
/-- For an expression `p` of the form `fun (x : α) ↦ (body : Prop)`, checks whether
`body` implies `x = a` for some `a`, and constructs a proof of `(∃ x, p x) = p a` using
`exists_of_imp_eq`. -/
partial def findImpEqProof (p : Expr) : MetaM <| Option (Expr × Expr) := do
lambdaTelescope p fun xs body => do
let #[x] := xs |
return none
withLocalDecl .anonymous .default body fun h =>
withNewMCtxDepth
(do
let some ⟨res, proof⟩ ← go x h |
return none
let pf1 ← mkLambdaFVars #[x, h] proof
return some ⟨res, ← mkAppM ``exists_of_imp_eq #[res, pf1]⟩)
where/-- Traverses the expression `h`, branching at each `And`, to find a proof of `x = a`
for some `a`. -/
go (x h : Expr) : MetaM <| Option (Expr × Expr) := do
match (← inferType h).getAppFnArgs with
| (``Eq, #[β, a, b]) =>
if !(← isDefEq (← inferType x) β) then
return none
if (← isDefEq x a) && !(b.containsFVar x.fvarId!) then
return some ⟨b, ← mkAppM ``Eq.symm #[h]⟩
if (← isDefEq x b) && !(a.containsFVar x.fvarId!) then
return some ⟨a, h⟩
else
return none
| (``And, #[_, _]) =>
if let some res← go x (← mkAppM ``And.left #[h]) then
return res
if let some res← go x (← mkAppM ``And.right #[h]) then
return res
return none
| _ =>
return none
