diff --git a/Basics.v b/Basics.v index ea66eaf..d9b4af3 100644 --- a/Basics.v +++ b/Basics.v @@ -282,17 +282,20 @@ Proof. simpl. reflexivity. Qed. model of the [orb] tests above.) The function should return [true] if either or both of its inputs are [false]. *) -Definition nandb (b1:bool) (b2:bool) : bool - (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. +Definition nandb (b1:bool) (b2:bool) : bool := + match b1, b2 with + | true, true => false + | _, _ => true + end. Example test_nandb1: (nandb true false) = true. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_nandb2: (nandb false false) = true. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_nandb3: (nandb false true) = true. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_nandb4: (nandb true true) = false. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. (** [] *) (** **** Exercise: 1 star, standard (andb3) @@ -301,17 +304,20 @@ Example test_nandb4: (nandb true true) = false. return [true] when all of its inputs are [true], and [false] otherwise. *) -Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool - (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. +Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool := + match b1, b2, b3 with + | true, true, true => true + | _, _, _ => false + end. Example test_andb31: (andb3 true true true) = true. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_andb32: (andb3 false true true) = false. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_andb33: (andb3 true false true) = false. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_andb34: (andb3 true true false) = false. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. (** [] *) (* ================================================================= *) @@ -698,13 +704,16 @@ Fixpoint exp (base power : nat) : nat := Translate this into Coq. *) -Fixpoint factorial (n:nat) : nat - (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. +Fixpoint factorial (n:nat) : nat := + match n with + | 0 => 1 + | S n => (S n) * factorial (n) + end. Example test_factorial1: (factorial 3) = 6. -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. Example test_factorial2: (factorial 5) = (mult 10 12). -(* FILL IN HERE *) Admitted. +Proof. reflexivity. Qed. (** [] *) (** Again, we can make numerical expressions easier to read and write @@ -791,17 +800,17 @@ Proof. simpl. reflexivity. Qed. function. (It can be done with just one previously defined function, but you can use two if you need to.) *) -Definition ltb (n m : nat) : bool - (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. +Definition ltb (n m : nat) : bool := + 1 <=? m - n. Notation "x m = o -> n + m = m + o. Proof. - (* FILL IN HERE *) Admitted. + intros n m o. + intros H J. + rewrite -> H. + rewrite -> J. + reflexivity. +Qed. (** [] *) (** The [Admitted] command tells Coq that we want to skip trying @@ -985,7 +999,12 @@ Theorem mult_S_1 : forall n m : nat, m = S n -> m * (1 + n) = m * m. Proof. - (* FILL IN HERE *) Admitted. + intros n m. + intros H. + simpl. + rewrite <- H. + reflexivity. +Qed. (* (N.b. This proof can actually be completed with tactics other than [rewrite], but please do use [rewrite] for the sake of the exercise.) @@ -1213,15 +1232,21 @@ Qed. Theorem andb_true_elim2 : forall b c : bool, andb b c = true -> c = true. Proof. - (* FILL IN HERE *) Admitted. -(** [] *) + intros [] []. + - reflexivity. + - intros H. destruct H. reflexivity. + - reflexivity. + - intros H. destruct H. reflexivity. +Qed. (** **** Exercise: 1 star, standard (zero_nbeq_plus_1) *) Theorem zero_nbeq_plus_1 : forall n : nat, 0 =? (n + 1) = false. Proof. - (* FILL IN HERE *) Admitted. -(** [] *) + intros []. + - reflexivity. + - reflexivity. +Qed. (* ================================================================= *) (** ** More on Notation (Optional) *) @@ -1327,9 +1352,11 @@ Theorem identity_fn_applied_twice : (forall (x : bool), f x = x) -> forall (b : bool), f (f b) = b. Proof. - (* FILL IN HERE *) Admitted. - -(** [] *) + intros f x b. + rewrite -> x. + rewrite -> x. + reflexivity. +Qed. (** **** Exercise: 1 star, standard (negation_fn_applied_twice) @@ -1360,7 +1387,12 @@ Theorem andb_eq_orb : (andb b c = orb b c) -> b = c. Proof. - (* FILL IN HERE *) Admitted. + intros [] []. + - reflexivity. + - simpl. intros H. rewrite -> H. reflexivity. + - simpl. intros H. rewrite -> H. reflexivity. + - reflexivity. +Qed. (** [] *) @@ -1399,11 +1431,19 @@ Inductive bin : Type := for binary numbers, and a function [bin_to_nat] to convert binary numbers to unary numbers. *) -Fixpoint incr (m:bin) : bin - (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. +Fixpoint incr (m:bin) : bin := + match m with + | Z => B Z + | A n => B n + | B n => A (incr n) + end. -Fixpoint bin_to_nat (m:bin) : nat - (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. +Fixpoint bin_to_nat (m:bin) : nat := + match m with + | Z => 0 + | A n => 2 * (bin_to_nat n) + | B n => 1 + 2 * (bin_to_nat n) + end. (** (b) Write five unit tests [test_bin_incr1], [test_bin_incr2], etc. for your increment and binary-to-unary functions. (A "unit @@ -1413,10 +1453,31 @@ Fixpoint bin_to_nat (m:bin) : nat then converting it to unary should yield the same result as first converting it to unary and then incrementing. *) -(* FILL IN HERE *) +Example test_bin_incr1 : incr Z = B Z. +Proof. reflexivity. Qed. +Example test_bin_incr2 : incr (B Z) = A (B Z). +Proof. reflexivity. Qed. +Example test_bin_incr3 : incr (A (B Z)) = B (B Z). +Proof. reflexivity. Qed. +Example test_bin_incr4 : incr (B (B Z)) = A (A (B Z)). +Proof. reflexivity. Qed. +Example test_bin_incr5 : incr (A (A (B Z))) = B (A (B Z)). +Proof. reflexivity. Qed. + +Example test_bin_to_nat0 : bin_to_nat Z = 0. +Proof. reflexivity. Qed. +Example test_bin_to_nat1 : bin_to_nat (B Z) = 1. +Proof. reflexivity. Qed. +Example test_bin_to_nat2 : bin_to_nat (A (B Z)) = 2. +Proof. reflexivity. Qed. +Example test_bin_to_nat3 : bin_to_nat (B (B Z)) = 3. +Proof. reflexivity. Qed. +Example test_bin_to_nat4 : bin_to_nat (A (A (B Z))) = 4. +Proof. reflexivity. Qed. (* Do not modify the following line: *) Definition manual_grade_for_binary : option (nat*string) := None. + (** [] *) (* Wed Jan 9 12:02:44 EST 2019 *)