/-
Copyright (c) 2019 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot, Simon Hudon, Alice Laroche, Frédéric Dupuis, Jireh Loreaux
-/

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: Prop
p 
q: Prop
q : 
Prop: Type
Prop) (
s: α → Prop
s : 
α: ?m.766
α → 
Prop: Type
Prop)

theorem 
not_not_eq: (¬¬p) = p
not_not_eq : (¬ ¬ 
p: Prop
p) = 
p: Prop
p := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_not: ∀ {a : Prop}, ¬¬a ↔ a
not_not
theorem 
not_and_eq: (¬(p ∧ q)) = (p → ¬q)
not_and_eq : (¬ (
p: Prop
p ∧ 
q: Prop
q)) = (
p: Prop
p → ¬ 
q: Prop
q) := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_and: ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
not_and
theorem 
not_and_or_eq: (¬(p ∧ q)) = (¬p ∨ ¬q)
not_and_or_eq : (¬ (
p: Prop
p ∧ 
q: Prop
q)) = (¬ 
p: Prop
p ∨ ¬ 
q: Prop
q) := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_and_or: ∀ {a b : Prop}, ¬(a ∧ b) ↔ ¬a ∨ ¬b
not_and_or
theorem 
not_or_eq: (¬(p ∨ q)) = (¬p ∧ ¬q)
not_or_eq : (¬ (
p: Prop
p ∨ 
q: Prop
q)) = (¬ 
p: Prop
p ∧ ¬ 
q: Prop
q) := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬q
not_or
theorem 
not_forall_eq: ∀ {α : Sort u_1} (s : α → Prop), (¬∀ (x : α), s x) = ∃ x, ¬s x
not_forall_eq : (¬ ∀ 
x: ?m.183
x, 
s: α → Prop
s 
x: ?m.183
x) = (∃ 
x: ?m.190
x, ¬ 
s: α → Prop
s 
x: ?m.190
x) := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_forall: ∀ {α : Sort ?u.201} {p : α → Prop}, (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
not_forall
theorem 
not_exists_eq: (¬∃ x, s x) = ∀ (x : α), ¬s x
not_exists_eq : (¬ ∃ 
x: ?m.241
x, 
s: α → Prop
s 
x: ?m.241
x) = (∀ 
x: ?m.246
x, ¬ 
s: α → Prop
s 
x: ?m.246
x) := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_exists: ∀ {α : Sort ?u.257} {p : α → Prop}, (¬∃ x, p x) ↔ ∀ (x : α), ¬p x
not_exists
theorem 
not_implies_eq: (¬(p → q)) = (p ∧ ¬q)
not_implies_eq : (¬ (
p: Prop
p → 
q: Prop
q)) = (
p: Prop
p ∧ ¬ 
q: Prop
q) := 
propext: ∀ {a b : Prop}, (a ↔ b) → a = b
propext 
not_imp: ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
not_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 = b
ne_eq 
x: α
x 
y: α
y ▸ 
not_not_eq: ∀ (p : Prop), (¬¬p) = p
not_not_eq 
_: Prop
_

variable {
β: Type u
β : 
Type u: Type (u+1)
Type u} [
LinearOrder: Type ?u.385 → Type ?u.385
LinearOrder 
β: 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 = b
propext 
not_le: ∀ {α : Type ?u.461} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_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 = b
propext 
not_lt: ∀ {α : Type ?u.554} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_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 = b
propext 
not_le: ∀ {α : Type ?u.647} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_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 = b
propext 
not_lt: ∀ {α : Type ?u.740} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_lt

/-- Make `push_neg` use `not_and_or` rather than the default `not_and`. -/
register_option 
push_neg.use_distrib: Lean.Option Bool
push_neg.use_distrib : 
Bool: Type
Bool :=
  { defValue := 
false: Bool
false
    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: Expr
e : 
Expr: Type
Expr) : 
SimpM: Type → Type
SimpM (
Option: Type ?u.925 → Type ?u.925
Option 
Simp.Step: Type
Simp.Step) := do
  let 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep (
e: Expr
e : 
Expr: Type
Expr) (
pf: Expr
pf : 
Expr: Type
Expr) : 
Simp.Step: Type
Simp.Step :=
    
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit { expr := 
e: Expr
e, proof? := 
some: {α : Type ?u.1255} → α → Option α
some 
pf: Expr
pf }
  let 
e_whnf: ?m.1407
e_whnf ← 
whnfR: Expr → MetaM Expr
whnfR 
e: Expr
e
  let 
some: {α : Type ?u.967} → α → Option α
some 
ex: Expr
ex := 
e_whnf: ?m.1407
e_whnf.
not?: Expr → Option Expr
not? | return 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit { expr := 
e: Expr
e }
  match 
ex: Expr
ex.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``Not: Name
``
Not: Prop → Prop
Not, #[
e: Expr
e]) =>
      return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
e: Expr
e 
(← mkAppM ``not_not_eq #[e]): ?m.1533
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``not_not_eq #[e]): ?m.1533
 ``
not_not_eq: ∀ (p : Prop), (¬¬p) = p
not_not_eq
(← mkAppM ``not_not_eq #[e]): ?m.1533
 #[
e: Expr
e
(← mkAppM ``not_not_eq #[e]): ?m.1533
])
  | (
``And: Name
``
And: Prop → Prop → Prop
And, #[
p: Expr
p, 
q: Expr
q]) =>
      match ← 
getBoolOption: {m : Type → Type} → [inst : Monad m] → [inst : MonadOptions m] → Name → optParam Bool false → m Bool
getBoolOption 
`push_neg.use_distrib: Name
`push_neg.use_distrib with
      | 
false: Bool
false => return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep (
.forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE 
`_: Name
`_ 
p: Expr
p (
mkNot: Expr → Expr
mkNot 
q: Expr
q) 
default: {α : Sort ?u.1966} → [self : Inhabited α] → α
default) 
(←mkAppM ``not_and_eq #[p, q]): ?m.1939
(←
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(←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: Expr
p
(←mkAppM ``not_and_eq #[p, q]): ?m.1939
, 
q: Expr
q
(←mkAppM ``not_and_eq #[p, q]): ?m.1939
])
      | 
true: Bool
true  => return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep (
mkOr: Expr → Expr → Expr
mkOr (
mkNot: Expr → Expr
mkNot 
p: Expr
p) (
mkNot: Expr → Expr
mkNot 
q: Expr
q)) 
(←mkAppM ``not_and_or_eq #[p, q]): ?m.2211
(←
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(←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: Expr
p
(←mkAppM ``not_and_or_eq #[p, q]): ?m.2211
, 
q: Expr
q
(←mkAppM ``not_and_or_eq #[p, q]): ?m.2211
])
  | (
``Or: Name
``
Or: Prop → Prop → Prop
Or, #[
p: Expr
p, 
q: Expr
q]) =>
      return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep (
mkAnd: Expr → Expr → Expr
mkAnd (
mkNot: Expr → Expr
mkNot 
p: Expr
p) (
mkNot: Expr → Expr
mkNot 
q: Expr
q)) 
(←mkAppM ``not_or_eq #[p, q]): ?m.2622
(←
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(←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: Expr
p
(←mkAppM ``not_or_eq #[p, q]): ?m.2622
, 
q: Expr
q
(←mkAppM ``not_or_eq #[p, q]): ?m.2622
])
  | (
``Eq: Name
``
Eq: {α : Sort u_1} → α → α → Prop
Eq, #[
_ty: Expr
_ty, 
e₁: Expr
e₁, 
e₂: Expr
e₂]) =>
      return 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit 
{ expr := ← mkAppM ``Ne #[e₁, e₂] }: Simp.Result
{ expr := ← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
{ expr := ← mkAppM ``Ne #[e₁, e₂] }: Simp.Result
 ``
Ne: {α : Sort u} → α → α → Prop
Ne
{ expr := ← mkAppM ``Ne #[e₁, e₂] }: Simp.Result
 #[
e₁: Expr
e₁
{ expr := ← mkAppM ``Ne #[e₁, e₂] }: Simp.Result
, 
e₂: Expr
e₂
{ expr := ← mkAppM ``Ne #[e₁, e₂] }: Simp.Result
] }
  | (
``Ne: Name
``
Ne: {α : Sort u} → α → α → Prop
Ne, #[
_ty: Expr
_ty, 
e₁: Expr
e₁, 
e₂: Expr
e₂]) =>
      return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``Eq #[e₁, e₂]): ?m.3128
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``Eq #[e₁, e₂]): ?m.3128
 ``
Eq: {α : Sort u_1} → α → α → Prop
Eq
(← mkAppM ``Eq #[e₁, e₂]): ?m.3128
 #[
e₁: Expr
e₁
(← mkAppM ``Eq #[e₁, e₂]): ?m.3128
, 
e₂: Expr
e₂
(← mkAppM ``Eq #[e₁, e₂]): ?m.3128
]) 
(← mkAppM ``not_ne_eq #[e₁, e₂]): ?m.3196
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← 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₁: Expr
e₁
(← mkAppM ``not_ne_eq #[e₁, e₂]): ?m.3196
, 
e₂: Expr
e₂
(← mkAppM ``not_ne_eq #[e₁, e₂]): ?m.3196
])
  | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, #[
ty: Expr
ty, 
_inst: Expr
_inst, 
e₁: Expr
e₁, 
e₂: Expr
e₂]) =>
      let 
linOrd: ?m.3492
linOrd ← 
synthInstance?: Expr → optParam (Option Nat) none → MetaM (Option Expr)
synthInstance? 
(← mkAppM ``LinearOrder #[ty]): ?m.3438
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LinearOrder #[ty]): ?m.3438
 ``
LinearOrder: Type u → Type u
LinearOrder
(← mkAppM ``LinearOrder #[ty]): ?m.3438
 #[
ty: Expr
ty
(← mkAppM ``LinearOrder #[ty]): ?m.3438
])
      match 
linOrd: ?m.3492
linOrd with
      | 
some: {α : Type ?u.3494} → α → Option α
some _ => return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``LT.lt #[e₂, e₁]): ?m.3575
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LT.lt #[e₂, e₁]): ?m.3575
 ``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt
(← mkAppM ``LT.lt #[e₂, e₁]): ?m.3575
 #[
e₂: Expr
e₂
(← mkAppM ``LT.lt #[e₂, e₁]): ?m.3575
, 
e₁: Expr
e₁
(← mkAppM ``LT.lt #[e₂, e₁]): ?m.3575
]) 
(← mkAppM ``not_le_eq #[e₁, e₂]): ?m.3643
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← 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₁: Expr
e₁
(← mkAppM ``not_le_eq #[e₁, e₂]): ?m.3643
, 
e₂: Expr
e₂
(← 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 α] → α → α → Prop
LT.lt, #[
ty: Expr
ty, 
_inst: Expr
_inst, 
e₁: Expr
e₁, 
e₂: Expr
e₂]) =>
      let 
linOrd: ?m.4196
linOrd ← 
synthInstance?: Expr → optParam (Option Nat) none → MetaM (Option Expr)
synthInstance? 
(← mkAppM ``LinearOrder #[ty]): ?m.4142
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LinearOrder #[ty]): ?m.4142
 ``
LinearOrder: Type u → Type u
LinearOrder
(← mkAppM ``LinearOrder #[ty]): ?m.4142
 #[
ty: Expr
ty
(← mkAppM ``LinearOrder #[ty]): ?m.4142
])
      match 
linOrd: ?m.4196
linOrd with
      | 
some: {α : Type ?u.1136} → α → Option α
some _ => return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``LE.le #[e₂, e₁]): ?m.4279
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LE.le #[e₂, e₁]): ?m.4279
 ``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le
(← mkAppM ``LE.le #[e₂, e₁]): ?m.4279
 #[
e₂: Expr
e₂
(← mkAppM ``LE.le #[e₂, e₁]): ?m.4279
, 
e₁: Expr
e₁
(← mkAppM ``LE.le #[e₂, e₁]): ?m.4279
]) 
(← mkAppM ``not_lt_eq #[e₁, e₂]): ?m.4347
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← 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₁: Expr
e₁
(← mkAppM ``not_lt_eq #[e₁, e₂]): ?m.4347
, 
e₂: Expr
e₂
(← 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 α] → α → α → Prop
GE.ge, #[
ty: Expr
ty, 
_inst: Expr
_inst, 
e₁: Expr
e₁, 
e₂: Expr
e₂]) =>
      let 
linOrd: ?m.4810
linOrd ← 
synthInstance?: Expr → optParam (Option Nat) none → MetaM (Option Expr)
synthInstance? 
(← mkAppM ``LinearOrder #[ty]): ?m.4756
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LinearOrder #[ty]): ?m.4756
 ``
LinearOrder: Type u → Type u
LinearOrder
(← mkAppM ``LinearOrder #[ty]): ?m.4756
 #[
ty: Expr
ty
(← mkAppM ``LinearOrder #[ty]): ?m.4756
])
      match 
linOrd: ?m.4810
linOrd with
      | 
some: {α : Type ?u.4812} → α → Option α
some _ => return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``LT.lt #[e₁, e₂]): ?m.4892
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LT.lt #[e₁, e₂]): ?m.4892
 ``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt
(← mkAppM ``LT.lt #[e₁, e₂]): ?m.4892
 #[
e₁: Expr
e₁
(← mkAppM ``LT.lt #[e₁, e₂]): ?m.4892
, 
e₂: Expr
e₂
(← mkAppM ``LT.lt #[e₁, e₂]): ?m.4892
]) 
(← mkAppM ``not_ge_eq #[e₁, e₂]): ?m.4960
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← 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₁: Expr
e₁
(← mkAppM ``not_ge_eq #[e₁, e₂]): ?m.4960
, 
e₂: Expr
e₂
(← 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 α] → α → α → Prop
GT.gt, #[
ty: Expr
ty, 
_inst: Expr
_inst, 
e₁: Expr
e₁, 
e₂: Expr
e₂]) =>
      let 
linOrd: ?m.5367
linOrd ← 
synthInstance?: Expr → optParam (Option Nat) none → MetaM (Option Expr)
synthInstance? 
(← mkAppM ``LinearOrder #[ty]): ?m.5313
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LinearOrder #[ty]): ?m.5313
 ``
LinearOrder: Type u → Type u
LinearOrder
(← mkAppM ``LinearOrder #[ty]): ?m.5313
 #[
ty: Expr
ty
(← mkAppM ``LinearOrder #[ty]): ?m.5313
])
      match 
linOrd: ?m.5367
linOrd with
      | 
some: {α : Type ?u.1204} → α → Option α
some _ => return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``LE.le #[e₁, e₂]): ?m.5449
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``LE.le #[e₁, e₂]): ?m.5449
 ``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le
(← mkAppM ``LE.le #[e₁, e₂]): ?m.5449
 #[
e₁: Expr
e₁
(← mkAppM ``LE.le #[e₁, e₂]): ?m.5449
, 
e₂: Expr
e₂
(← mkAppM ``LE.le #[e₁, e₂]): ?m.5449
]) 
(← mkAppM ``not_gt_eq #[e₁, e₂]): ?m.5517
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← 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₁: Expr
e₁
(← mkAppM ``not_gt_eq #[e₁, e₂]): ?m.5517
, 
e₂: Expr
e₂
(← 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) → Prop
Exists, #[_, 
.lam: Name → Expr → Expr → BinderInfo → Expr
.lam 
n: Name
n 
typ: Expr
typ 
bo: Expr
bo 
bi: BinderInfo
bi]) =>
      return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep (
.forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE 
n: Name
n 
typ: Expr
typ (
mkNot: Expr → Expr
mkNot 
bo: Expr
bo) 
bi: BinderInfo
bi)
                        
(← mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863
 ``
not_exists_eq: ∀ {α : Sort u_1} (s : α → Prop), (¬∃ x, s x) = ∀ (x : α), ¬s x
not_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: Name
n
(← mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863
 
typ: Expr
typ
(← mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863
 
bo: Expr
bo
(← mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863
 
bi: BinderInfo
bi
(← mkAppM ``not_exists_eq #[.lam n typ bo bi]): ?m.5863
])
  | (
``Exists: Name
``
Exists: {α : Sort u} → (α → Prop) → Prop
Exists, #[_, _]) =>
      return 
none: {α : Type ?u.6035} → Option α
none
  | _ => match 
ex: Expr
ex with
          | 
.forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE 
name: Name
name 
ty: Expr
ty 
body: Expr
body 
binfo: BinderInfo
binfo => do
              if 
(← isProp ty): ?m.6127
(← 
isProp: Expr → MetaM Bool
isProp
(← isProp ty): ?m.6127
 
ty: Expr
ty
(← isProp ty): ?m.6127
) then
                return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``And #[ty, mkNot body]): ?m.6264
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``And #[ty, mkNot body]): ?m.6264
 ``
And: Prop → Prop → Prop
And
(← mkAppM ``And #[ty, mkNot body]): ?m.6264
 #[
ty: Expr
ty
(← mkAppM ``And #[ty, mkNot body]): ?m.6264
, 
mkNot: Expr → Expr
mkNot
(← mkAppM ``And #[ty, mkNot body]): ?m.6264
 
body: Expr
body
(← mkAppM ``And #[ty, mkNot body]): ?m.6264
])
                  
(← mkAppM ``not_implies_eq #[ty, body]): ?m.6332
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← 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: Expr
ty
(← mkAppM ``not_implies_eq #[ty, body]): ?m.6332
, 
body: Expr
body
(← mkAppM ``not_implies_eq #[ty, body]): ?m.6332
])
              else
                let 
body': Expr
body' : 
Expr: Type
Expr := 
.lam: Name → Expr → Expr → BinderInfo → Expr
.lam 
name: Name
name 
ty: Expr
ty (
mkNot: Expr → Expr
mkNot 
body: Expr
body) 
binfo: BinderInfo
binfo
                let 
body'': Expr
body'' : 
Expr: Type
Expr := 
.lam: Name → Expr → Expr → BinderInfo → Expr
.lam 
name: Name
name 
ty: Expr
ty 
body: Expr
body 
binfo: BinderInfo
binfo
                return 
mkSimpStep: Expr → Expr → Simp.Step
mkSimpStep 
(← mkAppM ``Exists #[body']): ?m.6510
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``Exists #[body']): ?m.6510
 ``
Exists: {α : Sort u} → (α → Prop) → Prop
Exists
(← mkAppM ``Exists #[body']): ?m.6510
 #[
body': Expr
body'
(← mkAppM ``Exists #[body']): ?m.6510
]) 
(← mkAppM ``not_forall_eq #[body'']): ?m.6576
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``not_forall_eq #[body'']): ?m.6576
 ``
not_forall_eq: ∀ {α : Sort u_1} (s : α → Prop), (¬∀ (x : α), s x) = ∃ x, ¬s x
not_forall_eq
(← mkAppM ``not_forall_eq #[body'']): ?m.6576
 #[
body'': Expr
body''
(← 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.Step
transformNegation (
e: Expr
e : 
Expr: Type
Expr) : 
SimpM: Type → Type
SimpM 
Simp.Step: Type
Simp.Step := do
  let 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit 
r₁: Simp.Result
r₁ ← 
transformNegationStep: Expr → SimpM (Option Simp.Step)
transformNegationStep 
e: Expr
e | return 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit { expr := 
e: Expr
e }
  match 
r₁: Simp.Result
r₁.
proof?: Simp.Result → Option Expr
proof? with
  | 
none: {α : Type ?u.47269} → Option α
none => return 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit 
r₁: Simp.Result
r₁
  | 
some: {α : Type ?u.47271} → α → Option α
some _ => do
      let 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit 
r₂: Simp.Result
r₂ ← 
transformNegation: Expr → SimpM Simp.Step
transformNegation 
r₁: Simp.Result
r₁.
expr: Simp.Result → Expr
expr | return 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit 
r₁: Simp.Result
r₁
      return 
Simp.Step.visit: Simp.Result → Simp.Step
Simp.Step.visit 
(← Simp.mkEqTrans r₁ r₂): ?m.47728
(← 
Simp.mkEqTrans: Simp.Result → Simp.Result → MetaM Simp.Result
Simp.mkEqTrans
(← Simp.mkEqTrans r₁ r₂): ?m.47728
 
r₁: Simp.Result
r₁
(← Simp.mkEqTrans r₁ r₂): ?m.47728
 
r₂: Simp.Result
r₂
(← Simp.mkEqTrans r₁ r₂): ?m.47728
)

/-- Common entry point to `push_neg` as a conv. -/
def 
pushNegCore: Expr → MetaM Simp.Result
pushNegCore (
tgt: Expr
tgt : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Simp.Result: Type
Simp.Result := do
  let 
myctx: Simp.Context
myctx : 
Simp.Context: Type
Simp.Context :=
    { config := { eta := 
true: Bool
true },
      simpTheorems := 
#[ ]: Array ?m.50503
#[ ]
      congrTheorems := 
(← getSimpCongrTheorems): ?m.50485
(← 
getSimpCongrTheorems: MetaM SimpCongrTheorems
getSimpCongrTheorems
(← 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: Expr
tgt 
myctx: Simp.Context
myctx (methods := { pre := 
transformNegation: Expr → SimpM Simp.Step
transformNegation })

/--
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: ParserDescr
pushNegConv) "push_neg" : 
conv: Parser.Category
conv

/-- Execute `push_neg` as a conv tactic. -/
@[tactic 
pushNegConv: ParserDescr
pushNegConv] def 
elabPushNegConv: Tactic
elabPushNegConv : 
Tactic: Type
Tactic := fun 
_: ?m.52081
_ ↦ 
withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  
Conv.applySimpResult: Simp.Result → TacticM Unit
Conv.applySimpResult 
(← pushNegCore (← instantiateMVars (← Conv.getLhs))): ?m.52499
(← 
pushNegCore: Expr → MetaM Simp.Result
pushNegCore
(← pushNegCore (← instantiateMVars (← Conv.getLhs))): ?m.52499
 
(← instantiateMVars (← Conv.getLhs)): ?m.52293
(← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
(← instantiateMVars (← Conv.getLhs)): ?m.52293
 
(← Conv.getLhs): ?m.52159
(← 
Conv.getLhs: TacticM Expr
Conv.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: ParserDescr
pushNeg) 
tk: ?m.53406
tk:"#push_neg " 
e: ?m.53397
e:
term: Parser.Category
term : 
command: Parser.Category
command => `(
command: Parser.Category
command| #conv%$
tk: ?m.53406
tk push_neg => $
e: ?m.53397
e)

/-- Execute main loop of `push_neg` at the main goal. -/
def 
pushNegTarget: TacticM Unit
pushNegTarget : 
TacticM: Type → Type
TacticM 
Unit: Type
Unit := 
withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  let 
goal: ?m.55296
goal ← 
getMainGoal: TacticM MVarId
getMainGoal
  let 
tgt: ?m.55636
tgt ← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars 
(← goal.getType): ?m.55519
(← 
goal: ?m.55296
goal
(← goal.getType): ?m.55519
.
getType: MVarId → MetaM Expr
getType
(← goal.getType): ?m.55519
)
  
replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal 
[← applySimpResultToTarget goal tgt (← pushNegCore tgt)]: List ?m.55768
[← 
applySimpResultToTarget: MVarId → Expr → Simp.Result → MetaM MVarId
applySimpResultToTarget
[← applySimpResultToTarget goal tgt (← pushNegCore tgt)]: List ?m.55768
 
goal: ?m.55296
goal
[← applySimpResultToTarget goal tgt (← pushNegCore tgt)]: List ?m.55768
 
tgt: ?m.55636
tgt
[← applySimpResultToTarget goal tgt (← pushNegCore tgt)]: List ?m.55768
 
(← pushNegCore tgt): ?m.55690
(← 
pushNegCore: Expr → MetaM Simp.Result
pushNegCore
(← pushNegCore tgt): ?m.55690
 
tgt: ?m.55636
tgt
(← 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 Unit
pushNegLocalDecl (
fvarId: FVarId
fvarId : 
FVarId: Type
FVarId): 
TacticM: Type → Type
TacticM 
Unit: Type
Unit := 
withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  let 
ldecl: ?m.57143
ldecl ← 
fvarId: FVarId
fvarId.
getDecl: FVarId → MetaM LocalDecl
getDecl
  if 
ldecl: ?m.57143
ldecl.
isAuxDecl: LocalDecl → Bool
isAuxDecl then 
return: ?m.57249 ?m.57251
return
  let 
tgt: ?m.57540
tgt ← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars 
ldecl: ?m.57143
ldecl.
type: LocalDecl → Expr
type
  let 
goal: ?m.57588
goal ← 
getMainGoal: TacticM MVarId
getMainGoal
  let 
myres: ?m.57642
myres ← 
pushNegCore: Expr → MetaM Simp.Result
pushNegCore 
tgt: ?m.57540
tgt
  let 
some: {α : Type ?u.57737} → α → Option α
some (_, 
newGoal: MVarId
newGoal) ← 
applySimpResultToLocalDecl: MVarId → FVarId → Simp.Result → Bool → MetaM (Option (FVarId × MVarId))
applySimpResultToLocalDecl 
goal: ?m.57588
goal 
fvarId: FVarId
fvarId 
myres: ?m.57642
myres 
False: Prop
False | 
failure: {f : Type ?u.57803 → Type ?u.57802} → [self : Alternative f] → {α : Type ?u.57803} → f α
failure
  
replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal [
newGoal: MVarId
newGoal]

/--
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.60488
loc:(
ppSpace: Parser.Parser
ppSpace 
location: ParserDescr
location)? : 
tactic: Parser.Category
tactic =>
  let 
loc: ?m.60507
loc := (
loc: ?m.60488
loc.
map: {α : Type ?u.60509} → {β : Type ?u.60508} → (α → β) → Option α → Option β
map 
expandLocation: Syntax → Location
expandLocation).
getD: {α : Type ?u.60666} → Option α → α → α
getD (
.targets: Array Syntax → Bool → Location
.targets 
#[]: Array ?m.60672
#[] 
true: Bool
true)
  
withLocation: Location → (FVarId → TacticM Unit) → TacticM Unit → (MVarId → TacticM Unit) → TacticM Unit
withLocation 
loc: ?m.60507
loc
    
pushNegLocalDecl: FVarId → TacticM Unit
pushNegLocalDecl
    
pushNegTarget: TacticM Unit
pushNegTarget
    (fun 
_: ?m.60706
_ ↦ 
logInfo: {m : Type → Type} →
  [inst : Monad m] → [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → MessageData → m Unit
logInfo 
"push_neg couldn't find a negation to push": String
"push_neg couldn't find a negation to push")