(** * Basics: Functional Programming in Coq *) (* ################################################################# *) (** * Data and Functions *) (* ================================================================= *) (** ** Enumerated Types *) (** In Coq, we can build practically everything from first principles... *) (* ================================================================= *) (** ** Days of the Week *) (** A datatype definition: *) Inductive day : Type := | monday | tuesday | wednesday | thursday | friday | saturday | sunday. (** A function on days: *) Definition next_weekday (d:day) : day := match d with | monday => tuesday | tuesday => wednesday | wednesday => thursday | thursday => friday | friday => monday | saturday => monday | sunday => monday end. (** Simplification: *) Compute (next_weekday friday). (* ==> monday : day *) Compute (next_weekday (next_weekday saturday)). (* ==> tuesday : day *) (** Second, we can record what we _expect_ the result to be in the form of a Coq example: *) Example test_next_weekday: (next_weekday (next_weekday saturday)) = tuesday. (** A proof script giving evidence for the claim: *) Proof. simpl. reflexivity. Qed. (** The [Require Export] statement on the next line tells Coq to use the [String] module from the standard library. We'll use strings ourselves in later chapters, but we need to [Require] it here so that the grading scripts can use it for internal purposes. *) From Coq Require Export String. (* ================================================================= *) (** ** Booleans *) (** Another familiar enumerated type: *) Inductive bool : Type := | true | false. (** Booleans are also available from Coq's standard library, but in this course we'll define everything from scratch, just to see how it's done. *) Definition negb (b:bool) : bool := match b with | true => false | false => true end. Definition andb (b1:bool) (b2:bool) : bool := match b1 with | true => b2 | false => false end. Definition orb (b1:bool) (b2:bool) : bool := match b1 with | true => true | false => b2 end. (** Note the syntax for defining multi-argument functions ([andb] and [orb]). *) Example test_orb1: (orb true false) = true. Proof. simpl. reflexivity. Qed. Example test_orb2: (orb false false) = false. Proof. simpl. reflexivity. Qed. Example test_orb3: (orb false true) = true. Proof. simpl. reflexivity. Qed. Example test_orb4: (orb true true) = true. Proof. simpl. reflexivity. Qed. (** We can define new symbolic notations for existing definitions. *) Notation "x && y" := (andb x y). Notation "x || y" := (orb x y). Example test_orb5: false || false || true = true. Proof. simpl. reflexivity. Qed. (** **** Exercise: 1 star, standard (nandb) The command [Admitted] can be used as a placeholder for an incomplete proof. We use it in exercises to indicate the parts that we're leaving for you -- i.e., your job is to replace [Admitted]s with real proofs. Remove "[Admitted.]" and complete the definition of the following function; then make sure that the [Example] assertions below can each be verified by Coq. (I.e., fill in each proof, following the model of the [orb] tests above, and make sure Coq accepts it.) 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. Example test_nandb1: (nandb true false) = true. (* FILL IN HERE *) Admitted. Example test_nandb2: (nandb false false) = true. (* FILL IN HERE *) Admitted. Example test_nandb3: (nandb false true) = true. (* FILL IN HERE *) Admitted. Example test_nandb4: (nandb true true) = false. (* FILL IN HERE *) Admitted. (** [] *) (** Most exercises are omitted from the "terse" version of the notes used in lecture. The "full" version contains both the assigned reading and all the exercises for your homework assignment. *) (* ================================================================= *) (** ** Types *) (** Every expression in Coq has a type, describing what sort of thing it computes. The [Check] command asks Coq to print the type of an expression. *) Check true. (* ===> true : bool *) (** If the expression after [Check] is followed by a colon and a type, Coq will verify that the type of the expression matches the given type and halt with an error if not. *) Check true : bool. Check (negb true) : bool. (** Functions like [negb] itself are also data values, just like [true] and [false]. Their types are called _function types_, and they are written with arrows. *) Check negb : bool -> bool. (* ================================================================= *) (** ** New Types from Old *) (** A more interesting type definition: *) Inductive rgb : Type := | red | green | blue. Inductive color : Type := | black | white | primary (p : rgb). (** Atomic identifiers like [red], [green], [blue], [black], [white], and [primary] (and [true], [false], [monday], etc.) are _constructors_. From these, we build _constructor expressions_, each of which is either a simple constructor or a constructor applied to one or more arguments (each of which is in turn a constructor expression). *) (** Let's look at this in a little more detail. Every inductively defined type ([day], [bool], [rgb], [color], etc.) describes a set of _constructor expressions_ built from _constructors_ - We start with an infinite set of _constructors_. E.g., [red], [primary], [true], [false], [monday], etc. are constructors. - _Constructor expressions_ are formed by applying constructors to zero or more constructor expressions. E.g., [red], [true], [primary], [primary red], [red primary], [red true], [primary (primary primary)], etc. - Each [Inductive] definition carves out a subset of these constructor expressions and gives it a name, like [bool], [rgb], or [color]. *) (** In particular, the definitions of [rgb] and [color] say how constructor expressions belonging to the sets [rgb] and [color] can be built: - the constructor expression [red] belongs to the set [rgb], as do the constructor expressions [green] and [blue]; - the constructor expressions [black] and [white] belong to the set [color]; - if [p] is a constructor expression belonging to the set [rgb], then [primary p] (pronounced "the constructor [primary] applied to the argument [p]") is a constructor expression belonging to the set [color]; and - constructor expressions formed in these ways are the _only_ ones belonging to the sets [rgb] and [color]. *) (** We can define functions on colors using pattern matching just as we did for [day] and [bool]. *) Definition monochrome (c : color) : bool := match c with | black => true | white => true | primary p => false end. (** Since the [primary] constructor takes an argument, a pattern matching [primary] should include either a variable (as above -- note that we can choose its name freely) or a constant of appropriate type (as below). *) Definition isred (c : color) : bool := match c with | black => false | white => false | primary red => true | primary _ => false end. (** The pattern "[primary _]" here is shorthand for "the constructor [primary] applied to any [rgb] constructor except [red]." (The wildcard pattern [_] has the same effect as the dummy pattern variable [p] in the definition of [monochrome].) *) (* ================================================================= *) (** ** Modules *) (** [Module] declarations create separate namespaces. *) Module Playground. Definition b : rgb := blue. End Playground. Definition b : bool := true. Check Playground.b : rgb. Check b : bool. (* ================================================================= *) (** ** Tuples *) Module TuplePlayground. (** A nybble is half a byte -- that is, four bits. *) Inductive bit : Type := | B0 | B1. Inductive nybble : Type := | bits (b0 b1 b2 b3 : bit). Check (bits B1 B0 B1 B0) : nybble. (** We deconstruct a nybble by pattern-matching. *) Definition all_zero (nb : nybble) : bool := match nb with | (bits B0 B0 B0 B0) => true | (bits _ _ _ _) => false end. Compute (all_zero (bits B1 B0 B1 B0)). (* ===> false : bool *) Compute (all_zero (bits B0 B0 B0 B0)). (* ===> true : bool *) End TuplePlayground. (* ================================================================= *) (** ** Numbers *) Module NatPlayground. (** There are many representations possible of natural numbers. You may be familiar with decimal, hexadecimal, octal, and binary. For simplicity in proofs, we choose unary: [O] represents zero, and [S] represents adding an additional unary digit. That is, [S] is the "successor" operation, which, when applied to the representation of n, gives the representation of n+1. *) Inductive nat : Type := | O | S (n : nat). (** With this definition, 0 is represented by [O], 1 by [S O], 2 by [S (S O)], and so on. *) (** Again, let's look at this in a little more detail. The definition of [nat] says how expressions in the set [nat] can be built: - the constructor expression [O] belongs to the set [nat]; - if [n] is a constructor expression belonging to the set [nat], then [S n] is also a constructor expression belonging to the set [nat]; and - constructor expressions formed in these two ways are the only ones belonging to the set [nat]. *) (** Critical point: this just defines a _representation_ of numbers -- a unary notation for writing them down. The names [O] and [S] are arbitrary. They are just two different "marks", with no intrinsic meaning. We could just as well represent numbers with different marks: *) Inductive nat' : Type := | stop | tick (foo : nat'). (** The _interpretation_ of these marks comes from how we use them to compute. *) Definition pred (n : nat) : nat := match n with | O => O | S n' => n' end. End NatPlayground. (** As a convenience, standard decimal numerals can be used as a shorthand for sequences of applications of [S] to [O]; Coq uses the same shorthand when printing things: *) Check (S (S (S (S O)))). (* ===> 4 : nat *) Definition minustwo (n : nat) : nat := match n with | O => O | S O => O | S (S n') => n' end. Compute (minustwo 4). (* ===> 2 : nat *) (** Recursive functions are defined using the [Fixpoint] keyword. *) Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. (** We could define [oddb] by a similar [Fixpoint] declaration, but here is a simpler way: *) Definition oddb (n:nat) : bool := negb (evenb n). Example test_oddb1: oddb 1 = true. Proof. simpl. reflexivity. Qed. Example test_oddb2: oddb 4 = false. Proof. simpl. reflexivity. Qed. (** A multi-argument recursive function. *) Module NatPlayground2. Fixpoint plus (n : nat) (m : nat) : nat := match n with | O => m | S n' => S (plus n' m) end. Compute (plus 3 2). (* ===> 5 : nat *) (* [plus 3 2] i.e. [plus (S (S (S O))) (S (S O))] ==> [S (plus (S (S O)) (S (S O)))] by the second clause of the [match] ==> [S (S (plus (S O) (S (S O))))] by the second clause of the [match] ==> [S (S (S (plus O (S (S O)))))] by the second clause of the [match] ==> [S (S (S (S (S O))))] by the first clause of the [match] i.e. [5] *) (** Another: *) Fixpoint mult (n m : nat) : nat := match n with | O => O | S n' => plus m (mult n' m) end. Example test_mult1: (mult 3 3) = 9. Proof. simpl. reflexivity. Qed. (** Pattern-matching two values at the same time: *) Fixpoint minus (n m:nat) : nat := match n, m with | O , _ => O | S _ , O => n | S n', S m' => minus n' m' end. End NatPlayground2. (** Again, we can make numerical expressions easier to read and write by introducing notations for addition, multiplication, and subtraction. *) Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope. Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope. Check ((0 + 1) + 1) : nat. (** When we say that Coq comes with almost nothing built-in, we really mean it: even equality testing is a user-defined operation! Here is a function [eqb], which tests natural numbers for [eq]uality, yielding a [b]oolean. Note the use of nested [match]es (we could also have used a simultaneous match, as we did in [minus].) *) Fixpoint eqb (n m : nat) : bool := match n with | O => match m with | O => true | S m' => false end | S n' => match m with | O => false | S m' => eqb n' m' end end. (** Similarly, the [leb] function tests whether its first argument is less than or equal to its second argument, yielding a boolean. *) Fixpoint leb (n m : nat) : bool := match n with | O => true | S n' => match m with | O => false | S m' => leb n' m' end end. Example test_leb1: leb 2 2 = true. Proof. simpl. reflexivity. Qed. Example test_leb2: leb 2 4 = true. Proof. simpl. reflexivity. Qed. Example test_leb3: leb 4 2 = false. Proof. simpl. reflexivity. Qed. (** We'll be using these (especially [eqb]) a lot, so let's give them infix notations. *) Notation "x =? y" := (eqb x y) (at level 70) : nat_scope. Notation "x <=? y" := (leb x y) (at level 70) : nat_scope. Example test_leb3': (4 <=? 2) = false. Proof. simpl. reflexivity. Qed. (** We have two notions of equality: - [=] is already defined in Coq and that we attempt to _prove_. - [=?] is something we coded up and that Coq _computes_. *) (* ################################################################# *) (** * Proof by Simplification *) (** A general property of natural numbers: *) Theorem plus_O_n : forall n : nat, 0 + n = n. Proof. intros n. simpl. reflexivity. Qed. (** The [simpl] tactic is actually redundant, as [reflexivity] already does some simplification for us: *) Theorem plus_O_n' : forall n : nat, 0 + n = n. Proof. intros n. reflexivity. Qed. (** Any other (fresh) identifier could be used instead of [n]: *) Theorem plus_O_n'' : forall n : nat, 0 + n = n. Proof. intros m. reflexivity. Qed. (** Other similar theorems can be proved with the same pattern. *) Theorem plus_1_l : forall n:nat, 1 + n = S n. Proof. intros n. reflexivity. Qed. Theorem mult_0_l : forall n:nat, 0 * n = 0. Proof. intros n. reflexivity. Qed. (* ################################################################# *) (** * Proof by Rewriting *) (** A (slightly) more interesting theorem: *) Theorem plus_id_example : forall n m:nat, n = m -> n + n = m + m. Proof. (* move both quantifiers into the context: *) intros n m. (* move the hypothesis into the context: *) intros H. (* rewrite the goal using the hypothesis: *) rewrite -> H. reflexivity. Qed. (** The uses of [intros] name the hypotheses as they are moved to the context. The [rewrite] needs to know which equality is being used and in which direction to do the replacement. *) (** The [Check] command can also be used to examine the statements of previously declared lemmas and theorems. The two examples below are lemmas about multiplication that are proved in the standard library. (We will see how to prove them ourselves in the next chapter.) *) Check mult_n_O. (* ===> forall n : nat, 0 = n * 0 *) Check mult_n_Sm. (* ===> forall n m : nat, n * m + n = n * S m *) (** We can use the [rewrite] tactic with a previously proved theorem instead of a hypothesis from the context. If the statement of the previously proved theorem involves quantified variables, as in the example below, Coq tries to instantiate them by matching with the current goal. *) Theorem mult_n_0_m_0 : forall p q : nat, (p * 0) + (q * 0) = 0. Proof. intros p q. rewrite <- mult_n_O. rewrite <- mult_n_O. reflexivity. Qed. (* ################################################################# *) (** * Proof by Case Analysis *) (** Sometimes simple calculating and rewriting are not enough... *) Theorem plus_1_neq_0_firsttry : forall n : nat, (n + 1) =? 0 = false. Proof. intros n. simpl. (* does nothing! *) Abort. (** We can use [destruct] to perform case analysis: *) Theorem plus_1_neq_0 : forall n : nat, (n + 1) =? 0 = false. Proof. intros n. destruct n as [| n'] eqn:E. - reflexivity. - reflexivity. Qed. (** Note the "bullets" marking the proofs of the two subgoals. *) (** Another example (using booleans): *) Theorem negb_involutive : forall b : bool, negb (negb b) = b. Proof. intros b. destruct b eqn:E. - reflexivity. - reflexivity. Qed. (** We can have nested subgoals (and we use different "bullets" to mark the inner ones): *) Theorem andb_commutative : forall b c, andb b c = andb c b. Proof. intros b c. destruct b eqn:Eb. - destruct c eqn:Ec. + reflexivity. + reflexivity. - destruct c eqn:Ec. + reflexivity. + reflexivity. Qed. (** Besides [-] and [+], we can use [*] (asterisk) or any repetition of a bullet symbol (e.g. [--] or [***]) as a bullet. We can also enclose sub-proofs in curly braces: *) Theorem andb_commutative' : forall b c, andb b c = andb c b. Proof. intros b c. destruct b eqn:Eb. { destruct c eqn:Ec. { reflexivity. } { reflexivity. } } { destruct c eqn:Ec. { reflexivity. } { reflexivity. } } Qed. (** One final convenience: Instead of intros x y. destruct y as [|y] eqn:E. we can write intros x [|y]. *) Theorem plus_1_neq_0' : forall n : nat, (n + 1) =? 0 = false. Proof. intros [|n]. - reflexivity. - reflexivity. Qed. (** If there are no constructor arguments that need names, we can just write [[]] to get the case analysis. *) Theorem andb_commutative'' : forall b c, andb b c = andb c b. Proof. intros [] []. - reflexivity. - reflexivity. - reflexivity. - reflexivity. Qed. (* ################################################################# *) (** * Testing Your Solutions *) (** Run [make BasicsTest.vo] to check your solution for common errors: - Deleting or renaming exercises. - Changing what you were supposed to prove. - Leaving the exercise unfinished. *)