File: bug_1643.v

package info (click to toggle)
coq 9.1.0%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 35,964 kB
  • sloc: ml: 239,908; sh: 4,355; python: 2,985; ansic: 2,644; makefile: 874; lisp: 171; javascript: 63; xml: 24; sed: 2
file content (20 lines) | stat: -rw-r--r-- 475 bytes parent folder | download | duplicates (13) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
 
(* Check some aspects of that the algorithm used to possibly reuse a
   global name in the recursive calls (coinductive case) *)

CoInductive Str : Set := Cons (h:nat) (t:Str).

Definition decomp_func (s:Str) :=
  match s with
    | Cons h t => Cons h t
  end.

Theorem decomp s: s = decomp_func s.
Proof.
  case s; simpl; reflexivity.
Qed.

Definition zeros := (cofix z : Str := Cons 0 z).
Lemma zeros_rw : zeros = Cons 0 zeros.
  rewrite (decomp zeros).
  simpl.
Admitted.