Require Import FSets. Require Import Program. (* Today, we'll extend our use of the program tactic to use what the authors call subset types. *) (* We'll expand on the approach from last time, reusing some of the same definitions. *) 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. Section A. (* We begin by defining our function f, which will always reach a fixpoint when recursively applied. *) Variable f : forall s, {s' | s' [<=] s }. (* We assume our 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. (* Last time we wrote a nice function using the program tactic that returned the fixed point of the application of f. 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. *) (* However, there's more that we can say about this function, k, based on the properties of the function f. *) Program Fixpoint k (s : t) { measure cardinal s} : {t | t [<=] s} := let z := f s in if Dep.equal z s then z else k z. Next Obligation. (* In the previous case, the various implicit Program tactics were able to handle everthing. Now, we have to help them along. But, it turns out that there are some handy mini-tactics to assist. *) (* What we need to do here is to get the type of the application of f to s. *) destruct_call f. simpl in *. auto. Defined. Next Obligation. destruct_call k. simpl in *. destruct_call f. simpl in *. fsetdec. Defined. (* We can get even more ambitious, and demonstrate that our function returns a fixed point. However, first we need to point out that f really is a function on sets. *) (* We admit this proof. It seems funny to have to make it, because we already know that f is a function. The problem is, we know that it is a function on our representation of sets, which is not at all the same as knowing it is a function on sets. Speaking algebraicly, we can say that A is the set of all possible representations of sets and that B is the sets of all possible sets. We have a mapping, m, from A to B which maps elements in A to the sets in B that they represent. It's a surjective mapping, but it is, in general, many-to-one. Two elements, a and a' in A, are equivalent, call this property (=), if m(a) [=] m(a') (where [=] is the set equality). The fact about f that we want to know is: if a (=) a', then f(a) (=) f (a'). If we scrutinize the implementation of the FSets interfaces, we'll find out that it's possible to prove these and equivalent facts about the functions that are part of the FSets interfaces based on their properties that are also defined in the interfaces. For example, it is possible to prove: forall s1 s1' s2 s2', s1 [=] s1' -> s2 [=] s2' -> add s1 s2 [=] add s1' s2' without a specific implementation of add. Once you've proved the necessary facts, you can use the Add Morphism instruction to add f to a special database for rewriting. That way, we can rewrite instances of the application of f to equal sets. Below, we just admit the necessary lemma about f. We can't prove it --- since we don't have any lemmas about f and we don't have it's implementation either. If we were trying to make this reusable, we'ld have to do a bit better. *) Lemma f_func : forall s s', s [=] s' -> proj1_sig (f s) [=] proj1_sig (f s'). Admitted. Hint Resolve f_func. (* We can now move ahead and prove our more ambitious fixed point. *) Program Fixpoint l (s : t) { measure cardinal s} : {t | t [<=] s /\ f t [=] t} := let z := f s in if Dep.equal z s then z else l z. Next Obligation. (* The hard part of the first obligation is to prove that the argument returned, i.e, f s, is really a fixed point. But with the help of the lemma we proved above it's handled automatically. *) intuition. Defined. Next Obligation. (* No different from what we did last time. *) destruct_call f. simpl in *. auto. Defined. Next Obligation. (* This looks complex, but can be simplified readily by destructing the calls. The proof is quite easy, as it is really just the application of recursive facts. *) destruct_call l. simpl in *. intuition. destruct_calls f. simpl in *. fsetdec. Defined. End A. (* We inline proj1_sig so that the extraction mechanism will remove it. *) Extraction Inline proj1_sig. (* Our two extracted functions are identical. *) Recursive Extraction k. Recursive Extraction l. End AFixpoint.