(* * CS 598 TLR * Artifact 2: Tactics * Student Copy * * READ ME FIRST: As always, the emphasis is on learning, in this case * what it is like to use tactics. So you are graded for the discussion * question at the bottom of this file, and not on your ability to finish * the proofs. * * At the end of this class (or, if you're not attending in person, * sometime before 1230 PM the day of class) you'll post on the forum * about what you found challenging, what you enjoyed, how the experience * compared to the experience from last week, and how you wish you could * improve the automation to make the experience better. * If you or someone you're working with is a Coq wizard already, * and you know about automation that already exists that makes the * job easy, definitely take note of that and mention it as well. * * If you have a lot of trouble with a proof, it's OK to ask me for help * (or post in the forum if you're not here in person). It's also OK to * ask people in other groups. * * But again, as before, this is about the journey, not the destination. * * NOTE: To navigate this file, you will want to step down (the down arrow in the * top left corner) past definitions and proofs, step back up (the up arrow in the * top left corner) to back up, and step to a particular line using the go to * cursor button (the curved arrow in the top left corner). As you do that, * Coq will execute automation, and type check definitions and proofs. * The output will appear in the buffer on the right. *) (* * Some built-in datatypes we'll use in this exercise (equality in Coq is included by default): *) Require Import Nat. (* natural numbers *) Require Import List. (* polymorphic lists *) Require Import Ascii. (* characters *) (* * Some syntax, separate from the datatype definitions: *) Open Scope char_scope. Import ListNotations. (* * In addition to the tactics we'll see today, Coq has a notion of commands. * A command is kind of like a tactic, but it doesn't need to happen inside * of a proof, it can happen anywhere. These can produce new proofs, they can * print proofs for you, they can help you search for information, and they can * do a whole lot more. These are implemented inside of OCaml, either in Coq itself * or in plugins, which we'll see in later classes. * * Why does this matter right now? Well, in Coq, there's a nice command that lets * you print the definitions you just imported, and see how they're defined. * * So, for example, here's our list datatype: *) Print list. (* polymorphic lists *) (* * It is exactly like lists in Agda, albeit with less unicode :). * Though we still get the syntax [] for nil and :: for cons (two colons this time). * * This lets us define our example lists just like we did in Agda. * Note that in Coq, the type is not on a separate line from the definition; * it looks a lot more like OCaml whereas Agda looks a lot more like Haskell. * (This is no coincidence; Coq is implemented in OCaml, and Agda is implemented * in Haskell, so the communities are pretty tightly coupled). *) (* The empty list of natural numbers *) Definition empty_nat : list nat := []. (* The empty list of characters *) Definition empty_char : list ascii := []. (* A list [1; 2; 3; 4] *) Definition one_two_three_four : list nat := [1; 2; 3; 4]. (* syntax for 1 :: 2 :: 3 :: 4 :: [] *) (* A list [x; y; z] *) Definition x_y_z : list ascii := ["x"; "y"; "z"]. (* * NOTE: Since Coq notation is kept separately from the definitions, it is easy * to figure out how to expand the syntax, as long as you're inside of the IDE. * In CoqIDE, what you do is go to the View menu and uncheck "Display notations". * Give it a try right now. *) Print empty_nat. Print one_two_three_four. (* * Now reenable syntax if you prefer (by checking "Display notations" in that same menu)---or * leave it as is if you'd rather see all syntax expanded. Your choice! * * Our length function is defined for us in the standard library, but I will * redefine it here to show it to you in more detail, and to minimize reliance on * the standard library for now. Let's define length: *) Fixpoint length {A : Type} (l : list A) : nat := match l with | [] => 0 (* empty case *) | _ :: tl => S (length tl) (* cons case *) end. (* * This is defined the same wqay as in Agda, but the pattern matching syntax is quite * different, and we must tell Coq explicitly to recurse by declaring a Fixpoint. * * Coq has a limited form of recursion, since it needs to terminate to avoid * paradoxes. Basically, one of the arguments needs to provably get smaller every time. * Like in our length definition, we recurse on only the tail of the list. * Coq checks this guard for recursion syntactically. * * Coq supports one thing Agda doesn't support natively---induction. * In addition to pattern matching and recursing over inductive types, * we can now induct over them. Every inductive time comes equipped with * an induction principle. The induction principle for nat looks exactly * like the way we induct over natural numbers in mathematics * (the "Check" command checks the type of its argument): *) Check nat_rect. (* * We have that for any P : nat -> Type (this is called the _inductive motive_), * if we have a proof of P 0, plus a proof that for any n, P n implies P (S n), * then we can construct a proof of forall n, P n. * * The induction principle for lists looks similar, but with nil in place of 0, * and cons in place of S, with some extra logic to deal with the new element consed * onto the list: *) Check list_rect. (* * For any type A and motive P : list A -> Type, if we have a proof of P [], * plus a proof that for any element a and list l, P l implies P (a :: l), * then we can construct a proof of forall (l : list A), P l. * * Induction and pattern matching plus syntactically guarded terminating recursion are * deeply and beautifully related to one another. You actually need only one or the other * in your language! Coq makes the decision to support recursion natively. * Then, every time you define a new inductive datatype, Coq automatically generates * induction principles defined in terms of recursion: *) Print nat_rect. Print list_rect. (* * The first thing that's cool about this is that we can write our functions * using these induction principles. Here's an alternative way to define list length: *) Definition length' {A : Type} (l : list A) : nat := list_rect (fun _ => nat) (* motive *) O (* empty or base case*) (fun (a : A) (tl : list A) (length_tl : nat) => (* cons or inductive case *) S length_tl) l. (* argument to induct over *) (* * Take a second to look at these side-by-side. *) Print length. Print length'. (* * The recursive argument---length tl in the original---is now generated automatically * in the inductive case. I've called it length_tl for the sake of making it easier * to relate to the original definition. * * The absolute coolest thing about this is that we get automation---by way of tactics---to * prove things by induction. By Curry-Howard, our length function is a proof, so we * can actually define the same we'd write a proof. Let's do that. *) Theorem length'' {A : Type}: list A -> nat. Proof. intros l. (* bind l : list A in our environment. *) induction l as [| h tl length_tl]. (* induct over l *) - apply 0. (* empty or base case *) - apply S. apply length_tl. (* cons or inductive case *) Defined. (* * Of course, there are many proofs that list A -> nat, and not all of them are the * length function. Some of them are quite boring. We could prove this theorem * by just returning 0 all the time, if we'd like. But the important thing here is * that tactics are really search procedures for proof terms. They sort of compile * to proof terms, if you will. So we can print our proof of length'': *) Print length''. (* * And see that it's the same as length'. Indeed: *) Theorem length''_OK {A : Type}: forall (l : list A), length'' l = length' l. Proof. intros l. reflexivity. Qed. (* * In general, we write "Qed" when we don't care about the content of our proof. That is, * when we don't want to use it like a program, and we care just about its type---the theorem * it proves---from here on out. We write "Defined" when we do care about the * content. Personally, I always write "Defined" in my own proofs, but I'm a weird * type theorist and nobody really likes us. *) (* * EXERCISE 1: It's your turn to write some functions. Let's write app and rev like * we did in Agda last week---but let's use induction instead of recursion, and let's * write it using tactics. (This is something Coq programmers occasionally do, * though it's more common to write functions like app and rev directly.) *) (* append two lists *) Theorem app {A : Type} : list A -> list A -> list A. Proof. intros l1. (* bind l1 *) induction l1 as [| h tl app_tl]; intros l2. (* induct over l1, then bind l2 in both cases *) - apply l2. (* base case *) - apply (h :: app_tl l2). (* inductive case *) Defined. (* reverse a list *) Theorem rev {A : Type} : list A -> list A. Proof. (* your tactics here *) Admitted. (* <- change to Defined when done *) (* * We can test your rev function like we did in Agda * (Example means the same thing as Theorem basically, it's just nice notation): *) (* empty_nat doesn't change *) Example rev_empty_nat_empty_nat : rev empty_nat = empty_nat. Proof. reflexivity. Defined. (* empty_char doesn't change *) Example rev_empty_char_empty_char : rev empty_char = empty_char. Proof. reflexivity. Defined. (* [1; 2; 3; 4] becomes [4; 3; 2; 1] *) Example rev_1_2_3_4_4_3_2_1 : rev one_two_three_four = [4; 3; 2; 1]. Proof. reflexivity. Defined. (* ["x"; "y"; "z"] becomes ["z"; "y"; "x"] *) Example rev_x_y_z_z_y_x : rev x_y_z = ["z"; "y"; "x"]. Proof. reflexivity. Defined. (* * What does reflexivity do? It applies the refl constructor for the equality type, * much like we saw in Agda. In Coq, that constructor is called eq_refl: *) Print rev_empty_nat_empty_nat. Print rev_empty_char_empty_char. Print rev_1_2_3_4_4_3_2_1. Print rev_x_y_z_z_y_x. (* * And the type is called eq: *) Print eq. (* * Actually, though, let's do better. We have a proof assistant---so why rely * just on testing? Here, we have reference implementations of append and reverse * inside of the standard library. So let's prove your reverse function correct. * * EXERCISE 2: I've given you the proof that my append function behaves the same as Coq's * append function. Write the proof that your reverse function behaves the same as Coq's * reverse function. *) (* app is correct *) Lemma app_OK {A : Type}: forall (l1 l2 : list A), app l1 l2 = List.app l1 l2. Proof. intros. (* bind l1 and l2 *) induction l1. (* induct over l1 *) - reflexivity. (* these are computationally equal *) - simpl. (* reduce both sides neatly *) rewrite IHl1. (* use IHl1 to substitute (like subst in Agda) app l1 l2 with l1 ++ l2 *) reflexivity. (* these are computationally equal *) Qed. (* rev is correct *) Lemma rev_OK {A : Type}: forall (l : list A), rev l = List.rev l. Proof. (* your tactics here *) Admitted. (* <- change to Qed when done *) (* * There are two really cool things to note here. The first something quite beautiful * and general, which we saw in Agda last week---our proofs mirror the programs they're * about! And indeed, this mirrored structure exists at the term level, too (list_ind is * basically list_rect; the distinction doesn't matter for now, but ask if you're curious): *) Print app. Print app_OK. (* * The second cool thing to note is that, while we (or at least I) used tactics that are super close * to the terms they produce, we can get a bit fancier if we'd like. * We can actually get _way_ fancier, as we'll see in later classes, and write our own * custom tactics and apply them in our proof. But also, Coq already has a bunch of * those defined for us, so we might as well use them. Like what if we don't want to * think about reflexivity, we just want to use something like "that looks obvious"? * How about: *) Lemma app_OK' {A : Type}: forall (l1 l2 : list A), app l1 l2 = List.app l1 l2. Proof. induction l1; simpl; congruence. Qed. (* * Woah woah woah what happened there? Well, congruence is an equality solver (we'll see * these in future classes too!). It used this cute function, which is cong in Agda: *) Check f_equal. (* * And this, which is trans in Agda: *) Check eq_trans. (* * So we get a proof term that applies these for us and solves equalities: *) Print app_OK'. (* * Though this is different from the first proof we wrote, for the curious, * even though they prove the same theorem: *) Print app_OK. (* * Our first proof uses eq_ind_r (basically subst in Agda). The tactic "rewrite" * roughly generates a term that acts like subst in Agda, though it is a bit more * powerful sometimes (and can sometimes give you scary looking terms because of that). * * Oh, by the way, about subst in Agda? There's something cute about it---I didn't * say it last week, but it's really an induction principle for the inductive equality * type. That's why in Coq, it's called eq_rect (or eq_ind), like we have list_rect * (or list_ind). And it's defined by matching over the equality type and destructing to * the singular reflexivity case: *) Print eq_rect. (* * Coq also defines inverses of eq_rect and eq_ind, which just swap x and y using * symmetry of equality: *) Print eq_rect_r. (* * NOTE: You can switch between eq_rect_r and eq_rect by using "rewrite <-" versus "rewrite" * (similarly for eq_ind). This is useful when you have some x = y as a hypothesis, and your * goal has a y in it, but you want an x in it. * * EXERCISE 3: Prove rev_OK again, but this time using heavier automation. * (If your first proof was already heavily automated, then expand it into something * longer that applies each step explicitly.) *) (* rev is still correct *) Lemma rev_OK' {A : Type}: forall (l : list A), rev l = List.rev l. Proof. (* your proof here *) Admitted. (* <- change to Qed when done *) (* * With all of that in mind, let's prove app_nil_l and app_nil_r. * * EXERCISES 4 and 5: Prove app_nil_l and app_nil_r. * You may reference the Agda proofs from last week if it helps. *) (* left identity of nil for append *) Theorem app_nil_l {A : Type}: forall (l : list A), app [] l = l. Proof. (* your proof here *) Admitted. (* <- change to Qed when done *) (* right identity of nil for append *) Theorem app_nil_r {A : Type}: forall (l : list A), app l [] = l. Proof. (* your proof here *) Admitted. (* <- change to Qed when done *) (* * Coq, like Agda, has symmetry of equality, and also a tactic for it: *) Theorem app_nil_r_sym {A : Type} : forall (l : list A), l = app l []. Proof. intros. symmetry. apply app_nil_r. Qed. (* * Though using fancier automation can let you avoid having to think about it, sometimes: *) Theorem app_nil_r_sym' {A : Type} : forall (l : list A), l = app l []. Proof. intros. auto using app_nil_r. Qed. (* * OK, now let's write the proof about reverse preserving the length function. * * NOTE: I'm omitting the lemma that helped you out last week---you can refer to the Agda * source if you want some help, or you can see organically why you might need to * cut a lemma. The latter is a really, really useful skill IRL, so I think it's * worth trying it that way. * * NOTE: There are also multiple ways to prove this. Like you can prove it like we did * in Agda last week, or you can use your proof of rev_OK to relate rev to Coq's List.rev, * then use functions in the Coq standard library. Either is fine! Both if you want. * * EXERCISE 6: Show that the reverse function preserves the length of the input list. *) (* any lemmas you want to write can go here *) Theorem rev_pres_length {A : Type}: forall (l : list A), length (rev l) = length l. Proof. (* your proof here *) Admitted. (* <- change to Qed when done *) (* * You're done with the proofs based on our Agda proofs last week! Some bonuses, * but if you don't have time, feel free to skip to the bottom. * * BONUS 1: Consider the alternative definition of rev defined below as rev_alt. * Prove rev_pres_length, but for this version of rev. How does it compare * to your old version of rev_pres_length? What changes? Why do you think this is? * * BONUS 2: Prove that rev and rev_alt behave the same way. *) (* auxiliary function *) Fixpoint rev_aux {A : Type} (l1 l2 : list A) : list A := match l1 with | [] => l2 | h :: tl => rev_aux tl (h :: l2) end. (* new definition of rev *) Definition rev_alt {A : Type} (l : list A) := rev_aux l []. (* Your theorems and proofs here *) (* * That's it for now! You can keep playing with other proofs if you have * extra time. For example, it might be fun to define your own inductive types, * like a binary tree, and then write proofs about those types. * * If you have a lot of extra time, I recommend looking at the * Coq source code on Github to get a sense for how it's implemented: * https://github.com/coq/coq. In any case, when we have 25 minutes * left of class, please do this: * * 1. Turn to your group and discuss the question below. * 2. Post your answer─just one answer for your group, clearly indicating * all members of the group. (If you are not here, and are working alone, * you can post your answer alone.) * 3. With 10 minutes left, finish posting your answer, so we can discuss * a bit as a class if time allows. We will follow up with more discussion * at the start of Tuesday's class. * * You'll be graded based on whether you post an answer, not based on * what it is, so don't worry too much about saying something silly. * * DISCUSSION QUESTION: What was it like constructing these proofs using tactics, * relative to your experience using Agda last week? In your experience so far, what do you * think the tradeoffs are of writing proofs as terms versus using tactics? * What did you find challenging about this experience, if anything? * What did you find helpful, if anything? Where do you wish you'd had more automation to help you out? *)