(* When we start up the Coq toplevel a lot of basic stuff is loaded for us automatically--- much as occurs when we start up the ML top level. In Coq, though, it looks like we get a lot less, since we don't get just the operations---we must get facts about the operations, too. *) (* To see what's already loaded, enter "Print Libraries." *) Print Libraries. (* Use the navigation keys in the menu bar to step through your script. In this case, you want to make use of the downarrow. Use the "Navigation" menu to find out the key combination for the different navigation items. *) (* Library is the Coq word for a module defined in a file. Coq also uses modules, which resemble ML modules. *) (* Note that the libraries are "loaded" and "imported". If a library is imported, that means we can use their short names for accessing their members, i.e., we don't need to use their fully qualified names. *) (* We can print out the contents of an individual library. *) Print Datatypes. (* We can print out the definition of natural numbers in the Datatypes Library. *) Print nat. (* If we didn't happen to know what library nat belonged to we could ask Coq. *) Locate nat. (* We can also print out stuff in a separate window. Go to Queries -> Print and enter nat. Now it won't disappear if we type something else in our main window. *) (* nat is an inductive datatype and looks a lot like an algebraic datatype in ML. You can extract it to an ML datatype using the command "Extraction nat." *) Extraction nat. (* For fun, you can set the target language to, e.g., Haskell and get a Haskell datatype. *) Extraction Language Haskell. Extraction nat. (* The significant difference between Coq and these other languages is that the Inductive datatype nat is itself given a type, Set. We'll talk more about that later. *) (* Inductive datatypes are Coq's way of inserting axioms into our environment. In this case, we'll list the axioms on the board. *) (* Exercise 1: Proving nat. *) Goal nat. Proof. (* at this point, let's stop and try to solve the problem on the board *) exact (S (S O)). Qed. (* We used the "exact" tactic to explicitly supply the whole proof. *) (* We can print out our proof. We didn't give our proof an explicit name, so Coq generated its own name, "Unnamed_thm." *) Print Unnamed_thm. Print All. (* That was our first proof. Everything we do from here on in, will be essentially what we just did: supply a program which has the type of the statement of our goal. *) (* Certain facts about nat are defined in the Datatypes library as well. Let's take a look at them. *) Print Datatypes. (* When nat is defined three functions are automatically generated. They are nat_rect, nat_rec, and nat_ind. Take a look at nat_rect. *) Print nat_rect. (* This is the induction principle for nat. Induction principles are automatically generated for every inductive datatype definition. We'll talk about these induction principles more later. *) (* Note: for next time you want to have some way to access the documentation for the Coq standard libraries. When I installed the beta I also installed the documentation. It has changed a good deal since Coq 8.1 and is not yet readily available on the Coq site. *) (* Since the induction principles are automatically generated they do not appear in the standard library documentation. *) (* Because natural numbers are so important, there are a lot of facts about the natural numbers made available in the core portion of the standard library. *) (* To look at the facts that are available, check out the Peano library. *) Print Peano. (* What we see is a mix of definitions and facts about definitions. We can pick out the definitions easily, they are prefixed by words like "Definition" and "Inductive". Facts about the definitions are prefixed by the word "Theorem". *) (* We can have relations on nats. A particularly important relation on nats is the <= relation. Note that it is defined inductively. *) Print le. (* Let's check the types of the inductive definitions we've looked at so far. *) Check nat. Check le. (* They're certainly different. Let try to extract le. I set the language back to Ocaml first. *) Extraction Language Ocaml. Extraction le. (* Note that when we extract le we get comments, not actual code. This is because its head type is Prop. nat gets extracted to code, because its head type is Set. *) (* There are other important ways in which items in Prop and items in Set are handled differently. We will discuss them later. *) (* <, >, and >= are defined in terms of <=. *) Print lt. Print gt. Print ge. (* A question to ponder: Why is <= chosen to be the fundamental relation on natural numbers? *) Print le. (* Note that le also has an inductive principle, just like nat. *) Print Peano. (* But unlike nat, it has just one. This is another consequence of the fact that le is in Prop and not in Set. *) Print le_ind. (* Now that we've learned about le we can make statement about natural numbers. *) (* Let's make a true statement. *) Definition O_le_2 := 0 <= 2. (* Observe that we can use the infix notation "<=" for le. A lot of the standard libraries define special notations for their inductive types. You can look at the standard library documentation to see how this is done. *) (* We can check the type of our definitions. *) Check O_le_2. (* Turns out it's a proposition. This is what we would expect since the type of le is nat -> nat -> Prop and we applied le to two nats. *) (* We can print our definition. *) Print O_le_2. (* We can construct definitions that don't typecheck, e.g., le true true. *) (* We can state facts that we know are false. *) Definition two_le_O := 2 <= 0. (* Coq will typecheck this false statement happily. In fact, it wouldn't have accepted our previous definition if it couldn't typecheck it. *) Check two_le_O. (* It's important to understand that what we have here is a statement of a proposition, not a proof of that proposition. If it were a proof of a proposition and Coq typechecked it we would be deeply saddened. We would also be deeply saddened if Coq failed to typecheck a completely valid statement of a proposition that just happens to be false. *) (* Note that this inductive definition of le inserts axioms into our environment just the way that the definition of nat did. *) (* Let's decide what those axioms are. At this point, I encourage everybody to stop and write the axioms down on a piece of paper. *) (* Exercise 2: Proving 23 <= 23. *) Goal 23 <= 23. Proof. (* At this point I wish to discourage you from using the automation that Coq provides. You will not learn anything by doing so. *) (* Let's take a second to write out what the proof should look like on paper. *) (* You might want to print the definition of le, so you can refer to it. *) (* We use exact to supply the proof. *) exact (le_n 23). Qed. (* We print the theorem again. *) Print Unnamed_thm0. (* Exercise 3: A little bit harder. *) Goal 23 <= 24. Proof. (* Again, let's stop and do this on paper first. *) exact (le_S 23 23 (le_n 23)). Qed. (* Exercise 4: Harder still. *) Goal 23 <= 25. Proof. (* Again, let's stop and do this on paper. We can reuse our paper proof from the previous exercise. *) (* We can copy and paste our program from the previous exercise to use in solving our new goal. *) exact (le_S 23 24 (le_S 23 23 (le_n 23))). Qed. (* Note that the standard library also defines operations on natural numbers. *) Print Peano. (* For example, pred is just a function that gets the predecessor of a natural number. *) Print pred. (* Note that it is a function with a very simple type, nat -> nat. This specification is no richer than the kind that ML provides. Any facts about pred that we need to use will have to be proven somewhere. *) (* To looks at the proofs about pred that have been loaded into the current environment, we can use the SearchAbout command. *) SearchAbout pred. (* There's just one, pred_Sn. *) (* We can construct expressions using functions. *) Definition pred_23 := pred 23. (* We can check the type of our definition. *) Check pred_23. (* We can also check it's value. *) Print pred_23. (* What we get is an expression in the COC, the application of the function pred to the natural number 23. We can also evaluate the expression in Coq's internal engine. *) Eval compute in pred_23. (* We get the answer we expected. *) (* Fun aside: what do we get when we set the target language to Scheme.? *) Extraction Language Scheme. (* When we extract nat we get nothing. Scheme says no to algebraic datatypes. *) Extraction nat. (* But when we extract pred we get a nice lisp function. *) Extraction pred.