# 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
This assignment will familiarize you with functional programming in Coq. In many ways, this should be similar to similar functional programming you have done elsewhere (certainly in typed functional languages with algebraic data types), but there are some real differences, which this assignment will help you get used to.

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
Example test_nonzeros:
nonzeros [:: 0;1;0;2;3;0;0] = [:: 1;2;3].
Fixpoint oddmembers (l:seq nat) : seq nat
Example test_oddmembers:
oddmembers [:: 0;1;0;2;3;0;0] = [:: 1;3].
Definition countoddmembers (l:seq nat) : nat
Example test_countoddmembers1:
countoddmembers [:: 1;0;3;1;4;5] = 4.
Example test_countoddmembers2:
countoddmembers [:: 0;2;4] = 0.
Example test_countoddmembers3:
countoddmembers nil = 0.

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
Example test_count1: count 1 [:: 1;2;3;1;4;1] = 3.
Example test_count2: count 6 [:: 1;2;3;1;4;1] = 0.

Definition sum : bag -> bag -> bag
Example test_sum1: count 1 (sum [:: 1;2;3] [:: 1;4;1]) = 3.
Definition add (v:nat) (s:bag) : bag
Definition member (v:nat) (s:bag) : bool
Example test_member1: member 1 [:: 1;4;1] = true.
Example test_member2: member 2 [:: 1;4;1] = false.

Fixpoint remove_one (v:nat) (s:bag) : bag
Example test_remove_one1:
count 5 (remove_one 5 [:: 2;1;5;4;1]) = 0.
Example test_remove_one2:
count 5 (remove_one 5 [:: 2;1;4;1]) = 0.
Example test_remove_one3:
count 4 (remove_one 5 [:: 2;1;4;5;1;4]) = 2.
Example test_remove_one4:
count 5 (remove_one 5 [:: 2;1;5;4;5;1;4]) = 1.
Fixpoint remove_all (v:nat) (s:bag) : bag
Example test_remove_all1: count 5 (remove_all 5 [:: 2;1;5;4;1]) = 0.
Example test_remove_all2: count 5 (remove_all 5 [:: 2;1;4;1]) = 0.
Example test_remove_all3: count 4 (remove_all 5 [:: 2;1;4;5;1;4]) = 2.
Example test_remove_all4: count 5 (remove_all 5 [:: 2;1;5;4;5;1;4;5;1;4]) = 0.
Fixpoint subset (s1:bag) (s2:bag) : bool
Example test_subset1: subset [:: 1;2] [:: 2;1;4;1] = true.
Example test_subset2: subset [:: 1;2;2] [:: 2;1;4;1] = false.