否定が論理式に含まれているとき使えるタクティクを勉強しました。
introタクティク：ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ Bを両方含むようにできれば最後にapply hb hbnで矛盾を導いて証明が終わります。
by_contraタクティク：ゴールが特に否定の形ではない場合でも、by_contra hとすることでゴールの否定を仮定hとして導入するとともに、ゴールをFlase(矛盾)にすることができます。仮定の中で矛盾を導くことで証明を終了させることができます。
不等式の変形：ゴールが不等式の否定である場合には以下の４つの定理を使って否定を外したり導入したりすることができます。
#check (not_le_of_gt : a > b → ¬a ≤ b)
#check (not_lt_of_ge : a ≥ b → ¬a < b)
#check (lt_of_not_ge : ¬a ≥ b → a < b)
#check (le_of_not_gt : ¬a > b → a ≤ b)
push_negタクティク：ゴールが複数の量化子のついた命題の否定である時push_negで量化子を調整した命題に変換してくれます。push_neg at hとすると仮説hも変換することができます。連続性に関連する命題などで便利そうです。これは１つ例を示してみましょう(MIL記載の例です）。
example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
by_contra h1 -- h1: ¬∃ x y, x ≤ y ∧ f y < f x
-- ⊢ False
push_neg at h1 -- h1: ∀ (x y : ℝ), x ≤ y → f x ≤ f y-- ⊢ False
apply h h1 -- No goals
push_neg at h1のところでh1が書き変わっていることがわかります。その結果の主張はまさにMonotone fです。したがってapply h h1で矛盾が導けます。
exfalso, contradictionタクティク：exfalsoはゴールを強制的にFalseに変えるタクティクです。仮定から矛盾(False)を導けそうな状況で、ゴールPが（多少変なのも含めて）てきとうな論理式である場合に使えます。任意の命題PについてFalse→Pなのでゴールの命題Pは実はどうでもよくて仮定の中に矛盾が見つかれば証明終了です。さらに一歩進んでcontradictionというタクティクを使うと仮定の中に明らかな矛盾が見つかればゴールをクローズして証明終了となります。
