A tactic pushing negations inwards while keeping names

push_neg.lean

import tactic.interactive
import algebra.order



open tactic expr

namespace push_neg
section

universe u
variable  {α : Sort u}
variables (p q : Prop)
variable  (s : α → Prop)

local attribute [instance] classical.prop_decidable
theorem not_not_eq : (¬ ¬ p) = p := propext not_not
theorem not_and_eq : (¬ (p ∧ q)) = (¬ p ∨ ¬ q) := propext not_and_distrib
theorem not_or_eq : (¬ (p ∨ q)) = (¬ p ∧ ¬ q) := propext not_or_distrib
theorem not_forall_eq : (¬ ∀ x, s x) = (∃ x, ¬ s x) := propext not_forall
theorem not_exists_eq : (¬ ∃ x, s x) = (∀ x, ¬ s x) := propext not_exists
theorem not_implies_eq : (¬ (p → q)) = (p ∧ ¬ q) := propext not_imp

theorem classical.implies_iff_not_or : (p → q) ↔ (¬ p ∨ q) := imp_iff_not_or


theorem not_eq (a b : α) : (¬ a = b) ↔ (a ≠ b) := iff.rfl

variable  {β : Type u}
variable [linear_order β]
theorem not_le_eq (a b : β) : (¬ (a ≤ b)) = (b < a) := propext not_le
theorem not_lt_eq (a b : β) : (¬ (a < b)) = (b ≤ a) := propext not_lt
end

meta def whnf_reducible (e : expr) : tactic expr := whnf e reducible

private meta def transform_negation_step (e : expr) :
  tactic (option (expr × expr)) :=
do e ← whnf_reducible e,
   match e with
   | `(¬ %%ne) :=
      (do ne ← whnf_reducible ne,
      match ne with
      | `(¬ %%a)      := do pr ← mk_app ``not_not_eq [a],
                            return (some (a, pr))
      | `(%%a ∧ %%b)  := do pr ← mk_app ``not_and_eq [a, b],
                            return (some (`(¬ %%a ∨ ¬ %%b), pr))
      | `(%%a ∨ %%b)  := do pr ← mk_app ``not_or_eq [a, b],
                            return (some (`(¬ %%a ∧ ¬ %%b), pr))
      | `(%%a ≤ %%b)  := do e ← to_expr ``(%%b < %%a),
                            pr ← mk_app ``not_le_eq [a, b],
                            return (some (e, pr))
      | `(%%a < %%b)  := do e ← to_expr ``(%%b ≤ %%a),
                            pr ← mk_app ``not_lt_eq [a, b],
                            return (some (e, pr))
      | `(Exists %%p) := do pr ← mk_app ``not_exists_eq [p],
                            e ← match p with
                                | (lam n bi typ bo) := do
                                    body ← mk_app ``not [bo],
                                    return (pi n bi typ body)
                                | _ := tactic.fail "Unexpected failure negating ∃"
                                end,
                            return (some (e, pr))
      | (pi n bi d p) := if p.has_var then do
                            pr ← mk_app ``not_forall_eq [lam n bi d p],
                            body ← mk_app ``not [p],
                            e ←  mk_app ``Exists [lam n bi d body],
                            return (some (e, pr))
                         else do
                            pr ← mk_app ``not_implies_eq [d, p],
                            `(%%_ = %%e') ← infer_type pr,
                            return (some (e', pr))
      | _             := return none
      end)
    | _        := return none
  end

-- given an expr 'e', returns a new expression with transformed negation and a proof of equality
private meta def transform_negation : expr → tactic (option (expr × expr)) :=
λ e, do
  opr ← transform_negation_step e,
  match opr with
  | (some (e', pr)) := do
    opr' ← transform_negation e',
    match opr' with
    | none              := return (some (e', pr))
    | (some (e'', pr')) := do pr'' ← mk_eq_trans pr pr',
                              return (some (e'', pr''))
    end
  | none            := return none
  end

meta def normalize_negations (t : expr) : tactic (expr × expr) :=
do (_, e, pr) ← simplify_top_down ()
                   (λ _, λ e, do
                       oepr ← transform_negation e,
                       match oepr with
                       | (some (e', pr)) := return ((), e', pr)
                       | none            := do pr ← mk_eq_refl e, return ((), e, pr)
                       end)
                   t { eta := ff },
   return (e, pr)

meta def push_neg_at_hyp (h : name) : tactic unit :=
do
  H ← get_local h,
  t ← infer_type H,
  (e, pr) ← normalize_negations t,
  replace_hyp H e pr,
  skip

meta def push_neg_at_goal : tactic unit :=
do
  H ← target,
  (e, pr) ← normalize_negations H,
  replace_target e pr
end push_neg

open interactive (parse)
open interactive (loc.ns loc.wildcard)
open interactive.types (location)
open push_neg

meta def tactic.interactive.push_neg : parse location → tactic unit
| (loc.ns loc_l) := loc_l.mmap' (λ l, match l with
                                      | some h := push_neg_at_hyp h >>  try `[simp only [not_eq] at h { eta := ff }]
                                      | none   := push_neg_at_goal >>  try `[simp only [not_eq] { eta := ff }]
                                      end)
| loc.wildcard := do
    push_neg_at_goal,
    local_context >>= mmap' (λ h, push_neg_at_hyp (local_pp_name h)) ,
    try `[simp only [not_eq] at * { eta := ff }]

example (h : ∃ p: ℕ, ¬ ∀ n : ℕ, n > p) (h' : ∃ p: ℕ, ¬ ∃ n : ℕ, n < p): ¬ ∀ n : ℕ, n = 0 :=
begin
  push_neg at *,
  use 1,
end

-- In the next example, ℤ should be ℝ in maths, but I don't want to import real numbers
-- for testing only
notation `|` x `|` := abs x

example (a : ℕ → ℤ) (l : ℤ) (h : ¬ ∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < ε) : true :=
begin
  push_neg at h,
  trivial
end

example (f : ℤ → ℤ) (x₀ y₀ : ℤ) (h : ¬ (∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε)) : true :=
begin
  push_neg at h,
  trivial,
end