blob: 4114987d36e353b66e22801a1548bafce31ff891 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* 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.
intros s.
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.
|
