# Problem Set 1 : Logic and Tactics

Module PSET1_EX1.

Definition X1 {A B C D:Prop} :

(B /\ (B -> C /\ D)) -> D.

Definition X2 {A B C:Prop} :

~(A \/ B) -> B -> C.

Definition X3 {A B C:Prop} :

A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).

To solve the following, you'll need to figure out what
the definition of "<->" is and how to work with it...

Definition X4 {A:Prop} :

A <-> A.

Definition X5 {A B:Prop} :

(A <-> B) <-> (B <-> A).

Definition X6 {A B C:Prop} :

(A <-> B) -> (B <-> C) -> (A <-> C).

### Thought exercise:

End PSET1_EX1.

## Proving with tactics

Module PSET1_EX2.

Lemma X1 {A B C D:Prop} :

(B /\ (B -> C /\ D)) -> D.

Proof.

tauto.

Qed.

Lemma X2 {A B C:Prop} :

~(A \/ B) -> B -> C.

Proof.

tauto.

Qed.

Lemma X3 {A B C:Prop} :

A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).

Proof.

tauto.

Qed.

Lemma X4 {A:Prop} :

A <-> A.

Proof.

tauto.

Qed.

Lemma X5 {A B:Prop} :

(A <-> B) <-> (B <-> A).

Proof.

tauto.

Qed.

Lemma X6 {A B C:Prop} :

(A <-> B) -> (B <-> C) -> (A <-> C).

Proof.

tauto.

Qed.

End PSET1_EX2.

Lemma X1 {A B C D:Prop} :

(B /\ (B -> C /\ D)) -> D.

Proof.

tauto.

Qed.

Lemma X2 {A B C:Prop} :

~(A \/ B) -> B -> C.

Proof.

tauto.

Qed.

Lemma X3 {A B C:Prop} :

A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).

Proof.

tauto.

Qed.

Lemma X4 {A:Prop} :

A <-> A.

Proof.

tauto.

Qed.

Lemma X5 {A B:Prop} :

(A <-> B) <-> (B <-> A).

Proof.

tauto.

Qed.

Lemma X6 {A B C:Prop} :

(A <-> B) -> (B <-> C) -> (A <-> C).

Proof.

tauto.

Qed.

End PSET1_EX2.

This page has been generated by coqdoc