(** * Lab: Functional Programming in Coq This lab is designed as a file that you should download and complete in a Coq IDE. Before doing that, you need to install Coq. The installation instructions are on the course website. *) (* Exercise: mult2 [1 star]. Define a function that multiplies its input by 2. What is the function's type? What is the result of computing the function on 0? On 3110? *) (* Exercise: xor [1 star]. Define a function that computes the xor of two [bool] inputs. Do this by pattern matching on the inputs. What is the function's type? Compute all four possible combinations of inputs to test your function. *) (* Exercise: is_none [2 star]. Define a function that returns [true] if its input is [None], and [false] otherwise. Your function's type should be [forall A : Type, option A -> bool]. That means the function will actually need to take two inputs: the first has type [Type], and the second is an option. Hint: model your solution on [is_empty] in the notes for this lecture. *) Require Import List. Import ListNotations. (* Exercise: double_all [2 star]. There is a function [map] that was imported by the [Require Import List] command above. First, check its type with [Check map]. Explain that type in your own words. Second, print it with [Print map]. Note at the end of that which arguments are _implicit_. For a discussion of what implicit means, see the notes for this lecture. Third, use map to write your own function, which should double (i.e., multiply by 2) every value of a list. For example, [double_all [0;2;10]] should be [[0;4;20]]. *) (* Exercise: sum [2 star]. Write a function that sums all the natural numbers in a list. Implement this two different ways: - as a recursive function, using the [Fixpoint] syntax. - as a nonrecursive function, using [Definition] and an application of [fold_left]. *) Inductive day : Type := | sun : day | mon : day | tue : day | wed : day | thu : day | fri : day | sat : day. Definition next_day d := match d with | sun => mon | mon => tue | tue => wed | wed => thu | thu => fri | fri => sat | sat => sun end. (* Exercise: thu after wed [2 star]. State a theorem that says [thu] is the [next_day] after [wed]. Write down in natural language how you would informally explain to a human why this theorem is true. ---> Don't skip this "natural language" part of the exercise; it's crucial to develop intuition before proceeding. Prove the theorem in Coq. *) (* Exercise: wed before thu [3 star]. Below is a theorem that says if the day after [d] is [thu], then [d] must be [wed]. Write down in natural language how you would informally explain to a human why this theorem is true. ---> Don't skip this "natural language" part of the exercise; it's crucial to develop intuition before proceeding. Prove the theorem in Coq. To do that, delete the [Abort] command, which tells Coq to discard the theorem, then fill in your own proof. *) Theorem wed_proceeds_thu : forall d : day, next_day d = thu -> d = wed. Abort. (* Exercise: tl_opt [2 star]. Define a function [tl_opt] such that [tl_opt lst] return [Some t] if [t] is the tail of [lst], or [None] if [lst] is empty. We have gotten you started by providing an obviously incorrect definition, below; you should replace the body of the function with a correct definition. *) Definition tl_opt {A : Type} (lst : list A) : option (list A) := None. (* Here is a new tactic: [rewrite x]. If [x : e] is an assumption in the proof state, then [rewrite x] replaces [x] with [e] in the subgoal being proved. For example, here is a proof that incrementing 1 produces 2: *) Theorem inc1_is_2 : forall n, n=1 -> (fun x => x+1) n = 2. Proof. intros n n_is_1. rewrite n_is_1. trivial. Qed. (* Exercise: tl_opt correct [2 star]. Using [rewrite], prove the following theorems. For both, first explain in natural language why the theorem should hold, before moving on to prove it with Coq. *) Theorem nil_implies_tlopt_none : forall A : Type, forall lst : list A, lst = nil -> tl_opt lst = None. Abort. Theorem cons_implies_tlopt_some : forall {A : Type} (h:A) (t : list A) (lst : list A), lst = h::t -> tl_opt lst = Some t. Abort.