Disjunctive Syllogism tactic in Coq?

Question

I am learning propositional logic and the rules of inference. The Disjunctive Syllogism rule states that if we have in our premises (P or Q), and also (not P); then we can reach Q.

I can not for the life of me figure out how to do this in Coq. Let's say I have :

H : A \/ B
H0 : ~ A
______________________________________(1/1)

What tactic should I use to reach

H1 : B.

As an extra, I would be glad if someone could share with me the Coq tactic equivalents of basic inference rules, like modus tollens, or disjunctive introduction etc. Is there maybe a plugin I can use?

Answer 1

Coq does not have this tactic built-in, but fortunately you can define your own tactics. Notice that

destruct H as [H1 | H1]; [contradiction |].

puts H1 : B in the context, just as you asked. So you can create an alias for this combined tactic:

Ltac disj_syllogism AorB notA B :=
  destruct AorB as [? | B]; [contradiction |].

Now we can easily imitate the disjunctive syllogism rule like so:

Section Foo.
Context (A B : Prop) (H : A \/ B) (H0 : ~ A).
Goal True.
  disj_syllogism H H0 H1.
End Foo.

Let me show a couple less automated approaches:

Ltac disj_syllogism AorB notA B :=
  let A := fresh "A" in
  destruct AorB as [A | B]; [contradiction (notA A) |].

This approach does not ask Coq to find a contradiction, it provides it directly to the contradiction tactic (notA A term). Or we could have used an explicit term with the pose proof tactic:

Ltac disj_syllogism AorB notA B :=
  pose proof (match AorB with
              | or_introl a => False_ind _ (notA a)
              | or_intror b => b
              end) as B.

I hope this helps. I'm not sure if some extra explanation is needed -- feel free to ask for clarification and I'll update my answer.