The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

> You can't actually achieve this for infinite values like the above, so to 
> usefully prove their equality, you'd have to add an extensionality axiom like 
> you suggest. But in principle, bisimilarity means that you could prove two 
> values intensionally equal through evaluation (the equality just isn't 
> decidable).

You are right indeed, mea culpa for that. Bisimilarity allows 
coinductive reasoning which are more powerful than reasoning with 
intentional equality (which only allows to look at a finite prefix, 
although of arbitrary length).

Therefore you will only have properties such as the following (still 
contestable, in my opinion):

CoInductive stream (A:Type) : Type :=
 | cons : A -> stream A -> stream A
.

Definition hd (A:Type) (s:stream A) :=
 match s with
 | cons a _ => a
 end
.
Implicit Arguments hd [ A ].

Definition tl (A:Type) (s:stream A) :=
 match s with
 | cons _ t => t
 end
.
Implicit Arguments tl [ A ].

CoInductive bisim (A:Type) (s1 s2:stream A) :Prop :=
 | mk_bisim : hd s1 = hd s2 -> bisim _ (tl s1) (tl s2) -> bisim _ s1 s2
.

Fixpoint tln (A:Type) (s:stream A) (n:nat) {struct n} : stream A :=
 match n with
 | 0 => s
 | S n' => tln _ (tl s) n'
 end
.

Goal forall A n (s1 s2:stream A), tln _ s1 n = tln _ s2 n -> bisim _ s1 s2 -> 
s1 = s2.
 intro A. induction n.
   trivial.

   intros [ h1 s1 ] [ h2 s2 ] t [ h b ].
   simpl in *. rewrite h. 
   rewrite (IHn s1 s2); trivial.
Qed.