tactic for modus tollens

Stream: general

[Kevin Buzzard]

In NNG I sometimes have the following tactic state:

h1 : a ≠ b
⊢ c ≠ d

and I want to turn it into this:

h2 : c = d
⊢ a = b

(here a,b,c,d are fake naturals, if this matters). The first instance of this has just gone live in "Algorithm world", but I realise now that I'm not happy with my solution. I introduce the tactic have to do this, and I don't really want to introduce that tactic there, I would rather introduce it in a more "core" world like advanced multiplication world rather than in a world which is kind of "optional" like algorithm world (a new world, which I'd be very happy to have feedback on).

One approach is

  apply mt _ h1
  intro h2
  -- clear h1

but I'm wondering if we already have some more high-powered tactic which does this for me. I would far rather teach high-powered tactics which do things which mathematicians find comprehensible like the transformation above ("prove the contrapositive"), than weird tactics like apply which do maths backwards and confuse mathematicians no end. Does anyone have any suggestions?

[Yaël Dillies]

Isn't contrapose exactly what you're looking for?

[Shreyas Srinivas]

contrapose adds negations

[Kevin Buzzard]

Aah -- no -- but contrapose! is! Thanks!

[Eric Wieser]

I'm sure no one cares, but contrapose! uses choice for no reason

[Shreyas Srinivas]

It performs double negatoin elimination doesn't it? Which in turn is probably using LEM which probably uses choice (Diaconescu)

[Kevin Buzzard]

In the context of NNG I definitely don't care :-)

[Chris Wong]

That is true, but since equality on natural numbers is decidable, it should be able to go without it

[Kevin Buzzard]

Yes but that would be a completely irrelevant red herring in this context

[Shreyas Srinivas]

Chris Wong said:

That is true, but since equality on natural numbers is decidable, it should be able to go without it

This is beside the point. (EDIT : contrapose! contrapose) calls push_neg which applies logic lemmas to push negations and eliminate double negations. It doesn't care whether the propositions are decidable or not and how to handle negations in that case. I can't imagine that it would be trivial to extend push_neg to do all that.

[Ruben Van de Velde]

Eric Wieser said:

I'm sure no one cares, but contrapose! uses choice for no reason

I read your comment as "uses choice as opposed to contrapose", but contrapose already uses choice in

lemma mtr {p q : Prop} : (¬ q → ¬ p) → (p → q) := fun h hp ↦ by_contra (fun h' ↦ h h' hp)

[Ruben Van de Velde]

Shreyas Srinivas said:

Chris Wong said:

That is true, but since equality on natural numbers is decidable, it should be able to go without it

This is beside the point. contrapose calls push_neg which applies logic lemmas to push negations and eliminate double negations. It doesn't care whether the propositions are decidable or not and how to handle negations in that case. I can't imagine that it would be trivial to extend push_neg to do all that.

only contrapose! calls push_neg

[Shreyas Srinivas]

Yeah I was talking about contrapose!. See the first few lines of push_neg which adds a bunch of theorems used by push_neg which is used by transformNegationStep :

[Eric Wieser]

My comment is "if people cared, there could be a version of contrapose that sees ¬p → ¬q, and uses mt instead of choice"

[Eric Wieser]

We already have this behavior in by_contra