Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A tactic pushing negations inwards while keeping names
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, ∀ nN, | 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment