Post

Rules of Inference with Coq

Posted
By Sungchan Yi 6 min read

This is a list of proofs with Coq, for each rule of inference stated in List of Rules of Inference (Wikipedia)

Some rules that need the law of excluded middle are at the end of the section.

Rules for Negation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Lemma reductio_ad_absurdum : forall P Q : Prop,
  (P -> Q) -> (P -> ~Q) -> ~P.
Proof.
  intros. intros HP.
  apply H0 in HP as HNQ.
  apply H in HP as HQ.
  contradiction.
Qed.

Lemma ex_contradictione_quodlibet : forall P Q : Prop,
  P -> ~P -> Q.
Proof. intros. contradiction. Qed.

Lemma double_negation_introduction : forall P : Prop,
  P -> ~~P.
Proof. auto. Qed.

Rules for Conditionals

1
2
3
4
5
6
7

Lemma modus_ponens : forall P Q : Prop,
  (P -> Q) -> P -> Q.
Proof. auto. Qed.

Lemma modus_tollens : forall P Q : Prop,
  (P -> Q) -> ~Q -> ~P.
Proof. auto. Qed.

Rules for Conjunctions

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

Lemma conjuction_introduction : forall P Q : Prop,
  P -> Q -> P /\ Q.
Proof. auto. Qed.

Lemma conjunction_elimination_left : forall P Q : Prop,
  P /\ Q -> P.
Proof. intros P Q [HP HQ]; auto. Qed.

Lemma conjunction_elimination_right : forall P Q : Prop,
  P /\ Q -> Q.
Proof. intros P Q [HP HQ]; auto. Qed.

Lemma conjunction_commutative : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros. destruct H; split; auto.
Qed.

Lemma conjunction_associative : forall P Q R : Prop,
  (P /\ Q) /\ R -> P /\ (Q /\ R).
Proof.
  intros. destruct H as [H H1]; destruct H; split; auto.
Qed.

Rules for Disjunctions

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

Lemma disjunction_introduction_left : forall P Q : Prop,
  P -> P \/ Q.
Proof. auto. Qed.

Lemma disjunction_introduction_right : forall P Q : Prop,
  Q -> P \/ Q.
Proof. auto. Qed.

Lemma disjunction_elimination : forall P Q R : Prop,
  (P -> R) -> (Q -> R) -> (P \/ Q) -> R.
Proof.
  intros. destruct H1; auto.
Qed.

Lemma disjunctive_syllogism_left : forall P Q : Prop,
  (P \/ Q) -> ~P -> Q.
Proof.
  intros. destruct H; auto. contradiction.
Qed.

Lemma disjunctive_syllogism_right : forall P Q : Prop,
  (P \/ Q) -> ~Q -> P.
Proof.
  intros. destruct H; auto. contradiction.
Qed.

Lemma constructive_dilemma : forall P Q R S : Prop,
  (P -> R) -> (Q -> S) -> (P \/ Q) -> (R \/ S).
Proof.
  intros. destruct H1; auto.
Qed.

Lemma disjunction_commutative : forall P Q : Prop,
  P \/ Q -> Q \/ P.
Proof. intros. destruct H; auto. Qed.

Lemma disunction_associative : forall P Q R : Prop,
  (P \/ Q) \/ R -> P \/ (Q \/ R).
Proof.
  intros. destruct H as [H | H]; auto.
  destruct H; auto.
Qed.

Rules for Biconditionals

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

Lemma biconditional_introduction : forall P Q : Prop,
  (P -> Q) -> (Q -> P) -> (P <-> Q).
Proof. split; auto. Qed.

Lemma biconditional_elimination_left_mp : forall P Q : Prop,
  (P <-> Q) -> P -> Q.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_right_mp : forall P Q : Prop,
  (P <-> Q) -> Q -> P.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_left_mt : forall P Q : Prop,
  (P <-> Q) -> ~P -> ~Q.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_right_mt : forall P Q : Prop,
  (P <-> Q) -> ~Q -> ~P.
Proof.
  intros. destruct H; auto.
Qed.

Lemma biconditional_elimination_disjunction : forall P Q : Prop,
  (P <-> Q) -> (P \/ Q) -> (P /\ Q).
Proof.
  intros. destruct H, H0; auto.
Qed.

Lemma biconditional_elimination_disjunction_not : forall P Q : Prop,
  (P <-> Q) -> (~P \/ ~Q) -> (~P /\ ~Q).
Proof.
  intros. destruct H, H0; auto.
Qed.

Other Rules

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

Lemma exportation : forall P Q R : Prop,
  (P /\ Q) -> R <-> (P -> Q -> R).
Proof.
  split; auto.
  destruct H; auto.
Qed.

Lemma distributive_disjunction : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  split; intros.
  - destruct H as [H | [H1 H2]]; split; auto.
  - destruct H as [H1 H2]; destruct H1, H2; auto.
Qed.

Lemma distributive_conjunction : forall P Q R : Prop,
  P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
Proof.
  split; intros.
  - destruct H as [H [H1 | H1]]; auto.
  - destruct H as [ [H1 H2](H1%20H2.md); auto.
Qed.

Lemma material_implication_converse : forall P Q : Prop,
  (~P \/ Q) -> (P -> Q).
Proof.
  intros. destruct H; auto. contradiction.
Qed.

Lemma resolution : forall P Q R : Prop,
  (P \/ Q) -> (~P \/ R) -> (Q \/ R).
Proof.
  intros. destruct H, H0; auto. contradiction.
Qed.

Rules that require Excluded Middle

We declare the law of excluded middle as an axiom.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

Axiom excluded_middle : forall P : Prop, P \/ ~P.

Lemma double_negation_elimination : forall P : Prop,
  ~~P -> P.
Proof.
  intros. destruct (excluded_middle P); auto. contradiction.
Qed.

Lemma material_implication : forall P Q : Prop,
  (P -> Q) -> (~P \/ Q).
Proof.
  intros. destruct (excluded_middle P); auto.
Qed.

Lemma reductio_ad_absurdum_neg : forall P Q : Prop,
  (~P -> Q) -> (~P -> ~Q) -> P.
Proof.
  intros. destruct (excluded_middle P); auto.
  apply H in H1 as HQ.
  apply H0 in H1 as HNQ.
  contradiction.
Qed.

I was supposed to be reading the source for the paper Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency but I got carried away…

Mathematics, Coq
math coq proof-verification
This post is licensed under CC BY 4.0 by the author.