Problem Set 1 : Logic and Tactics

For the first part of this assignment, please prove terms manually, as we did at the beginning of class, instead of using tactics.

For each Definition provided, please replace the "." with ":= <exp>." for some expression of the appropriate type.

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:

This is not provable in Coq without adding an axiom, even though in classical logic, we take this for granted:

P \/ ~P

Try to prove it and see what goes wrong... Interestingly, this will almost never bite us.

End PSET1_EX1.

Proving with tactics

Now remove the tauto tactics and redo these problems using only the following tactics:

intros, apply, destruct, unfold, split, contradiction, left, right

(Hopefully we haven't left off any that you may need. In general, don't use things like firstorder or tauto that automatically solves goals. We want you to perform the basic steps to see what is going on.)

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.

This page has been generated by coqdoc