CSE 191: Discrete Structures
Spring 2021 Take-Home Final Exam
Matthew G. Knepley
211A Capen Hall [email protected]
Instructions
You have 27 hours to complete this exam from the start time, 11:45pm Monday
May 10th. Thus all exams must be submitted by 2:45pm Tuesday May 11th.
You are to turn in your exam on Autograder, exactly as you turn in homework.
If you have a problem with submission, mail your Coq .v file directly to the
instructor before the submission deadline. All exams must be submitted in Coq
format.
This is an open book exam. You may use all books, notes, and other edu-
cational materials you find. You may not consult with other students. For all
questions, you must submit a valid constructive proof. You may not use the
following tactics:
1. auto,
2. tauto,
3. lia (except in problem 8),
4. nia,
5. omega.
You are encouraged to use the ring tactic and the tactics suggested specifically
in the problems.
Remember that if you have an algebraic identity that you want to use, for
instance
(n + 1)(n + 2) + 5n + 1 = n2 + 8n + 3,
then you can assert that statement
assert (H : (n + 1) * (n + 2) + 5 * n + 1 = n * n + 8 * n + 3).
prove it using ring, and then transform your equation using
rewrite H.
1
Submission File
Please use this template submission file in order to get the imports and defini-
tions right. It is also posted on the website as FinalExamTemplate2021.v.
Require Import Arith.
Lemma prob1 : forall P Q R S T U : Prop,
(P -> Q) -> (R -> S) -> (T -> U) -> (P /\ R /\ T) -> (Q /\ S /\ U).
Proof.
Qed.
Lemma prob2 : forall P : Prop, ~~~P -> ~P.
Proof.
Qed.
Lemma prob3 : forall A B C : Prop, ((A \/ B) /\ (~A \/ C)) -> (C -> B) -> B.
Proof.
Qed.
Fixpoint sum_n_quartic (n : nat) : nat :=
match n with
O => 0
| S p => n*n*n*n + sum_n_quartic p
end.
Lemma prob4 : forall n : nat,
sum_n_quartic n * 30 + n*(n+1)*(2*n+1) = n*(n+1)*(2*n+1)*(3*n*n + 3*n).
Proof.
Qed.
Open Scope Z_scope.
Require Import ZArith.
Require Import Znumtheory.
Lemma prob5 : forall a b c d : Z, (a | b) -> (c | d) -> (a*c | b*d).
Proof.
Qed.
Lemma prob6 : forall a b c d : Z, (a | b*c) -> Zis_gcd a b d -> (a | c*d).
Proof.
Qed.
Close Scope Z_scope.
Definition relation (X Y : Type) := X -> Y -> Prop.
Definition partial_function {X Y: Type} (R: relation X Y) := forall x : X,
forall y1 y2 : Y, R x y1 -> R x y2 -> y1 = y2.
2
Definition injective {X Y : Type} (R: relation X Y) := forall x1 x2: X, forall y : Y,
(R x1 y) -> (R x2 y) -> x1 = x2.
Definition surjective {X Y : Type} (R: relation X Y) := forall y : Y, exists x : X, R x y.
Definition f := fun x y : nat => 5*x + 2 = y.
Lemma prob7 : ~partial_function ge.
Proof.
Qed.
Lemma f_inj : injective f.
Proof.
Qed.
Require Import Lia.
Lemma f_not_sur : ~surjective f.
Proof.
Qed.
3
1 Implication and Conjunction
Prove that
∀P QRS T U ∈Prop,
(P =⇒ Q) ∧ (R =⇒ S) ∧ (T =⇒ U) ∧ (P ∧R ∧ T ) =⇒ (Q ∧ S ∧ U)
for which the Coq statement is
Lemma prob1 : forall P Q R S T U : Prop,
(P -> Q) -> (R -> S) -> (T -> U) -> (P /\ R /\ T) -> (Q /\ S /\ U).
4
2 Negation
Prove that
∀P ∈ Prop,¬¬¬P =⇒ ¬P
following the instructions for an acceptable proof. The Coq statement is
Lemma prob2 : forall P : Prop, ~~~P -> ~P.
5
3 Disjunction and Negation
Prove that
∀ABC ∈ Prop, ((A ∨B) ∧ (¬A ∨ C)) =⇒ (C =⇒ B) =⇒ B
following the instructions for an acceptable proof. The Coq statement is
Lemma prob3 : forall A B C : Prop, ((A \/ B) /\ (~A \/ C)) -> (C -> B) -> B.
6
4 Induction
Prove that
∀n ∈ N,
n∑
i=0
i4 =
n(n + 1)(2n + 1)(3n2 + 3n− 1)
30
We will use the recursive definition for the sum
Fixpoint sum_n_quartic (n : nat) : nat :=
match n with
O => 0
| S p => n*n*n*n + sum_n_quartic p
end.
and reformulate the statement to eliminate any division or subtraction,
Lemma prob4 : forall n : nat, sum_n_quartic n * 30 + n*(n+1)*(2*n+1) =
n*(n+1)*(2*n+1)*(3*n*n + 3*n).
7
5 Divisibility
Prove that
∀a b c d ∈ Z, (a|b) =⇒ (c|d) =⇒ (ac|bd).
The Coq statement is
Lemma prob5 : forall a b c d : Z, (a | b) -> (c | d) -> (a*c | b*d).
8
6 Divisibility and GCD
Prove that
∀a b c d ∈ Z, (a|bc) =⇒ d = gcd(a, b) =⇒ (a|cd).
following the instructions for an acceptable proof. The Coq statement is
Lemma prob6 : forall a b c d : Z, (a | b*c) -> Zis_gcd a b d -> (a | c*d).
The Zis gcd bezout lemma can be apply’ed to get a Bezout statement, which
can then be destructed, to get the Bezout relation from Zis gcd.
9
7 Relations
Prove that the relation ge is not a partial function, where a partial function
satisfies
∀x : X,∀y1 y2 : Y, (R x y1) =⇒ (R x y2) =⇒ y1 = y2.
In Coq, you would prove
Lemma prob7 : ~partial_function ge.
using the definitions from Chapter 3. You can use unfold ge to expand and
simplify expressions such as a >= b, and use Print ge and Print le to see the
theorems associated with the inductive types.
10
8 Functions
Show that the function f on the natural numbers N given by
f(n) = 5n + 2
in injective, but not surjective. The Coq definition of this function can be
expressed as a relation,
Definition f := fun x y : nat => 5*x + 2 = y.
First, prove that f is injective
Lemma f_inj : injective f.
You will likely find it necessary to use Nat.add cancel r, Nat.mul cancel l,
and discriminate in the proof. Second, prove that f is not surjective
Lemma f_not_sur : ~surjective f.
You will use the lia tactic to prove the last step.
11

欢迎咨询51作业君