Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
-/

import Lean
import Mathlib.Lean.Expr
import Mathlib.Logic.Basic
import Mathlib.Init.Algebra.Order
import Mathlib.Tactic.Conv

namespace Mathlib.Tactic.PushNeg

open Lean Meta Elab.Tactic Parser.Tactic

variable (p: Propp q: Propq : Prop: TypeProp) (s: Ξ± β Props : Ξ±: ?m.766Ξ± β Prop: TypeProp)

theorem not_not_eq: (Β¬Β¬p) = pnot_not_eq : (Β¬ Β¬ p: Propp) = p: Propp := propext: β {a b : Prop}, (a β b) β a = bpropext not_not: β {a : Prop}, Β¬Β¬a β anot_not
theorem not_and_eq: (Β¬(p β§ q)) = (p β Β¬q)not_and_eq : (Β¬ (p: Propp β§ q: Propq)) = (p: Propp β Β¬ q: Propq) := propext: β {a b : Prop}, (a β b) β a = bpropext not_and: β {a b : Prop}, Β¬(a β§ b) β a β Β¬bnot_and
theorem not_and_or_eq: (Β¬(p β§ q)) = (Β¬p β¨ Β¬q)not_and_or_eq : (Β¬ (p: Propp β§ q: Propq)) = (Β¬ p: Propp β¨ Β¬ q: Propq) := propext: β {a b : Prop}, (a β b) β a = bpropext not_and_or: β {a b : Prop}, Β¬(a β§ b) β Β¬a β¨ Β¬bnot_and_or
theorem not_or_eq: (Β¬(p β¨ q)) = (Β¬p β§ Β¬q)not_or_eq : (Β¬ (p: Propp β¨ q: Propq)) = (Β¬ p: Propp β§ Β¬ q: Propq) := propext: β {a b : Prop}, (a β b) β a = bpropext not_or: β {p q : Prop}, Β¬(p β¨ q) β Β¬p β§ Β¬qnot_or
theorem not_forall_eq: β {Ξ± : Sort u_1} (s : Ξ± β Prop), (Β¬β (x : Ξ±), s x) = β x, Β¬s xnot_forall_eq : (Β¬ β x: ?m.183x, s: Ξ± β Props x: ?m.183x) = (β x: ?m.190x, Β¬ s: Ξ± β Props x: ?m.190x) := propext: β {a b : Prop}, (a β b) β a = bpropext not_forall: β {Ξ± : Sort ?u.201} {p : Ξ± β Prop}, (Β¬β (x : Ξ±), p x) β β x, Β¬p xnot_forall
theorem not_exists_eq: (Β¬β x, s x) = β (x : Ξ±), Β¬s xnot_exists_eq : (Β¬ β x: ?m.241x, s: Ξ± β Props x: ?m.241x) = (β x: ?m.246x, Β¬ s: Ξ± β Props x: ?m.246x) := propext: β {a b : Prop}, (a β b) β a = bpropext not_exists: β {Ξ± : Sort ?u.257} {p : Ξ± β Prop}, (Β¬β x, p x) β β (x : Ξ±), Β¬p xnot_exists
theorem not_implies_eq: (Β¬(p β q)) = (p β§ Β¬q)not_implies_eq : (Β¬ (p: Propp β q: Propq)) = (p: Propp β§ Β¬ q: Propq) := propext: β {a b : Prop}, (a β b) β a = bpropext not_imp: β {a b : Prop}, Β¬(a β b) β a β§ Β¬bnot_imp
theorem not_ne_eq: β (x y : Ξ±), (Β¬x β  y) = (x = y)not_ne_eq (x: Ξ±x y: Ξ±y : Ξ±: ?m.321Ξ±) : (Β¬ (x: Ξ±x β  y: Ξ±y)) = (x: Ξ±x = y: Ξ±y) := ne_eq: β {Ξ± : Sort ?u.345} (a b : Ξ±), (a β  b) = Β¬a = bne_eq x: Ξ±x y: Ξ±y βΈ not_not_eq: β (p : Prop), (Β¬Β¬p) = pnot_not_eq _: Prop_

variable {Ξ²: Type uΞ² : Type u: Type (u+1)Type u} [LinearOrder: Type ?u.385 β Type ?u.385LinearOrder Ξ²: Type uΞ²]
theorem not_le_eq: β (a b : Ξ²), (Β¬a β€ b) = (b < a)not_le_eq (a: Ξ²a b: Ξ²b : Ξ²: Type uΞ²) : (Β¬ (a: Ξ²a β€ b: Ξ²b)) = (b: Ξ²b < a: Ξ²a) := propext: β {a b : Prop}, (a β b) β a = bpropext not_le: β {Ξ± : Type ?u.461} [inst : LinearOrder Ξ±] {a b : Ξ±}, Β¬a β€ b β b < anot_le
theorem not_lt_eq: β (a b : Ξ²), (Β¬a < b) = (b β€ a)not_lt_eq (a: Ξ²a b: Ξ²b : Ξ²: Type uΞ²) : (Β¬ (a: Ξ²a < b: Ξ²b)) = (b: Ξ²b β€ a: Ξ²a) := propext: β {a b : Prop}, (a β b) β a = bpropext not_lt: β {Ξ± : Type ?u.554} [inst : LinearOrder Ξ±] {a b : Ξ±}, Β¬a < b β b β€ anot_lt
theorem not_ge_eq: β (a b : Ξ²), (Β¬a β₯ b) = (a < b)not_ge_eq (a: Ξ²a b: Ξ²b : Ξ²: Type uΞ²) : (Β¬ (a: Ξ²a β₯ b: Ξ²b)) = (a: Ξ²a < b: Ξ²b) := propext: β {a b : Prop}, (a β b) β a = bpropext not_le: β {Ξ± : Type ?u.647} [inst : LinearOrder Ξ±] {a b : Ξ±}, Β¬a β€ b β b < anot_le
theorem not_gt_eq: β (a b : Ξ²), (Β¬a > b) = (a β€ b)not_gt_eq (a: Ξ²a b: Ξ²b : Ξ²: Type uΞ²) : (Β¬ (a: Ξ²a > b: Ξ²b)) = (a: Ξ²a β€ b: Ξ²b) := propext: β {a b : Prop}, (a β b) β a = bpropext not_lt: β {Ξ± : Type ?u.740} [inst : LinearOrder Ξ±] {a b : Ξ±}, Β¬a < b β b β€ anot_lt

/-- Make `push_neg` use `not_and_or` rather than the default `not_and`. -/
register_option push_neg.use_distrib: Lean.Option Boolpush_neg.use_distrib : Bool: TypeBool :=
{ defValue := false: Boolfalse
group := "": String""
descr := "Make `push_neg` use `not_and_or` rather than the default `not_and`.": String"Make `push_neg` use `not_and_or` rather than the default `not_and`." }

/-- Push negations at the top level of the current expression. -/
def transformNegationStep: Expr β SimpM (Option Simp.Step)transformNegationStep (e: Expre : Expr: TypeExpr) : SimpM: Type β TypeSimpM (Option: Type ?u.925 β Type ?u.925Option Simp.Step: TypeSimp.Step) := do
let mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (e: Expre : Expr: TypeExpr) (pf: Exprpf : Expr: TypeExpr) : Simp.Step: TypeSimp.Step :=
Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit { expr := e: Expre, proof? := some: {Ξ± : Type ?u.1255} β Ξ± β Option Ξ±some pf: Exprpf }
let e_whnf: ?m.1407e_whnf β whnfR: Expr β MetaM ExprwhnfR e: Expre
let some: {Ξ± : Type ?u.967} β Ξ± β Option Ξ±some ex: Exprex := e_whnf: ?m.1407e_whnf.not?: Expr β Option Exprnot? | return Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit { expr := e: Expre }
match ex: Exprex.getAppFnArgs: Expr β Name Γ Array ExprgetAppFnArgs with
| (``Not: Name``Not: Prop β PropNot, #[e: Expre]) =>
return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep e: Expre (β mkAppM ``not_not_eq #[e]): ?m.1533(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_not_eq #[e]): ?m.1533 ``not_not_eq: β (p : Prop), (Β¬Β¬p) = pnot_not_eq(β mkAppM ``not_not_eq #[e]): ?m.1533 #[e: Expre(β mkAppM ``not_not_eq #[e]): ?m.1533])
| (``And: Name``And: Prop β Prop β PropAnd, #[p: Exprp, q: Exprq]) =>
match β getBoolOption: {m : Type β Type} β [inst : Monad m] β [inst : MonadOptions m] β Name β optParam Bool false β m BoolgetBoolOption `push_neg.use_distrib: Name`push_neg.use_distrib with
| false: Boolfalse => return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (.forallE: Name β Expr β Expr β BinderInfo β Expr.forallE `_: Name`_ p: Exprp (mkNot: Expr β ExprmkNot q: Exprq) default: {Ξ± : Sort ?u.1966} β [self : Inhabited Ξ±] β Ξ±default) (βmkAppM ``not_and_eq #[p, q]): ?m.1939(βmkAppM: Name β Array Expr β MetaM ExprmkAppM(βmkAppM ``not_and_eq #[p, q]): ?m.1939 ``not_and_eq: β (p q : Prop), (Β¬(p β§ q)) = (p β Β¬q)not_and_eq(βmkAppM ``not_and_eq #[p, q]): ?m.1939 #[p: Exprp(βmkAppM ``not_and_eq #[p, q]): ?m.1939, q: Exprq(βmkAppM ``not_and_eq #[p, q]): ?m.1939])
| true: Booltrue  => return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (mkOr: Expr β Expr β ExprmkOr (mkNot: Expr β ExprmkNot p: Exprp) (mkNot: Expr β ExprmkNot q: Exprq)) (βmkAppM ``not_and_or_eq #[p, q]): ?m.2211(βmkAppM: Name β Array Expr β MetaM ExprmkAppM(βmkAppM ``not_and_or_eq #[p, q]): ?m.2211 ``not_and_or_eq: β (p q : Prop), (Β¬(p β§ q)) = (Β¬p β¨ Β¬q)not_and_or_eq(βmkAppM ``not_and_or_eq #[p, q]): ?m.2211 #[p: Exprp(βmkAppM ``not_and_or_eq #[p, q]): ?m.2211, q: Exprq(βmkAppM ``not_and_or_eq #[p, q]): ?m.2211])
| (``Or: Name``Or: Prop β Prop β PropOr, #[p: Exprp, q: Exprq]) =>
return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (mkAnd: Expr β Expr β ExprmkAnd (mkNot: Expr β ExprmkNot p: Exprp) (mkNot: Expr β ExprmkNot q: Exprq)) (βmkAppM ``not_or_eq #[p, q]): ?m.2622(βmkAppM: Name β Array Expr β MetaM ExprmkAppM(βmkAppM ``not_or_eq #[p, q]): ?m.2622 ``not_or_eq: β (p q : Prop), (Β¬(p β¨ q)) = (Β¬p β§ Β¬q)not_or_eq(βmkAppM ``not_or_eq #[p, q]): ?m.2622 #[p: Exprp(βmkAppM ``not_or_eq #[p, q]): ?m.2622, q: Exprq(βmkAppM ``not_or_eq #[p, q]): ?m.2622])
| (``Eq: Name``Eq: {Ξ± : Sort u_1} β Ξ± β Ξ± β PropEq, #[_ty: Expr_ty, eβ: Expreβ, eβ: Expreβ]) =>
return Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit { expr := β mkAppM ``Ne #[eβ, eβ] }: Simp.Result{ expr := β mkAppM: Name β Array Expr β MetaM ExprmkAppM{ expr := β mkAppM ``Ne #[eβ, eβ] }: Simp.Result ``Ne: {Ξ± : Sort u} β Ξ± β Ξ± β PropNe{ expr := β mkAppM ``Ne #[eβ, eβ] }: Simp.Result #[eβ: Expreβ{ expr := β mkAppM ``Ne #[eβ, eβ] }: Simp.Result, eβ: Expreβ{ expr := β mkAppM ``Ne #[eβ, eβ] }: Simp.Result] }
| (``Ne: Name``Ne: {Ξ± : Sort u} β Ξ± β Ξ± β PropNe, #[_ty: Expr_ty, eβ: Expreβ, eβ: Expreβ]) =>
return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``Eq #[eβ, eβ]): ?m.3128(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``Eq #[eβ, eβ]): ?m.3128 ``Eq: {Ξ± : Sort u_1} β Ξ± β Ξ± β PropEq(β mkAppM ``Eq #[eβ, eβ]): ?m.3128 #[eβ: Expreβ(β mkAppM ``Eq #[eβ, eβ]): ?m.3128, eβ: Expreβ(β mkAppM ``Eq #[eβ, eβ]): ?m.3128]) (β mkAppM ``not_ne_eq #[eβ, eβ]): ?m.3196(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_ne_eq #[eβ, eβ]): ?m.3196 ``not_ne_eq: β {Ξ± : Sort u_1} (x y : Ξ±), (Β¬x β  y) = (x = y)not_ne_eq(β mkAppM ``not_ne_eq #[eβ, eβ]): ?m.3196 #[eβ: Expreβ(β mkAppM ``not_ne_eq #[eβ, eβ]): ?m.3196, eβ: Expreβ(β mkAppM ``not_ne_eq #[eβ, eβ]): ?m.3196])
| (``LE.le: Name``LE.le: {Ξ± : Type u} β [self : LE Ξ±] β Ξ± β Ξ± β PropLE.le, #[ty: Exprty, _inst: Expr_inst, eβ: Expreβ, eβ: Expreβ]) =>
let linOrd: ?m.3492linOrd β synthInstance?: Expr β optParam (Option Nat) none β MetaM (Option Expr)synthInstance? (β mkAppM ``LinearOrder #[ty]): ?m.3438(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LinearOrder #[ty]): ?m.3438 ``LinearOrder: Type u β Type uLinearOrder(β mkAppM ``LinearOrder #[ty]): ?m.3438 #[ty: Exprty(β mkAppM ``LinearOrder #[ty]): ?m.3438])
match linOrd: ?m.3492linOrd with
| some: {Ξ± : Type ?u.3494} β Ξ± β Option Ξ±some _ => return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``LT.lt #[eβ, eβ]): ?m.3575(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LT.lt #[eβ, eβ]): ?m.3575 ``LT.lt: {Ξ± : Type u} β [self : LT Ξ±] β Ξ± β Ξ± β PropLT.lt(β mkAppM ``LT.lt #[eβ, eβ]): ?m.3575 #[eβ: Expreβ(β mkAppM ``LT.lt #[eβ, eβ]): ?m.3575, eβ: Expreβ(β mkAppM ``LT.lt #[eβ, eβ]): ?m.3575]) (β mkAppM ``not_le_eq #[eβ, eβ]): ?m.3643(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_le_eq #[eβ, eβ]): ?m.3643 ``not_le_eq: β {Ξ² : Type u} [inst : LinearOrder Ξ²] (a b : Ξ²), (Β¬a β€ b) = (b < a)not_le_eq(β mkAppM ``not_le_eq #[eβ, eβ]): ?m.3643 #[eβ: Expreβ(β mkAppM ``not_le_eq #[eβ, eβ]): ?m.3643, eβ: Expreβ(β mkAppM ``not_le_eq #[eβ, eβ]): ?m.3643])
| none: {Ξ± : Type ?u.3754} β Option Ξ±none => return none: {Ξ± : Type ?u.3787} β Option Ξ±none
| (``LT.lt: Name``LT.lt: {Ξ± : Type u} β [self : LT Ξ±] β Ξ± β Ξ± β PropLT.lt, #[ty: Exprty, _inst: Expr_inst, eβ: Expreβ, eβ: Expreβ]) =>
let linOrd: ?m.4196linOrd β synthInstance?: Expr β optParam (Option Nat) none β MetaM (Option Expr)synthInstance? (β mkAppM ``LinearOrder #[ty]): ?m.4142(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LinearOrder #[ty]): ?m.4142 ``LinearOrder: Type u β Type uLinearOrder(β mkAppM ``LinearOrder #[ty]): ?m.4142 #[ty: Exprty(β mkAppM ``LinearOrder #[ty]): ?m.4142])
match linOrd: ?m.4196linOrd with
| some: {Ξ± : Type ?u.1136} β Ξ± β Option Ξ±some _ => return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``LE.le #[eβ, eβ]): ?m.4279(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LE.le #[eβ, eβ]): ?m.4279 ``LE.le: {Ξ± : Type u} β [self : LE Ξ±] β Ξ± β Ξ± β PropLE.le(β mkAppM ``LE.le #[eβ, eβ]): ?m.4279 #[eβ: Expreβ(β mkAppM ``LE.le #[eβ, eβ]): ?m.4279, eβ: Expreβ(β mkAppM ``LE.le #[eβ, eβ]): ?m.4279]) (β mkAppM ``not_lt_eq #[eβ, eβ]): ?m.4347(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_lt_eq #[eβ, eβ]): ?m.4347 ``not_lt_eq: β {Ξ² : Type u} [inst : LinearOrder Ξ²] (a b : Ξ²), (Β¬a < b) = (b β€ a)not_lt_eq(β mkAppM ``not_lt_eq #[eβ, eβ]): ?m.4347 #[eβ: Expreβ(β mkAppM ``not_lt_eq #[eβ, eβ]): ?m.4347, eβ: Expreβ(β mkAppM ``not_lt_eq #[eβ, eβ]): ?m.4347])
| none: {Ξ± : Type ?u.4514} β Option Ξ±none => return none: {Ξ± : Type ?u.4547} β Option Ξ±none
| (``GE.ge: Name``GE.ge: {Ξ± : Type u} β [inst : LE Ξ±] β Ξ± β Ξ± β PropGE.ge, #[ty: Exprty, _inst: Expr_inst, eβ: Expreβ, eβ: Expreβ]) =>
let linOrd: ?m.4810linOrd β synthInstance?: Expr β optParam (Option Nat) none β MetaM (Option Expr)synthInstance? (β mkAppM ``LinearOrder #[ty]): ?m.4756(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LinearOrder #[ty]): ?m.4756 ``LinearOrder: Type u β Type uLinearOrder(β mkAppM ``LinearOrder #[ty]): ?m.4756 #[ty: Exprty(β mkAppM ``LinearOrder #[ty]): ?m.4756])
match linOrd: ?m.4810linOrd with
| some: {Ξ± : Type ?u.4812} β Ξ± β Option Ξ±some _ => return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``LT.lt #[eβ, eβ]): ?m.4892(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LT.lt #[eβ, eβ]): ?m.4892 ``LT.lt: {Ξ± : Type u} β [self : LT Ξ±] β Ξ± β Ξ± β PropLT.lt(β mkAppM ``LT.lt #[eβ, eβ]): ?m.4892 #[eβ: Expreβ(β mkAppM ``LT.lt #[eβ, eβ]): ?m.4892, eβ: Expreβ(β mkAppM ``LT.lt #[eβ, eβ]): ?m.4892]) (β mkAppM ``not_ge_eq #[eβ, eβ]): ?m.4960(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_ge_eq #[eβ, eβ]): ?m.4960 ``not_ge_eq: β {Ξ² : Type u} [inst : LinearOrder Ξ²] (a b : Ξ²), (Β¬a β₯ b) = (a < b)not_ge_eq(β mkAppM ``not_ge_eq #[eβ, eβ]): ?m.4960 #[eβ: Expreβ(β mkAppM ``not_ge_eq #[eβ, eβ]): ?m.4960, eβ: Expreβ(β mkAppM ``not_ge_eq #[eβ, eβ]): ?m.4960])
| none: {Ξ± : Type ?u.5071} β Option Ξ±none => return none: {Ξ± : Type ?u.5104} β Option Ξ±none
| (``GT.gt: Name``GT.gt: {Ξ± : Type u} β [inst : LT Ξ±] β Ξ± β Ξ± β PropGT.gt, #[ty: Exprty, _inst: Expr_inst, eβ: Expreβ, eβ: Expreβ]) =>
let linOrd: ?m.5367linOrd β synthInstance?: Expr β optParam (Option Nat) none β MetaM (Option Expr)synthInstance? (β mkAppM ``LinearOrder #[ty]): ?m.5313(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LinearOrder #[ty]): ?m.5313 ``LinearOrder: Type u β Type uLinearOrder(β mkAppM ``LinearOrder #[ty]): ?m.5313 #[ty: Exprty(β mkAppM ``LinearOrder #[ty]): ?m.5313])
match linOrd: ?m.5367linOrd with
| some: {Ξ± : Type ?u.1204} β Ξ± β Option Ξ±some _ => return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``LE.le #[eβ, eβ]): ?m.5449(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``LE.le #[eβ, eβ]): ?m.5449 ``LE.le: {Ξ± : Type u} β [self : LE Ξ±] β Ξ± β Ξ± β PropLE.le(β mkAppM ``LE.le #[eβ, eβ]): ?m.5449 #[eβ: Expreβ(β mkAppM ``LE.le #[eβ, eβ]): ?m.5449, eβ: Expreβ(β mkAppM ``LE.le #[eβ, eβ]): ?m.5449]) (β mkAppM ``not_gt_eq #[eβ, eβ]): ?m.5517(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_gt_eq #[eβ, eβ]): ?m.5517 ``not_gt_eq: β {Ξ² : Type u} [inst : LinearOrder Ξ²] (a b : Ξ²), (Β¬a > b) = (a β€ b)not_gt_eq(β mkAppM ``not_gt_eq #[eβ, eβ]): ?m.5517 #[eβ: Expreβ(β mkAppM ``not_gt_eq #[eβ, eβ]): ?m.5517, eβ: Expreβ(β mkAppM ``not_gt_eq #[eβ, eβ]): ?m.5517])
| none: {Ξ± : Type ?u.1208} β Option Ξ±none => return none: {Ξ± : Type ?u.5661} β Option Ξ±none
| (``Exists: Name``Exists: {Ξ± : Sort u} β (Ξ± β Prop) β PropExists, #[_, .lam: Name β Expr β Expr β BinderInfo β Expr.lam n: Namen typ: Exprtyp bo: Exprbo bi: BinderInfobi]) =>
return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (.forallE: Name β Expr β Expr β BinderInfo β Expr.forallE n: Namen typ: Exprtyp (mkNot: Expr β ExprmkNot bo: Exprbo) bi: BinderInfobi)
(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863 ``not_exists_eq: β {Ξ± : Sort u_1} (s : Ξ± β Prop), (Β¬β x, s x) = β (x : Ξ±), Β¬s xnot_exists_eq(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863 #[.lam: Name β Expr β Expr β BinderInfo β Expr.lam(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863 n: Namen(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863 typ: Exprtyp(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863 bo: Exprbo(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863 bi: BinderInfobi(β mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863])
| (``Exists: Name``Exists: {Ξ± : Sort u} β (Ξ± β Prop) β PropExists, #[_, _]) =>
return none: {Ξ± : Type ?u.6035} β Option Ξ±none
| _ => match ex: Exprex with
| .forallE: Name β Expr β Expr β BinderInfo β Expr.forallE name: Namename ty: Exprty body: Exprbody binfo: BinderInfobinfo => do
if (β isProp ty): ?m.6127(β isProp: Expr β MetaM BoolisProp(β isProp ty): ?m.6127 ty: Exprty(β isProp ty): ?m.6127) then
return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``And #[ty, mkNot body]): ?m.6264(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``And #[ty, mkNot body]): ?m.6264 ``And: Prop β Prop β PropAnd(β mkAppM ``And #[ty, mkNot body]): ?m.6264 #[ty: Exprty(β mkAppM ``And #[ty, mkNot body]): ?m.6264, mkNot: Expr β ExprmkNot(β mkAppM ``And #[ty, mkNot body]): ?m.6264 body: Exprbody(β mkAppM ``And #[ty, mkNot body]): ?m.6264])
(β mkAppM ``not_implies_eq #[ty, body]): ?m.6332(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_implies_eq #[ty, body]): ?m.6332 ``not_implies_eq: β (p q : Prop), (Β¬(p β q)) = (p β§ Β¬q)not_implies_eq(β mkAppM ``not_implies_eq #[ty, body]): ?m.6332 #[ty: Exprty(β mkAppM ``not_implies_eq #[ty, body]): ?m.6332, body: Exprbody(β mkAppM ``not_implies_eq #[ty, body]): ?m.6332])
else
let body': Exprbody' : Expr: TypeExpr := .lam: Name β Expr β Expr β BinderInfo β Expr.lam name: Namename ty: Exprty (mkNot: Expr β ExprmkNot body: Exprbody) binfo: BinderInfobinfo
let body'': Exprbody'' : Expr: TypeExpr := .lam: Name β Expr β Expr β BinderInfo β Expr.lam name: Namename ty: Exprty body: Exprbody binfo: BinderInfobinfo
return mkSimpStep: Expr β Expr β Simp.StepmkSimpStep (β mkAppM ``Exists #[body']): ?m.6510(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``Exists #[body']): ?m.6510 ``Exists: {Ξ± : Sort u} β (Ξ± β Prop) β PropExists(β mkAppM ``Exists #[body']): ?m.6510 #[body': Exprbody'(β mkAppM ``Exists #[body']): ?m.6510]) (β mkAppM ``not_forall_eq #[body'']): ?m.6576(β mkAppM: Name β Array Expr β MetaM ExprmkAppM(β mkAppM ``not_forall_eq #[body'']): ?m.6576 ``not_forall_eq: β {Ξ± : Sort u_1} (s : Ξ± β Prop), (Β¬β (x : Ξ±), s x) = β x, Β¬s xnot_forall_eq(β mkAppM ``not_forall_eq #[body'']): ?m.6576 #[body'': Exprbody''(β mkAppM ``not_forall_eq #[body'']): ?m.6576])
| _ => return none: {Ξ± : Type ?u.6737} β Option Ξ±none

/-- Recursively push negations at the top level of the current expression. This is needed
to handle e.g. triple negation. -/
partial def transformNegation: Expr β SimpM Simp.SteptransformNegation (e: Expre : Expr: TypeExpr) : SimpM: Type β TypeSimpM Simp.Step: TypeSimp.Step := do
let Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit rβ: Simp.Resultrβ β transformNegationStep: Expr β SimpM (Option Simp.Step)transformNegationStep e: Expre | return Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit { expr := e: Expre }
match rβ: Simp.Resultrβ.proof?: Simp.Result β Option Exprproof? with
| none: {Ξ± : Type ?u.47269} β Option Ξ±none => return Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit rβ: Simp.Resultrβ
| some: {Ξ± : Type ?u.47271} β Ξ± β Option Ξ±some _ => do
let Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit rβ: Simp.Resultrβ β transformNegation: Expr β SimpM Simp.SteptransformNegation rβ: Simp.Resultrβ.expr: Simp.Result β Exprexpr | return Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit rβ: Simp.Resultrβ
return Simp.Step.visit: Simp.Result β Simp.StepSimp.Step.visit (β Simp.mkEqTrans rβ rβ): ?m.47728(β Simp.mkEqTrans: Simp.Result β Simp.Result β MetaM Simp.ResultSimp.mkEqTrans(β Simp.mkEqTrans rβ rβ): ?m.47728 rβ: Simp.Resultrβ(β Simp.mkEqTrans rβ rβ): ?m.47728 rβ: Simp.Resultrβ(β Simp.mkEqTrans rβ rβ): ?m.47728)

/-- Common entry point to `push_neg` as a conv. -/
def pushNegCore: Expr β MetaM Simp.ResultpushNegCore (tgt: Exprtgt : Expr: TypeExpr) : MetaM: Type β TypeMetaM Simp.Result: TypeSimp.Result := do
let myctx: Simp.Contextmyctx : Simp.Context: TypeSimp.Context :=
{ config := { eta := true: Booltrue },
simpTheorems := #[ ]: Array ?m.50503#[ ]
congrTheorems := (β getSimpCongrTheorems): ?m.50485(β getSimpCongrTheorems: MetaM SimpCongrTheoremsgetSimpCongrTheorems(β getSimpCongrTheorems): ?m.50485) }
(Β·.1): Simp.Result Γ Simp.UsedSimps β Simp.Result(Β·.1) <\$> Simp.main: Expr β
Simp.Context β
optParam Simp.UsedSimps β β
optParam Simp.Methods
{ pre := fun e => pure (Simp.Step.visit { expr := e, proof? := none, dischargeDepth := 0 }),
post := fun e => pure (Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }),
discharge? := fun x => pure none } β
MetaM (Simp.Result Γ Simp.UsedSimps)Simp.main tgt: Exprtgt myctx: Simp.Contextmyctx (methods := { pre := transformNegation: Expr β SimpM Simp.SteptransformNegation })

/--
Push negations into the conclusion of an expression.
For instance, an expression `Β¬ β x, β y, x β€ y` will be transformed by `push_neg` into
`β x, β y, y < x`. Variable names are conserved.
This tactic pushes negations inside expressions. For instance, given a hypothesis
```lean
| Β¬ β Ξ΅ > 0, β Ξ΄ > 0, β x, |x - xβ| β€ Ξ΄ β |f x - yβ| β€ Ξ΅)
```
writing `push_neg` will turn the target into
```lean
| β Ξ΅, Ξ΅ > 0 β§ β Ξ΄, Ξ΄ > 0 β (β x, |x - xβ| β€ Ξ΄ β§ Ξ΅ < |f x - yβ|),
```
(The pretty printer does *not* use the abreviations `β Ξ΄ > 0` and `β Ξ΅ > 0` but this issue
has nothing to do with `push_neg`).

Note that names are conserved by this tactic, contrary to what would happen with `simp`
using the relevant lemmas.

This tactic has two modes: in standard mode, it transforms `Β¬(p β§ q)` into `p β Β¬q`, whereas in
distrib mode it produces `Β¬p β¨ Β¬q`. To use distrib mode, use `set_option push_neg.use_distrib true`.
-/
syntax (name := pushNegConv: ParserDescrpushNegConv) "push_neg" : conv: Parser.Categoryconv

/-- Execute `push_neg` as a conv tactic. -/
@[tactic pushNegConv: ParserDescrpushNegConv] def elabPushNegConv: TacticelabPushNegConv : Tactic: TypeTactic := fun _: ?m.52081_ β¦ withMainContext: {Ξ± : Type} β TacticM Ξ± β TacticM Ξ±withMainContext do
Conv.applySimpResult: Simp.Result β TacticM UnitConv.applySimpResult (β pushNegCore (β instantiateMVars (β Conv.getLhs))): ?m.52499(β pushNegCore: Expr β MetaM Simp.ResultpushNegCore(β pushNegCore (β instantiateMVars (β Conv.getLhs))): ?m.52499 (β instantiateMVars (β Conv.getLhs)): ?m.52293(β instantiateMVars: {m : Type β Type} β [inst : Monad m] β [inst : MonadMCtx m] β Expr β m ExprinstantiateMVars(β instantiateMVars (β Conv.getLhs)): ?m.52293 (β Conv.getLhs): ?m.52159(β Conv.getLhs: TacticM ExprConv.getLhs(β Conv.getLhs): ?m.52159)(β instantiateMVars (β Conv.getLhs)): ?m.52293)(β pushNegCore (β instantiateMVars (β Conv.getLhs))): ?m.52499)

/--
The syntax is `#push_neg e`, where `e` is an expression,
which will print the `push_neg` form of `e`.

`#push_neg` understands local variables, so you can use them to introduce parameters.
-/
macro (name := pushNeg: ParserDescrpushNeg) tk: ?m.53406tk:"#push_neg " e: ?m.53397e:term: Parser.Categoryterm : command: Parser.Categorycommand => `(command: Parser.Categorycommand| #conv%\$tk: ?m.53406tk push_neg => \$e: ?m.53397e)

/-- Execute main loop of `push_neg` at the main goal. -/
def pushNegTarget: TacticM UnitpushNegTarget : TacticM: Type β TypeTacticM Unit: TypeUnit := withMainContext: {Ξ± : Type} β TacticM Ξ± β TacticM Ξ±withMainContext do
let goal: ?m.55296goal β getMainGoal: TacticM MVarIdgetMainGoal
let tgt: ?m.55636tgt β instantiateMVars: {m : Type β Type} β [inst : Monad m] β [inst : MonadMCtx m] β Expr β m ExprinstantiateMVars (β goal.getType): ?m.55519(β goal: ?m.55296goal(β goal.getType): ?m.55519.getType: MVarId β MetaM ExprgetType(β goal.getType): ?m.55519)
replaceMainGoal: List MVarId β TacticM UnitreplaceMainGoal [β applySimpResultToTarget goal tgt (β pushNegCore tgt)]: List ?m.55768[β applySimpResultToTarget: MVarId β Expr β Simp.Result β MetaM MVarIdapplySimpResultToTarget[β applySimpResultToTarget goal tgt (β pushNegCore tgt)]: List ?m.55768 goal: ?m.55296goal[β applySimpResultToTarget goal tgt (β pushNegCore tgt)]: List ?m.55768 tgt: ?m.55636tgt[β applySimpResultToTarget goal tgt (β pushNegCore tgt)]: List ?m.55768 (β pushNegCore tgt): ?m.55690(β pushNegCore: Expr β MetaM Simp.ResultpushNegCore(β pushNegCore tgt): ?m.55690 tgt: ?m.55636tgt(β pushNegCore tgt): ?m.55690)[β applySimpResultToTarget goal tgt (β pushNegCore tgt)]: List ?m.55768]

/-- Execute main loop of `push_neg` at a local hypothesis. -/
def pushNegLocalDecl: FVarId β TacticM UnitpushNegLocalDecl (fvarId: FVarIdfvarId : FVarId: TypeFVarId): TacticM: Type β TypeTacticM Unit: TypeUnit := withMainContext: {Ξ± : Type} β TacticM Ξ± β TacticM Ξ±withMainContext do
let ldecl: ?m.57143ldecl β fvarId: FVarIdfvarId.getDecl: FVarId β MetaM LocalDeclgetDecl
if ldecl: ?m.57143ldecl.isAuxDecl: LocalDecl β BoolisAuxDecl then return: ?m.57249 ?m.57251return
let tgt: ?m.57540tgt β instantiateMVars: {m : Type β Type} β [inst : Monad m] β [inst : MonadMCtx m] β Expr β m ExprinstantiateMVars ldecl: ?m.57143ldecl.type: LocalDecl β Exprtype
let goal: ?m.57588goal β getMainGoal: TacticM MVarIdgetMainGoal
let myres: ?m.57642myres β pushNegCore: Expr β MetaM Simp.ResultpushNegCore tgt: ?m.57540tgt
let some: {Ξ± : Type ?u.57737} β Ξ± β Option Ξ±some (_, newGoal: MVarIdnewGoal) β applySimpResultToLocalDecl: MVarId β FVarId β Simp.Result β Bool β MetaM (Option (FVarId Γ MVarId))applySimpResultToLocalDecl goal: ?m.57588goal fvarId: FVarIdfvarId myres: ?m.57642myres False: PropFalse | failure: {f : Type ?u.57803 β Type ?u.57802} β [self : Alternative f] β {Ξ± : Type ?u.57803} β f Ξ±failure
replaceMainGoal: List MVarId β TacticM UnitreplaceMainGoal [newGoal: MVarIdnewGoal]

/--
Push negations into the conclusion of a hypothesis.
For instance, a hypothesis `h : Β¬ β x, β y, x β€ y` will be transformed by `push_neg at h` into
`h : β x, β y, y < x`. Variable names are conserved.
This tactic pushes negations inside expressions. For instance, given a hypothesis
```lean
h : Β¬ β Ξ΅ > 0, β Ξ΄ > 0, β x, |x - xβ| β€ Ξ΄ β |f x - yβ| β€ Ξ΅)
```
writing `push_neg at h` will turn `h` into
```lean
h : β Ξ΅, Ξ΅ > 0 β§ β Ξ΄, Ξ΄ > 0 β (β x, |x - xβ| β€ Ξ΄ β§ Ξ΅ < |f x - yβ|),
```
(The pretty printer does *not* use the abreviations `β Ξ΄ > 0` and `β Ξ΅ > 0` but this issue
has nothing to do with `push_neg`).

Note that names are conserved by this tactic, contrary to what would happen with `simp`
using the relevant lemmas. One can also use this tactic at the goal using `push_neg`,
at every hypothesis and the goal using `push_neg at *` or at selected hypotheses and the goal
using say `push_neg at h h' β’` as usual.

This tactic has two modes: in standard mode, it transforms `Β¬(p β§ q)` into `p β Β¬q`, whereas in
distrib mode it produces `Β¬p β¨ Β¬q`. To use distrib mode, use `set_option push_neg.use_distrib true`.
-/
elab "push_neg" loc: ?m.60488loc:(ppSpace: Parser.ParserppSpace location: ParserDescrlocation)? : tactic: Parser.Categorytactic =>
let loc: ?m.60507loc := (loc: ?m.60488loc.map: {Ξ± : Type ?u.60509} β {Ξ² : Type ?u.60508} β (Ξ± β Ξ²) β Option Ξ± β Option Ξ²map expandLocation: Syntax β LocationexpandLocation).getD: {Ξ± : Type ?u.60666} β Option Ξ± β Ξ± β Ξ±getD (.targets: Array Syntax β Bool β Location.targets #[]: Array ?m.60672#[] true: Booltrue)
withLocation: Location β (FVarId β TacticM Unit) β TacticM Unit β (MVarId β TacticM Unit) β TacticM UnitwithLocation loc: ?m.60507loc
pushNegLocalDecl: FVarId β TacticM UnitpushNegLocalDecl
pushNegTarget: TacticM UnitpushNegTarget
(fun _: ?m.60706_ β¦ logInfo: {m : Type β Type} β
[inst : Monad m] β [inst : MonadLog m] β [inst : AddMessageContext m] β [inst : MonadOptions m] β MessageData β m UnitlogInfo "push_neg couldn't find a negation to push": String"push_neg couldn't find a negation to push")
```