contraposition

Stream: general

[Patrick Massot]

Still looking at my first year undergraduate course tactics, I see:

lemma contrapose (P Q : Prop) [decidable Q] : (¬ Q → ¬ P) → (P → Q) :=
λ h hP, by_contradiction (λ h', h h' hP)
open tactic interactive (parse loc) lean.parser (tk) interactive.loc

meta def tactic.interactive.contrapose (push : parse $ optional (tk "!" )) : tactic unit:=
do
  tgt ← target,
  match tgt with
  | `(%%P → %%Q) := `[apply contrapose %%P %%Q]
  | _ := skip
  end,
  if push.is_some then try (tactic.interactive.push_neg (ns [none])) else skip

Of course we can already use rw not_imp_not or rw ← not_imp_not but you need to remember this name and the direction, and you don't have integration with push_neg. From a pedagogical point of view, I like to say in lectures: "reasoning by contrapositive" is an important technique, here is the Lean command to do that. In the same way we have by_contradiction and exfalso that are thin wrappers around the corresponding lemmas.

How people would feel if I PRed it into mathlib? I ask before writing the PR because the process involves efforts to put things at the right location, and write tests.

[Rob Lewis]

This sounds reasonable. A useful variant might be contrapose h. When the goal is Q with h : P is in the local context, this reverts h, does your thing, and then intros h : ¬ Q.

[Patrick Massot]

I guess adding this wouldn't cost much, and can be ignored by users who don't want it

[Patrick Massot]

I'll try that

[Rob Lewis]

By the way, are you sure the failure behavior is what you want? When the goal isn't an implies, your tactic either does nothing or reduces to push_neg. My instinct is that it should fail.

meta def tactic.interactive.contrapose (push : parse $ optional (tk "!" )) : tactic unit:=
do `(%%P → %%Q) ← target,
   mk_app `contrapose [P, Q] >>= apply,
   when push.is_some $ try (tactic.interactive.push_neg (ns [none]))

[Patrick Massot]

You are right, it should fail. I'll modify this

[Patrick Massot]

Do we have a version of when where we get access to the assumption? (like when we do if h : ... then ... else ...)

[Patrick Massot]

Oh, I didn't see you wrote some code

[Patrick Massot]

I prefer the version I have now because it has a helpful error message

[Patrick Massot]

Is there any advantage of mk_app instead of my `[...] (besides the fact that it looks more profesionnal)?

[Rob Lewis]

Heh, I just noticed that when takes a decidable Prop. Figured it took a bool, but that's actually whenb.

[Rob Lewis]

Is there any advantage of mk_app instead of my `[...] (besides the fact that it looks more profesionnal)?

That, and it avoids entering interactive parsing mode. Not a big difference.

[Patrick Massot]

Hum, I also need to learn how to assert stuff is Prop. The pattern `(%%P → %%Q) is not specific enough

[Rob Lewis]

target >>= is_prop?

[Patrick Massot]

I wanted to test P and Q, but maybe testing target would be good enough

[Patrick Massot]

no, it's not good enough

[Patrick Massot]

It will be fooled by goals that look like forall x, P x

[Patrick Massot]

(and yes, students will try contrapose on such goals)

[Patrick Massot]

My wife asserts the goal's type is to mow the lawn. I'll read your explanations when I'll come back (there is also a tactic writing question in the choose thread, in case I'm too slow in the garden and you get bored).

[Rob Lewis]

Ah, yeah. Easiest to just check both with is_prop then.

[Patrick Massot]

Lean complains tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic when I try to use is_prop on P or Q

[Rob Lewis]

That should only happen on Q when there's a dependency. Your tactic can fail if Q.has_var is true. Otherwise, is_prop should succeed on both P and Q, and if it's true in both cases you have a nondependent implication.

[Rob Lewis]

Alternatively, you could try to unify the goal with an application of implies, but I think doing those checks is more straightforward.

[Patrick Massot]

I was not catching failure at the right level

[Patrick Massot]

My current version is

meta def tactic.interactive.contrapose (push : parse (tk "!" )?) (hyp : parse ident?): tactic unit:=
do
  when hyp.is_some (do
    h ← get_local (hyp.get_or_else `this),
    revert h,
    skip),
  tgt ← target,
  let err := "The goal is not an implication, and you didn't specify an assumption",
  match tgt with
  | `(%%P → %%Q) := do (is_prop P >> is_prop Q) <|> fail err,
                       mk_app `contrapose [P, Q] >>= apply
  | _ := fail err
  end,
  when push.is_some $ try (tactic.interactive.push_neg (ns [none])),
  when hyp.is_some $ (intro $ hyp.get_or_else `this) >> skip

I don't like the get_or_else where I already now the option is some. But I don't know better

[Rob Lewis]

There's an error using mk_app, it needs mk_mapp. I think this is a bit cleaner:

meta def tactic.interactive.contrapose (push : parse (tk "!" )?) : parse ident? → tactic unit
| (some h) := get_local h >>= revert >> tactic.interactive.contrapose none >> intro h >> skip
| none :=
  do tgt ← target,
  let err := "The goal is not an implication, and you didn't specify an assumption",
  match tgt with
  | `(%%P → %%Q) := do (is_prop P >> is_prop Q) <|> fail err,
                       mk_mapp `contrapose [P, Q] >>= apply
  | _ := fail err
  end,
  when push.is_some $ try (tactic.interactive.push_neg (loc.ns [none]))

[Rob Lewis]

The behavior of contrapose h will be funny if anything depends on h, but I think that's the user's problem.

[Patrick Massot]

https://github.com/leanprover-community/mathlib/pull/1015 Thanks a lot for all your help Rob!

[Rob Lewis]

No problem! I didn't notice before, but is_prop won't fail, it will just return true or false. So what you have now will give the error from mk_mapp if it gets a non-prop or dependent pi. If you only want to give the one error message, you should do something like this instead.

meta def tactic.interactive.contrapose (push : parse (tk "!" )?) : parse ident? → tactic unit
| (some h) := get_local h >>= revert >> tactic.interactive.contrapose none >> intro h >> skip
| none := let err := "The goal is not an implication, and you didn't specify an assumption" in
  (do `(%%P → %%Q) ← target,
  mk_mapp `contrapose [P, Q] >>= apply,
  when push.is_some $ try (tactic.interactive.push_neg (loc.ns [none]))) <|> fail err