Mercurial > cpdt > repo

comparison src/Coinductive.v @ 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents ed829eaa91b2
children
comparison
equal deleted inserted replaced
567:ec0ce5129fc4 568:81d63d9c1cc5
251 We can try restating the theorem with [stream_eq]. *) 251 We can try restating the theorem with [stream_eq]. *)
252 252
253 Theorem ones_eq : stream_eq ones ones'. 253 Theorem ones_eq : stream_eq ones ones'.
254 (** Coq does not support tactical co-inductive proofs as well as it supports tactical inductive proofs. The usual starting point is the [cofix] tactic, which asks to structure this proof as a co-fixpoint. *) 254 (** Coq does not support tactical co-inductive proofs as well as it supports tactical inductive proofs. The usual starting point is the [cofix] tactic, which asks to structure this proof as a co-fixpoint. *)
255 255
256 cofix. 256 cofix ones_eq.
257 (** [[ 257 (** [[
258 ones_eq : stream_eq ones ones' 258 ones_eq : stream_eq ones ones'
259 ============================ 259 ============================
260 stream_eq ones ones' 260 stream_eq ones ones'
261 261
321 Qed. 321 Qed.
322 322
323 (** But, miraculously, this theorem turns out to be just what we needed. *) 323 (** But, miraculously, this theorem turns out to be just what we needed. *)
324 324
325 Theorem ones_eq : stream_eq ones ones'. 325 Theorem ones_eq : stream_eq ones ones'.
326 cofix. 326 cofix ones_eq.
327 327
328 (** We can use the theorem to rewrite the two streams. *) 328 (** We can use the theorem to rewrite the two streams. *)
329 329
330 rewrite (frob_eq ones). 330 rewrite (frob_eq ones).
331 rewrite (frob_eq ones'). 331 rewrite (frob_eq ones').
377 If [cofix]es reduced haphazardly, it would be easy to run into infinite loops in evaluation, since we are, after all, building infinite objects. 377 If [cofix]es reduced haphazardly, it would be easy to run into infinite loops in evaluation, since we are, after all, building infinite objects.
378 378
379 One common source of difficulty with co-inductive proofs is bad interaction with standard Coq automation machinery. If we try to prove [ones_eq'] with automation, like we have in previous inductive proofs, we get an invalid proof. *) 379 One common source of difficulty with co-inductive proofs is bad interaction with standard Coq automation machinery. If we try to prove [ones_eq'] with automation, like we have in previous inductive proofs, we get an invalid proof. *)
380 380
381 Theorem ones_eq' : stream_eq ones ones'. 381 Theorem ones_eq' : stream_eq ones ones'.
382 cofix; crush. 382 cofix one_eq'; crush.
383 (** %\vspace{-.25in}%[[ 383 (** %\vspace{-.25in}%[[
384 Guarded. 384 Guarded.
385 ]] 385 ]]
386 %\vspace{-.25in}% 386 %\vspace{-.25in}%
387 *) 387 *)
416 (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %``%#<i>#hereditary#</i>#%''% in the sense that an [R] stream pair passes on "[R]-ness" to its tails. An established technical term for such a relation is%\index{bisimulation}% _bisimulation_. *) 416 (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %``%#<i>#hereditary#</i>#%''% in the sense that an [R] stream pair passes on "[R]-ness" to its tails. An established technical term for such a relation is%\index{bisimulation}% _bisimulation_. *)
417 417
418 (** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal. The reader may wish to step through the proof script to see what is going on. *) 418 (** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal. The reader may wish to step through the proof script to see what is going on. *)
419 419
420 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2. 420 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2.
421 cofix; destruct s1; destruct s2; intro. 421 cofix stream_eq_coind; destruct s1; destruct s2; intro.
422 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq. 422 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq.
423 constructor. 423 constructor.
424 apply stream_eq_coind. 424 apply stream_eq_coind.
425 apply (Cons_case_tl H). 425 apply (Cons_case_tl H).
426 Qed. 426 Qed.
613 \/ exists vs2, evalExp vs1 e <> 0 /\ R vs1 c vs2 /\ R vs2 (While e c) vs3. 613 \/ exists vs2, evalExp vs1 e <> 0 /\ R vs1 c vs2 /\ R vs2 (While e c) vs3.
614 614
615 (** The proof is routine. We make use of a form of %\index{tactics!destruct}%[destruct] that takes an%\index{intro pattern}% _intro pattern_ in an [as] clause. These patterns control how deeply we break apart the components of an inductive value, and we refer the reader to the Coq manual for more details. *) 615 (** The proof is routine. We make use of a form of %\index{tactics!destruct}%[destruct] that takes an%\index{intro pattern}% _intro pattern_ in an [as] clause. These patterns control how deeply we break apart the components of an inductive value, and we refer the reader to the Coq manual for more details. *)
616 616
617 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2. 617 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2.
618 cofix; intros; destruct c. 618 cofix evalCmd_coind; intros; destruct c.
619 rewrite (AssignCase H); constructor. 619 rewrite (AssignCase H); constructor.
620 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. 620 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto.
621 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto. 621 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto.
622 Qed. 622 Qed.
623 End evalCmd_coind. 623 End evalCmd_coind.