Require Import FSets. Require Import Program. (* Let's consider what's involved in doing recursion on sets. We'll examine this issue by writing a generic recursive function on sets. *) Module AFixpoint (Import M : S). Module Import P := Properties M. Module Import Dec := P.Dec. (* We make a dependently typed version of our module, so we can use function like equal. *) Module Dep := FSetBridge.DepOfNodep (M). Print Dep. Print Dep.equal. Print equal. (* Consider the following simple, syntactically correct function that recursively applies another function. *) (* We build it within a section, so we can abstract it. *) Section A. (* Variable f : t -> t. Fixpoint g s := let z := f s in if Dep.equal z s then z else g z. *) (* This is syntactically correct, and would extract to a correct, but potentially non-terminating OCaml program. We don't actually want a non-terminating program, though. Most likely we expect that f always returns a subset of its first argument. In Coq, of course, we can enrich the type with that fact. *) Variable f : forall s, {s' | s' [<=] s }. (* Well, now we know that g will always terminate. But our former function is still unacceptable, because it does not obey the syntactic restrictions that ensure that we terminate. These can't possibly work, because we don't have any access to the actual inductive type of the set. The trick: do induction on something else entirely, for which we do have the type available. The obvious choice: nats. *) (* First, we assume a useful lemma which we will prove later. *) Lemma subset_neq_cardinal_lt : forall s s', s [<=] s' -> ~ s [=] s' -> cardinal s < cardinal s'. Admitted. Hint Resolve subset_neq_cardinal_lt. Definition g : t -> t. intros s. (* Here we write a fixpoint on nats, but there are a few extra parameters. *) refine ((fix F (n : nat) (s : t) { struct n} : cardinal s <= n -> t := match n return cardinal s <= n -> t with | 0 => fun H => let (z, p) := f s in if Dep.equal z s then z else _ | S n => fun H => let (z, p) := f s in if Dep.equal z s then z else F n z _ end) (cardinal s) s (le_n (cardinal s))); clear F. assert (Empty s0); intuition. (* We try some forward reasoning. *) assert (cardinal z < cardinal s0) by intuition. intuition. Defined. (* You can even try closing the section and extracting a meaningful program. Note that the extracted program is not quite what we want; it includes some stuff about nats that is really irrelevant and only there to prove termination. We would like some other way, that throws all the stuff about cardinality away. It turns out that there is a whole library, quite recently developed, called Program, which is here to help us out. Note: We are now introducing yet another way to develop proofs in Coq. This approach is dependently typed, like the Chlipala approach, but in a more restricted way. That is, we are restricted to the use of the sig type, called subset types in much of the literature on this approach. The idea is that we write our program just as if it were an ML program, and the Program library will synthesize our proof obligations. This is due to Matthieu Sozeau *) (* To let Coq know what we are doing, we use a special new syntax. We take our original program, g, as our inspiration. *) (* We use a new annotation we've never used before. In regular Fixpoints we can only use the struct annotation, which indicates the argument on which we are doing structural recursion. In Program Fixpoints we can use measure. The first argument to measure has type X -> Y. In order for the program to typecheck X must be the type of the second argument to measure. Here we choose the first argument to be cardinal and the second to be our set argument. Note: Although Y is not restricted, your programs will be impossible to complete if Y is not nat. Happily, nat is the usual case. *) Program Fixpoint k (s : t) { measure cardinal s} : t := let (z, p) := f s in if Dep.equal z s then z else k z. (* The program generated an obligation like the one we had to solve for g, but then it solved it. It used the hint that we already have in the environment. *) (* If we extract this program, we'll see that it is clear of all mention of nats. *) End A. End AFixpoint. (* Exercise: Implement the algorithm for binary search. You do not need to prove that it is correct. You will have to prove that it terminates, of course. But you can cheat, by using lemmas that you don't prove, but just admit, as we did above. Consult Chapter 21 of the Reference Manual for the commands used to inspect proof obligations. Matthieu Sozeau's implementation of the Quicksort algorithm (http://mattam.org/repos/coq/misc/sort/) is a nice small scale example of what an entire implementation of a sorting algorithm using Program might look like. *) Module BinarySearch (Import E : OrderedType). Module Import F := OrderedTypeFacts E. Require Import Div2. Require Import Peano_dec. Require Import TheoryList. (* Some possibly useful functions. *) Print div2. Check eq_nat_dec. Print length. Print lt_dec. Print firstn. Check nth_error. Print Isnil_dec. (* Your solution should have type list t -> t -> option t, where t is the type of the OrderedType. *)