Skip to content

Instantly share code, notes, and snippets.

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

Embed
What would you like to do?
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.