Structural equality is an inductive notion, one that only applies to data that are constructed inductively. For streams, the corresponding coinductive notion is known as “bisimilarity”, which translates to “if it is constructed the same, it is the same”:
CoInductive bisimilar : forall V : Type, (V -> V -> bool) -> stream V -> stream V -> Prop :=
Bisimilar :
forall (V : Type)
(eqb_V : V -> V -> bool)
(v1 v2 : V),
eqb_V v1 v2 = true ->
forall v1s v2s : stream V,
bisimilar V eqb_V v1s v2s ->
bisimilar V eqb_V (SCons V v1 v1s) (SCons V v2 v2s).
Prove that bisimilar is an equivalence relation, i.e., that it is reflexive, symmetric, and transitive.
Reflexivity and symmetry are proved in the resource file.
By analogy with lists, the following function concatenates two streams:
CoFixpoint stream_append (V : Type) (v1s v2s : stream V) :=
match v1s with
| Cons _ v1 v1s' =>
Cons V v1 (stream_append V v1s' v2s)
end.
In another life, we argued that this function is equivalent to the following simpler one:
Definition stream_append_simpler (V : Type) (v1s v2s : stream V) :=
v1s.
We are now in position to prove this equivalence:
Proposition about_stream_append :
forall (V : Type)
(eq_V : V -> V -> Prop),
(forall v : V,
eqb_V v v = true) ->
forall v1s v2s : stream V,
bisimilar V eqb_V (stream_append V v1s v2s) (stream_append_simpler V v1s v2s).
Prove this proposition.
The happy drunkard, walking by: Hi, friends.
Harald: Hello to you too! And welcome back. Long time no see, and all that.
The happy drunkard: As you can see, I am still nursing my bottle of beer.
Alfrothul: And it is still pleasantly cool and never gets empty?
The happy drunkard, happily: As ever.
Harald: Talking about that, where are the two others? Did you, huh, drink them already?
The happy drunkard, modestly: No, no. I gave them to a good friend who needed them more than me. Oh, hi, Loki, I didn’t see you were there too. How are things?
Loki: Busy as ever, buddy. Busy as ever.
Created [10 Apr 2025]