CODEWITHSUNDEEP
coqcoq-tactic
mlg556
mlg556

Reputation: 419

Disjunctive Syllogism tactic in Coq?

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?

Upvotes: 4

Views: 330

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15414

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.

Upvotes: 3

Volker Stolz
Volker Stolz

Reputation: 7402

I think you maybe have the wrong expectations on how Coq works? The general way of proving this is essentially a truth-table on the different possibilities:

Lemma it: forall a b, (a \/ b) /\ ~a -> b.
Proof.
  intuition.
  Show Proof.
Qed.

(fun (a b : Prop) (H : (a \/ b) /\ ~ a) =>
 and_ind
   (fun (H0 : a \/ b) (H1 : ~ a) =>
    or_ind (fun H2 : a => let H3 : False := H1 H2 in False_ind b H3)
      (fun H2 : b => H2) H0) H)

If you look at the resulting proof-term, you see the Coq is essentially taking apart the boolean the constructors. We can do this manually and get the same proof-term:

Lemma it: forall a b, (a \/ b) /\ ~a -> b.
Proof.
  intros a b H.
  induction H.
  induction H.
  contradict H. exact H0.
  exact H.
Qed.

Whereas e.g. modus ponens corresponds to an apply in Coq, I don't think this is "built in" in any direct way.

Afterwards, you can use this lemma (and I'm sure there's a corresponding version somewhere in the standard library) to derive your additional hypothesis through apply.

Upvotes: 0

Related Questions