software foundations

first.v

Check 3 = 3.
Check forall n m : nat, n + m = m + n.

Definition is_three (n : nat) : Prop :=
  n = 3.

Definition injective {A B} (f : A -> B) :=
  forall x y : A,  f x = f y -> x = y.

Lemma succ_inj : injective S.
Proof.
  intros n m H.
  inversion H.
  reflexivity.
Qed.

Example and_example : 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
  split.
  simpl. reflexivity.
  simpl. reflexivity.
Qed.

Lemma and_intro : forall A B : Prop, A -> B -> A /\ B.
Proof.
  intros A B HA HB.
  split.
  apply HA.
  apply HB.
Qed.

Lemma and_example2 :
  forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.

Proof.
  intros n m [H1 H2].
  rewrite H1.
  rewrite H2.
  reflexivity.
Qed.

Lemma proj1 : forall P Q : Prop, P /\ Q -> P.
Proof.
  intros p q [h1 h2].
  assumption.
Qed.

Theorem and_commut : forall P Q : Prop, P /\ Q -> Q /\ P.
Proof.
  intros P Q [H1 H2].
  split.
  assumption.
  assumption.
Qed.

Theorem and_assoc : forall P Q R : Prop, P /\ (Q /\ R) -> (P /\ Q) /\ R.
Proof.
  intros P Q R [H1 H2].
  destruct H2.
  split.
  split.
  assumption. assumption. assumption. Qed.

Lemma or_example:
  forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof.
  intros n m [H1 | H2].
  rewrite H1.
  reflexivity.
  rewrite H2.
  auto.
Qed.

Lemma or_intro: forall A B : Prop, A -> B \/ A.
Proof.
  intros A B H.
  right.
  apply H.
Qed.

Theorem ex_false_quodlibet : forall (P : Prop),
     False -> P.
Proof.
  intros P H.
  destruct H.
Qed.

Theorem zero_not_one : not (0 = 1).
Proof.
  intros F. inversion F.
Qed.

Theorem contr_impl : forall P Q : Prop, (P /\ ~P) -> Q.
Proof.
  intros P Q [H1 H2].
  unfold not in H2.
  apply H2 in H1.
  destruct H1.
Qed.