(* Today we'll define a simple lazy structure, called a sequence. *) (* We'll rely on the definition of list, for inspiration. *) Require Import List. Print list. Require Import MoreSpecif. Open Scope specif_scope. (* We'll use a Section, to make things less verbose. *) Section Seq. (* We'll also use this directive. When we're done defining our infinite datatype, all arguments that can be inferred from subsequent arguments will be implicit. *) Set Implicit Arguments. (* Our lazy structure will be parameterized on the type of its contents. *) Variable A : Type. (* We could define our seq using an CoInductive datatype that is isomorphic to the list datatype. *) CoInductive seq : Type := | Nil : seq | Cons : A -> seq -> seq . (* Now it's lazy. Implicitly, the second argument to Cons is suspended. *) (* Note that our CoInductive definition did not get any induction principles. That would be because our coinductive definition is not well-founded, and so induction does not make sense. *) (* We can get the head and the tail very easily, since there's no recursion required. *) (* We follow the approach for list exactly. *) Print List.hd. Definition start (default : A) (s : seq) := match s with | Nil => default | Cons a s => a end. Print List.tail. Definition rest (s : seq) := match s with | Nil => Nil | Cons a s => s end. (* We can get the first n elements in the sequence using a fixpoint, since our function is structurally recursive on its first argument. *) Fixpoint firstn (n : nat) (s : seq) := match n with | 0 => Nil | S n => match s with | Cons a s => Cons a (firstn n s) | Nil => Nil end end. (* We can get the tail after the nth element of the seq as well. *) Fixpoint fromn (n : nat) (s : seq) : seq := match n with | 0 => s | S n => match s with | Cons a s => fromn n s | Nil => Nil end end. (* We can write a function that operates on every element of our seq. Unlike fromn, it must be a cofixpoint, because it has no other guarantor of termination. Note that the recursive call is inside a constructor application. *) CoFixpoint map (f : A -> A) (s : seq) := match s with | Nil => Nil | Cons a s => Cons (f a) (map f s) end. (* We can not write a simple filter function, however, because we cannot be certain of termination. *) (* CoFixpoint filter (f : A -> bool) (s : seq) := match s with | Nil => Nil | Cons a s => if (f a) then Cons a (filter s) else filter s end. *) (* The problem is that the second application of filter is not implicitly suspended. Consider the expression filter (fun a => false). Surrounding this by a match statement would trigger an evaluation of the cofix which might never terminate. Among other things, this means that we can not write an Eratosthenes' sieve in Coq. *) (* We can write an function that munges over our seq, skipping n elements. Thus, skip n 0 will return the list unchanged. skipn 1 will return every other element. This works, because we are always guaranteed to return a new seq. *) CoFixpoint skip_n (s : seq) (n : nat) := match s with | Nil => Nil | Cons a s => Cons a (skip_n (fromn n s) n) end. (* We can write an inductive predicate for finiteness. *) Inductive Finite : seq -> Prop := | FiniteNil : Finite Nil | FiniteCons : forall a s, Finite s -> Finite (Cons a s) . (* We can write a inductive predicate for infiniteness. If we make it inductive, then any proof will be finite. This seams bad, cause we'll be making proofs about infinite things. So, we choose to make it a co-inductive definition in hopes that this will help. *) CoInductive Infinite : seq -> Prop := | Inf : forall a s, Infinite s -> Infinite (Cons a s) . (* In the world of nat's, we were able to prove, forall n, { even n } + { odd n }. How about proving, forall s, { Finite s } + { Infinite s }. That's something we can not expect to do. *) (* It's surprising how many relationships we can prove between Finite and Infinite. *) (* Can we prove that finite implies not infinite? *) Lemma fin_not_inf : forall s, Finite s -> ~ Infinite s. refine (fix F s (f : Finite s) := match f in Finite s0 return ~ Infinite s0 with | FiniteNil => _ | FiniteCons a s f => let z := F s f in _ end); red; intros H; inversion H; subst; contradiction. Qed. (* What about not finite implies infinite. That's a good match. We can do coinduction on the structure of s to build a CoInductive proof of infiniteness. *) Lemma not_fin_inf : forall s, ~ Finite s -> Infinite s. Hint Constructors Finite. refine (cofix C (s : seq) : ~ Finite s -> Infinite s := match s return ~ Finite s -> Infinite s with | Nil => fun H => ! | Cons a s => fun H => Inf _ _ end); auto. Qed. (* What about infinite implies not finite. Impossible to prove using induction or coinduction, but easy to prove using our previous proofs. *) Lemma inf_not_fin: forall s, Infinite s -> not (Finite s). Proof. intros. contradict H. apply fin_not_inf. auto. Qed. (* What about not infinite implies finite. Goal forall s, ~ Infinite s -> Finite s. Alas, not possible. *) (* It's really hard to decide the length of co-inductive datatype. *) (* Even the length of a Finite seq is a problem. Definition length (s : seq) (H : Finite s) : nat. We can't do induction on the sequence, because it's coinductive. We can't do induction on the proof that it's finite, because we want to return a nat. *) (* We can fix this, by putting Finite in Set rather than Prop. If we do that, we need to do the same for Infinite. This is a common bind. *) (* Equality is also a problem. Remember the definition of eq. *) Print eq. (* We can also write an apparently pointless identity function, which will later turn out to be very valuable. *) Definition destruct_seq (s : seq) : seq := match s with | Nil => Nil | Cons a s => Cons a s end. (* We can show that it is an identity. *) Lemma destruct_seq_id : forall s, s = destruct_seq s. destruct s; auto. Qed. (* We can prove that equality is reflexive, symmetric, transitive on coinductive as on inductive types. *) Goal forall (s : seq), s = s. apply refl_equal. Qed. (* This was possible because we were not doing coinduction. But, what if we have to take two arbitrary sequences and inspect their contents to decide equality. We'll need to use coinduction, yet eq is an inductive type. *) (* So, we must define a co-inductive version of equality which can be used for these specific cases. *) CoInductive bisimilar : seq -> seq -> Prop := | BNil : bisimilar Nil Nil | BCons : forall a a' s s', a = a' -> bisimilar s s' -> bisimilar (Cons a s) (Cons a' s') . (* Can we write a decision procedure for bisimilarity? forall s s', {s [=] s'} + {~ (s [=] s')}. We have similar problems as with our other decision procedures. *) (* Can we prove that equality implies bisimilarity? Yes! *) Lemma eq_bis : forall s s', s = s' -> bisimilar s s'. intros. subst. Hint Constructors bisimilar. revert s'. refine (cofix F s' := match s' return bisimilar s' s' with | Nil => _ | Cons a s => BCons (refl_equal a) (F s) end); clear F; auto. Qed. End Seq. (* We'll use a notation for bisimilar that looks like =, but is different. *) Infix "[=]" := bisimilar (at level 70, no associativity). (* Note that now that we've closed the section, all our functions and definitions contain that A. Note that A is implicit, which means we won't need to supply it. *) Print seq. Print start. Print rest. Print firstn. (* We can write CoFixpoints to give us infinite structures. The reason why CoInductive definition are called coinductive is that we can write recursively defined functions where the codomain is the coinductive datatype. With Inductive definitions, we write recursively defined functions where the domain is the inductive datatype. *) (* Here we can write a recursively defined function that gives us an infinite stream of numbers starting from x. *) (* Note that there is no explicit suspension of computation. It is implicit where the recursive call occurs. Note that we do not supply the nat to Cons. *) CoFixpoint count x := Cons x (count (S x)). (* If we set printing to all, we would see that it's really still there. *) Print count. (* We must not have a non-terminating function. Here we see that the application of count to 3 will always remain unevaluated when it occurs at the top level. The cofix is expanded, but not applied. *) Eval compute in count 3. (* We can force one expansion by enriching the context in which it is evaluated. The cofix is applied once to 3 because the match in start triggered one step in the expansion. *) Eval compute in start 0 (count 3). (* rest has one match, so it triggers just one expansion, just like start. *) Eval compute in rest (count 3). (* We can do the usual multiple expansion by forcing multiple matches. *) Eval compute in start 0 (rest (count 3)). (* We can use first n to expand the seq to a finite seq of any length. *) Eval compute in fromn 32 (count 3). (* We can write a function that increments our seq of nats. *) Definition inc := fun s => map S s. (* We can grab a chunk of it. *) Eval compute in firstn 14 (inc (count 3)). (* Now, we show that rest (count 3) [=] count 4. Here we can use the fact that equality implies bisimilarity. *) Goal rest (count 3) [=] count 4. Proof. simpl. apply eq_bis; auto. Qed. (* Now, we try to show that inc (count 3) [=] count 4. This is surprisingly tricky. We can not massage this into a form where two sides are actually equal, because inc is a cofixpoint. We must use recursion. So, we must generalize. *) Lemma eq_proof : forall n, inc (count n) [=] count (S n). Proof. cofix. intro n. rewrite (destruct_seq_id (inc (count n))). rewrite (destruct_seq_id (count (S n))). simpl. apply BCons; intuition. apply eq_proof. Qed. Print eq_proof. (* Exercise: Use the structures from the previous exercise to show that rest (invert (false_true)) [=] false_true. Showing that invert (false_true) [=] true_false is just as good. *)