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

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
  . 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.