apply the contrapositive of a hypothesis

Stream: Is there code for X?

[Jared green]

how do i apply the contrapositive of a hypothesis in a proof of this structure?

theorem ex (a b : Nat -> Prop) : (a 0->b 0 ) -> ∀ n : Nat, (¬(a n) -> ¬(a (n + 1) )) ∧ (¬(b (n + 1)) -> ¬b n ) -> ∀ n : Nat, (a n -> b n) :=
  by
  intro hab hn n
  induction' n with n hna
  exact hab
  intro ha
  by_contra nhb
  apply (hn n).2 at nhb
  --what do i do here?
  apply (hn n).1 at nhb
  apply nhb
  exact ha

[Edward van de Meent]

you mean modus tollens? (also, it seems your code doesn't compile as-is, please make a #mwe )
docs#mt

[Jared green]

try it now

[Edward van de Meent]

i'd like to point out that the statement you're trying to prove isn't true; choose a := fun _ => True, and b := fun _ => False, and any n.

[Jared green]

try again.

[Edward van de Meent]

it has the same issue

[Edward van de Meent]

import Mathlib

theorem counterexample : ¬ ∀ (a b : Nat -> Prop), (∀ n : Nat, (¬(a n) -> ¬(a (n + 1) )) ∧ (¬(b (n + 1)) -> ¬b n ) -> ∀ n : Nat, (a n -> b n)) :=
  by
  push_neg
  use fun _ => True
  use fun _ => False
  simp only [not_true_eq_false, imp_self, not_false_eq_true, and_self, exists_const]

[Jared green]

try again

[Edward van de Meent]

here is a working version of what you wanted; note the addition of some more brackets in the statement to make it work; i took the liberty of not using by_contra, but rather using .mtr to get the contrapositive of the relevant implications where the negations are removed. Alternatively, i could have used have and .mt, and followed up with push_neg at hypothesis_name.

theorem ex (a b : Nat -> Prop) (h0 : a 0->b 0 ) (hna_step : ∀ n, ¬a n → ¬a (n+1))
    (hnb_step : ∀ n, ¬b (n + 1) → ¬b n) : ∀ n : Nat, (a n -> b n) := by
  intro n
  induction' n with n hinduct
  · exact h0
  · intro ha
    apply (hnb_step n).mtr
    apply hinduct
    apply (hna_step n).mtr
    exact ha

[Amir Livne Bar-on]

Reviving this old thread since I have a related question.

One of the things that the idiom

by_contra hc
apply h at hc
revert hc

can accomplish that

apply mt h

cannot is handle quantification: that is, cases where the property is stated as a quantified theorem.

Examples for this can't be too short, but I ran into this issue several times.

Here I'll try to demonstrate with a simple example. I know it's solvable by proving that 4 * m + 3 is odd first, but in my proofs it's sometimes more convenient to push it to the end.

def powerOf2 (n : ℕ) : Prop := ∃ k, k ≥ 1 ∧ n = 2 ^ k
theorem powerOf2_even (n : ℕ) : powerOf2 n → n % 2 = 0 := by sorry
example (m : ℕ) : ¬powerOf2 (4 * m + 3) := by
  by_contra hc
  apply powerOf2_even at hc
  revert hc
  -- prove that 4 * m + 3 is odd

The by_contra block cannot be replaced with apply mt. However, it could be replaced by apply mt_u where

lemma  mt_u {α : Type*} {p q : α → Prop} {x : α} (h : ∀ x, p x → q x) (hq : ¬q x) : ¬p x := fun hp => hq (h x hp)

Is there something like this in the standard library? A sequence of lemmas, or a tactic for this?

[Floris van Doorn]

refine mt (powerOf2_even _) ?_

[Amir Livne Bar-on]

Thanks! this is just that :))

[Amir Livne Bar-on]

I read the docs for the refine tactic before, and they say it's line "exact with holes", which is how I thought of apply too. From some testing all uses of exact in my proofs can be replaced with either refine or apply, but they can't stand in for each other.

What's the difference between them exactly? And where can I read about the ?_ syntax?

[Kevin Buzzard]

apply is "exact but Lean will figure out where the holes are and write ?_ for you"

[Kevin Buzzard]

I should think that any time exact works, both refine and apply will work.

[Ruben Van de Velde]

(*) some exceptions exist, but in general this is true

[Amir Livne Bar-on]

So apply is a limited type of refine where you're allowed to elide ?_s at the end? (except for typeclass resolution rules etc.)

[Ruben Van de Velde]

Pretty much