# File 0

# Functional Programming in Coq

Due | 2019-9-12 11:45AM |

Reading | Programs and Proofs: Chapter 2, Mathematical Components: Chapter 1 |

Link | https://github.ccs.neu.edu/verifcomp/19/asgn/0.v |

Require Import mathcomp.ssreflect.all_ssreflect.

Set Implicit Arguments.

Unset Strict Implicit.

Unset Printing Implicit Defensive.

Set Bullet Behavior "Strict Subproofs".

Exercise 1. Define the following list functions. Example uses are given via
"Example". Replace Admitted. with done. Qed. once you have defined the function to
have the example run.

Fixpoint nonzeros (l:seq nat) : seq nat

. Admitted.

Example test_nonzeros:

nonzeros [:: 0;1;0;2;3;0;0] = [:: 1;2;3].

Admitted.

Fixpoint oddmembers (l:seq nat) : seq nat

. Admitted.

Example test_oddmembers:

oddmembers [:: 0;1;0;2;3;0;0] = [:: 1;3].

Admitted.

Definition countoddmembers (l:seq nat) : nat

. Admitted.

Example test_countoddmembers1:

countoddmembers [:: 1;0;3;1;4;5] = 4.

Admitted.

Example test_countoddmembers2:

countoddmembers [:: 0;2;4] = 0.

Admitted.

Example test_countoddmembers3:

countoddmembers nil = 0.

Admitted.

Exercise 2. A bag (or multiset) is like a set, except that each element can appear
multiple times rather than just once. One possible representation for a bag of
numbers is as a list.

Definition bag := seq nat.

Complete the following definitions for the functions count, sum, add, and
member for bags.

Fixpoint count (v:nat) (s:bag) : nat

. Admitted.

Example test_count1: count 1 [:: 1;2;3;1;4;1] = 3.

Admitted.

Example test_count2: count 6 [:: 1;2;3;1;4;1] = 0.

Admitted.

Definition sum : bag -> bag -> bag

. Admitted.

Example test_sum1: count 1 (sum [:: 1;2;3] [:: 1;4;1]) = 3.

Admitted.

Definition add (v:nat) (s:bag) : bag

. Admitted.

Example test_add1: count 1 (add 1 [:: 1;4;1]) = 3.

Admitted.

Example test_add2: count 5 (add 1 [:: 1;4;1]) = 0.

Admitted.

Definition member (v:nat) (s:bag) : bool

. Admitted.

Example test_member1: member 1 [:: 1;4;1] = true.

Admitted.

Example test_member2: member 2 [:: 1;4;1] = false.

Admitted.

Fixpoint remove_one (v:nat) (s:bag) : bag

. Admitted.

Example test_remove_one1:

count 5 (remove_one 5 [:: 2;1;5;4;1]) = 0.

Admitted.

Example test_remove_one2:

count 5 (remove_one 5 [:: 2;1;4;1]) = 0.

Admitted.

Example test_remove_one3:

count 4 (remove_one 5 [:: 2;1;4;5;1;4]) = 2.

Admitted.

Example test_remove_one4:

count 5 (remove_one 5 [:: 2;1;5;4;5;1;4]) = 1.

Admitted.

Fixpoint remove_all (v:nat) (s:bag) : bag

. Admitted.

Example test_remove_all1: count 5 (remove_all 5 [:: 2;1;5;4;1]) = 0.

Admitted.

Example test_remove_all2: count 5 (remove_all 5 [:: 2;1;4;1]) = 0.

Admitted.

Example test_remove_all3: count 4 (remove_all 5 [:: 2;1;4;5;1;4]) = 2.

Admitted.

Example test_remove_all4: count 5 (remove_all 5 [:: 2;1;5;4;5;1;4;5;1;4]) = 0.

Admitted.

Fixpoint subset (s1:bag) (s2:bag) : bool

. Admitted.

Example test_subset1: subset [:: 1;2] [:: 2;1;4;1] = true.

Admitted.

Example test_subset2: subset [:: 1;2;2] [:: 2;1;4;1] = false.

Admitted.

Exercise 3. Define my_mul, but use a call to nat_rec, not Fixpoint.

Definition my_mul (n m : nat) : nat

. Admitted.

Exercise 4. Design an uninhabited inductive type that is different from the two examples
given in section 2.3 of Programs and Proofs.
Exercise 5. Design a function power_two that takes a nat and returns 2 to
that power.
Exercise 6. Design a function lt3 that takes a nat and returns true if
the input is less than 3, and false otherwise.
Exercise 7. Build an inductive type that represents propositional logic
without variables:
True | False | ~X | X /\ X | X \/ X | X => X
Exercise 8. (MASTERS CREDIT ONLY) Design the function interleave, that
takes two list of numbers and produces a list of their items, alternating from
each list. If the lists have different lengths, just finish with all the
remaining items of the longer list.
Exercise 9. Design the function powerlist which returns all possible
sublists of a list of numbers. A sublist of a list is any list whose items
appear in the same relative order that they do in the initial list and all of
the items appear in the initial list. Assume the initial list given to powerlist
contains no duplicates.