Instantly share code, notes, and snippets.

# dcci/first.v Last active Mar 5, 2018

software foundations
 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.