Zulip Chat Archive

Stream: general

Topic: contraposition


view this post on Zulip Patrick Massot (May 12 2019 at 12:23):

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.

view this post on Zulip Rob Lewis (May 12 2019 at 14:08):

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.

view this post on Zulip Patrick Massot (May 12 2019 at 14:10):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:11):

I'll try that

view this post on Zulip Rob Lewis (May 12 2019 at 14:28):

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]))

view this post on Zulip Patrick Massot (May 12 2019 at 14:28):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:34):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:35):

Oh, I didn't see you wrote some code

view this post on Zulip Patrick Massot (May 12 2019 at 14:36):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:38):

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

view this post on Zulip Rob Lewis (May 12 2019 at 14:40):

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

view this post on Zulip Rob Lewis (May 12 2019 at 14:41):

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.

view this post on Zulip Patrick Massot (May 12 2019 at 14:42):

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

view this post on Zulip Rob Lewis (May 12 2019 at 14:44):

target >>= is_prop?

view this post on Zulip Patrick Massot (May 12 2019 at 14:47):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:48):

no, it's not good enough

view this post on Zulip Patrick Massot (May 12 2019 at 14:48):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:49):

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

view this post on Zulip Patrick Massot (May 12 2019 at 14:51):

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).

view this post on Zulip Rob Lewis (May 12 2019 at 15:01):

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

view this post on Zulip Patrick Massot (May 12 2019 at 17:36):

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

view this post on Zulip Rob Lewis (May 12 2019 at 19:29):

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.

view this post on Zulip Rob Lewis (May 12 2019 at 19:30):

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

view this post on Zulip Patrick Massot (May 12 2019 at 19:32):

I was not catching failure at the right level

view this post on Zulip Patrick Massot (May 12 2019 at 19:34):

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

view this post on Zulip Rob Lewis (May 12 2019 at 19:57):

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]))

view this post on Zulip Rob Lewis (May 12 2019 at 19:58):

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

view this post on Zulip Patrick Massot (May 12 2019 at 20:58):

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

view this post on Zulip Rob Lewis (May 12 2019 at 21:43):

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

Last updated: May 13 2021 at 18:26 UTC