aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/coindprim.v
blob: 4e0b7bf5c6d7d6697b5ba3564f8f37c2c672761a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
Set Primitive Projections.

CoInductive stream A := { hd : A; tl : stream A }.

CoFixpoint ticks : stream unit :=
  {| hd := tt; tl := ticks |}.

Arguments hd [ A ] s.
Arguments tl [ A ] s.

CoInductive bisim {A} : stream A -> stream A -> Prop :=
  | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'.

Lemma bisim_refl {A} (s : stream A) : bisim s s.
Proof.
  revert s.
  cofix aux. intros. constructor. reflexivity. apply aux.
Defined.

Lemma constr : forall (A : Type) (s : stream A),
    bisim s (Build_stream _ s.(hd) s.(tl)).
Proof.
  intros. constructor. reflexivity. simpl. apply bisim_refl.
Defined.

Lemma constr' : forall (A : Type) (s : stream A),
  s = Build_stream _ s.(hd) s.(tl).
Proof.
  intros. 
  Fail destruct s. 
Abort.

Eval compute in constr _ ticks.

Notation convertible x y := (eq_refl x : x = y).

Fail Check convertible ticks {| hd := hd ticks; tl := tl ticks |}.

CoInductive U := inU
 { outU : U }.

CoFixpoint u : U :=
  inU u.

CoFixpoint force (u : U) : U :=
  inU (outU u).

Lemma eq (x : U) : x = force x.
Proof.
  Fail destruct x.
Abort.
  (* Impossible *)