Mercurial > cpdt > repo

comparison src/Coinductive.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents 2c88fc1dbe33
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
75 75
76 Eval simpl in approx zeroes 10. 76 Eval simpl in approx zeroes 10.
77 (** %\vspace{-.15in}% [[ 77 (** %\vspace{-.15in}% [[
78 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil 78 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
79 : list nat 79 : list nat
80 ]] *) 80 ]]
81 *)
81 82
82 Eval simpl in approx trues 10. 83 Eval simpl in approx trues 10.
83 (** %\vspace{-.15in}% [[ 84 (** %\vspace{-.15in}% [[
84 = true 85 = true
85 :: false 86 :: false
322 Theorem ones_eq' : stream_eq ones ones'. 323 Theorem ones_eq' : stream_eq ones ones'.
323 cofix; crush. 324 cofix; crush.
324 (** [[ 325 (** [[
325 Guarded. 326 Guarded.
326 327
327 ]] *) 328 ]]
329 *)
328 Abort. 330 Abort.
329 (* end thide *) 331 (* end thide *)
330 332
331 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with %``%#"#hiding#"#%''% the co-inductive hypothesis. *) 333 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with %``%#"#hiding#"#%''% the co-inductive hypothesis. *)
332 334