Lean4
/-- Given `(hNotEx : Not ex)` where `ex` is of the form `Exists x, p x`,
return a `forall x, Not (p x)` and a proof for it.
This function handles nested existentials. -/
partial def forallNot_of_notExists (ex hNotEx : Expr) : MetaM (Expr × Expr) := do
let .app (.app (.const ``Exists [lvl]) A) p := ex |
failure
go lvl A p hNotEx
where/-- Given `(hNotEx : Not (@Exists.{lvl} A p))`,
return a `forall x, Not (p x)` and a proof for it.
This function handles nested existentials. -/
go (lvl : Level) (A p hNotEx : Expr) : MetaM (Expr × Expr) := do
let xn ← mkFreshUserName `x
withLocalDeclD xn A fun x => do
let px := p.beta #[x]
let notPx := mkNot px
let hAllNotPx := mkApp3 (.const ``forall_not_of_not_exists [lvl]) A p hNotEx
if let .app (.app (.const ``Exists [lvl']) A') p' := px then
let hNotPxN ← mkFreshUserName `h
withLocalDeclD hNotPxN notPx fun hNotPx => do
let (qx, hQx) ← go lvl' A' p' hNotPx
let allQx ← mkForallFVars #[x] qx
let hNotPxImpQx ← mkLambdaFVars #[hNotPx] hQx
let hAllQx ← mkLambdaFVars #[x] (.app hNotPxImpQx (.app hAllNotPx x))
return (allQx, hAllQx)
else
let allNotPx ← mkForallFVars #[x] notPx
return (allNotPx, hAllNotPx)
