File: bug_1643.v

package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; xml: 24; sed: 2
file content (20 lines) | stat: -rw-r--r-- 475 bytes parent folder | download | duplicates (12) 
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.