Library proposition_logic

Introduction to Coq

To prove a result, we announce it as a Theorem or Lemma, with a name, as follows.

Lemma Tautology:
forall A B C:Prop, (A -> B -> C ) -> (A -> B ) -> (A -> C ).

Then we give the proof using tactics; we are now in "proof mode" We start with Proof, which is not mandatory but clarifies the structure

Proof.
intros.

moves as many hypotheses as possible to the context

apply H.

applies hypothesis H to prove C

assumption.

searches for a variable of type A in the context

apply H0.
assumption.

The proof is now complete. It is saved for future use with the command Qed. We can refer to this proof by the name we have given: Tautology This ends the proof mode.

Qed.

Here is the same proof with bulleting to improve the structure and make subgoals explicit

Lemma Tautology':
forall A B C:Prop, (A -> B -> C ) -> (A -> B ) -> (A -> C ).
Proof.
intros.
apply H.
- assumption.
- apply H0. assumption.

See the files by Jules Jacobs on the webpage for further explanation on the bulleting and indentation

Qed.

Implication_Logic

Section Implication_Logic.
Variable A B C : Prop.

It is nicer to not quantify over A B C : Prop all the time but to keep these global within a Section

TODO: use just intros apply assumption to prove the following. So you have to replace each Admitted by a proof script ending in Qed.

Lemma ex_1b : (A -> B ) -> (B -> C ) -> (A -> C ).
Admitted.

Lemma ex_1c : (A -> A -> B ) -> (A -> B ).
Admitted.

Lemma ex_1d : (A -> B ) -> (A -> A -> B ).
Admitted.

End Implication_Logic.

Conjunction and disjunction

Section And_Or.

Variable A B C : Prop.

Lemma prop_001 : (A /\ B ) -> (B /\ A ).
Proof.
intro H.
destruct H as [H1 H2].

Also try
destruct H.
or
elim H. intros H1 H2.
or
case H.
The primitive tactic is elim.
destruct basically does an intros immediately after the elim.
destruct H as [H1 H2] does the intros with the given names; here [H1 H2] describes the "intro pattern" for /\: we get two pieces of data, H1:A and H2:B

split.
- assumption.

or: exact H2. in case you want to name the assumption

- assumption.
Qed.

Lemma prop_001a : (A \/ B ) -> (B \/ A ).
Proof.
intro H.
destruct H as [H1 | H2].

Also try
destruct H.
or
elim H. intros H1.
or
case H.
Here [H1 | H2] describes the "intro pattern" for \/: we get a case split, as we get two cases, one with H1:A and one with H2:B.

- right. assumption.
- left; assumption.

The ; is for "chaining" tactics. The second tactic is applied to all goals generated by the first tactic

Qed.

Lemma prop_001b : (A \/ B )/\C -> (A \/ B )/\(A \/C ).
Admitted.

use just intros apply assumption destruct split left right

Lemma prop_001bb : (A \/ B ) /\ C -> (A /\ C ) \/ (B /\ C ).
Admitted.

Lemma prop_001c : (A \/ B -> C ) -> (A -> C )/\(B -> C ).
Admitted.

Lemma prop_035 : (A -> (B -> C )) /\ (A -> B ) -> (A -> C ).
Admitted.

End And_Or.

Negation

Section Negation.

Variable A B C : Prop.

The negation of A, not A, with notation ~A, is defined as A -> False, where from False we can derive anything.
Type unfold not to unfold the definition of ~A into A -> False and then you can apply your usual tactics

Lemma ex_2a : (A -> B ) -> ~B -> ~A.
Admitted.

Theorem prop_026 : (~A /\ ~B ) -> ~(A \/ (~A /\ B )).

NB Theorem does the same as Lemma, it is just for you if you want to distinguish between main results and auxiliary results

Proof.
intros.
intro H1.

Here we exploit that ~(A \/ (~A /\ B)) is just (A \/ (~A /\ B)) -> False
Coq does not automatically unfold this definition, but when we say intro H1 it does.
Try: unfold not to unfold the definition of ~

destruct H1 as [H2|H3].

Note that A \/ ~ A /\ B means A \/ (~ A /\ B)

- destruct H as [H4 H5].
apply H4.

remember that ~A is just A -> False

  assumption.
- destruct H as [H4 H5].
  destruct H3 as [H6 H7].
  contradiction.

This simplifies things a bit; Coq tries to derive False in the present context and if it succeeds, the proof is finished, as everything is provable from False

Qed.

Lemma ex_2c : ~~~A -> ~A.
Admitted.

Lemma ex_2d : (A -> ~A ) -> ~A.
Admitted.

Lemma prop_065 : (A /\ B ) \/ ~B -> B -> (A /\ B ).
Admitted.

Lemma prop_014 : (~(A /\ A ) -> (~A \/ ~A )).
Admitted.

Lemma ex_2e : (A -> B ) -> (A -> ~B ) -> A -> C.
Proof.
intros H1 H2 H3.
absurd B.

This says that B and ~B are derivable, and so we have False, from which anything follows

- apply H2.
assumption.
- exact (H1 H3).

Note that you can also destruct/apply/elim larger terms, like H1 H3 here, you don't just have to refer to variables

Also try typing intuition immediately after intros H1 H2 H3
intuition does some simple proposition logic steps automatically

Qed.

End Negation.

Classical Logic

Section Classical.

Require Import Classical.

It provides "excluded middle" as an axiom

Check classic.

One way of using it in the proofs is by means of the elimination rule for disjunction: destruct (classic A)

Variable A B C : Prop.

Theorem dn_law : ~~A -> A.
Proof.
destruct (classic A).
- intros. assumption.
- intros. contradiction.
Qed.

Again, we "chain tactics". The ; is sequential composition, t1 ; t2 means that t2 is applied to all goals generated by t1

Lemma prop_002 : (~A -> A ) -> A.
Admitted.

Lemma prop_003 : (~A -> A ) \/ ~A.
Admitted.

Lemma prop_025 : A -> (~B \/ (A /\ B )).
Admitted.

Lemma prop_021 : ~A \/ (B -> A ).
Admitted.

This one can also be done without classical logic

Lemma prop_065b : (A /\ B ) \/ ~B -> B -> (A /\ B ).
Admitted.

The following one can be done without classical logic

Lemma prop_104 : (A \/ B ) -> ~(~A /\ ~B ).
Admitted.

This one is found tricky and can only be doen using classical logic

Lemma prop_037 : ((A /\ B ) -> C ) -> ((A -> C ) \/ (B -> C )).
Admitted.

End Classical.

Assorted examples

Section Assorted.
Variable A B C D: Prop.

We do a bit of chaining and tactic combination in the next proof Try for yourself

Lemma prop_085 : ~((A -> (B \/ ~C )) /\ (B -> ~A ) /\ (A -> C ) /\ A ).
Proof.
intro H.
destruct H as [H [H1 H2]].

Does the same as destruct H. destruct H1. destruct H2.

destruct H.
- destruct H2; assumption.
- apply H1.
  + assumption.
  + destruct H2. assumption.
- apply H.
  destruct H2.
  apply (H0 H2).
Qed.

The following is tricky, but can be done without classical logic; for now you may use classical logic by typing
Require Import Classical.

Lemma prop_063 : ~~((~A -> B ) /\ (~A -> ~B ) -> A ).
Admitted.

You don't need Classical here

Lemma prop_082 : (A -> B ) /\ (C -> D ) -> (~B \/ ~D ) -> (~A \/ ~C ).
Admitted.

A variant of De Morgan; you need classical logic here: Require Import Classical.

Lemma prop_106 : ~(~A /\ ~B ) -> (A \/ B ).
Admitted.

End Assorted.