Library proposition_logic_answers

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.
Proof.
intros H H0.
intro H1.

or unfold not. intro H1

apply H0.
apply H.
assumption.
Qed.

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.
Proof.
intros.
unfold not.
intros.
apply H.

~~~A is just (~~A) -> False

intro H1.

forces Coq to consider ~~A as (~A) -> False; just intros does not do this

contradiction.

or apply H1 etc

Qed.

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

Lemma prop_065 : (A /\ B ) \/ ~B -> B -> (A /\ B ).
Proof.
intros.
destruct H as [H1|H2].
- exact H1.
- contradiction.
Qed.

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 ).
Proof.
intros H H1.
split.
- destruct H as [Hl | Hr].
* destruct Hl; assumption.
* contradiction.
- assumption.
Qed.

The following one can be done without classical logic

Lemma prop_104 : (A \/ B ) -> ~(~A /\ ~B ).
Proof.
intros H H1.
destruct H as [Ha | Hb].
- destruct H1 as [Hna Hnb].
contradiction.
- destruct H1 as [Hna Hnb].
contradiction.

or just
intros H H1.
destruct H as [Ha | Hb]; destruct H1 as [Hna Hnb]; contradiction.

Qed.

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

Lemma prop_037 : ((A /\ B ) -> C ) -> ((A -> C ) \/ (B -> C )).
Proof.
intro H.
destruct (classic B); destruct (classic A).
- left.

or right. also works

  intros Ha. apply H. split; assumption.
- left.
  intro Ha. contradiction.
- right.
  intro Hb. contradiction.
- left.

or right. also works

intro Ha. contradiction.
Qed.

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 ).
Proof.

We do the proof without classical

intro H.

Note that the only we we can prove False is by applying H. This looks weird because then we have to prove the "stronger" result, the one without the ~~. The point is that one can prove it from its negation, which is now in the context as H

apply H.
intro H0.
destruct H0.

Here is a proof using the assert tactic, but I try to avoid assert, as Coq is a goal directed prover
assert (~A). - intros H4. apply H. intros. assumption. - assert False. + apply H1. * assumption. * apply H0. assumption. + contradiction.

destruct H1.

!! This says: we will derive the goal from the False at the end of ~A -> ~ B. This leaves us with the goals to prove ~A and B

- intro H2. apply H.
intros;assumption.
- apply H0.
intro H2; apply H; intros; assumption.
Qed.

You don't need Classical here

Lemma prop_082 : (A -> B ) /\ (C -> D ) -> (~B \/ ~D ) -> (~A \/ ~C ).
Proof.
intros H H0.
destruct H as [Hl Hr]. destruct H0 as [H1 | H2].
- left. intro Ha; apply H1. apply Hl; assumption.
- right. intro Hc; apply H2. apply Hr; assumption.
Qed.

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

Require Import Classical.
Lemma prop_106 : ~(~A /\ ~B ) -> (A \/ B ).
Proof.
destruct (classic A).
- left; assumption.
- intros.
  destruct (classic B).
  * right; assumption.
  * destruct H0.
    split; assumption.
Qed.

End Assorted.