The axiom stating that bisimilarity implies Leibniz equality for coinductive datatypes like streams is consistent with Coq's logic. Here's the reasoning:

1. Bisimulation and Coinductive Types

Coinductive types, such as Stream A, represent infinite structures (e.g., infinite sequences) where elements are defined by their observable behavior. Bisimulation is the standard equivalence relation ...

Short answer: Yes—adding “bisimilarity implies Leibniz equality” for (non-indexed, strictly positive) coinductive datatypes such as streams is consistent with Coq’s logic. It is not provable in intensional Coq in general, but it holds in standard set-theoretic models and therefore is consistent relative to Coq.

Why it is reasonable

• For a coinductive datatype given as the greatest fixed point νF...

Short answer
Yes, nothing contradictory is known to follow from the axiom

Stream_bisim A xs ys  ->  xs = ys

(or the analogous axiom for any other guarded co-inductive type).
In the usual set–theoretic model of Coq the axiom is actually true, so adding it to Coq can only be inconsistent if Coq itself already is.

Why the axiom is true in a classical model

1. How streams are interprete...

Is Extensionality for Coinductive Datatypes Consistent with Coq's Logic?

Yes, the axiom Stream_bisim_eq stating that bisimilar streams are Leibniz-equal is consistent with Coq's logic.

Your intuition comparing this to functional extensionality is correct. Just as functional extensionality states that functions with the same input-output behavior are equal, your axiom states that streams with...

Yes – adding an axiom that identifies two coinductive values that are bisimilar with Leibniz equality does not lead to inconsistency. Just as with the more familiar “functional extensionality” axiom, the principle is independent of Coq’s core logic (it cannot be proved inside Coq), but it is consistent with it: there is a standard model of the Calculus of Inductive Constructions in which th...

The example given is for streams:

CoInductive Stream (A : Type) : Type := | Cons : A -> Stream A -> Stream A.

CoInductive Stream_bisim (A : Type) : Stream A -> Stream A -> Prop := | Stream_bisim_Cons : forall (x...

Excellent question. This gets to the heart of the difference between intensional and extensional type theory.

Short Answer

Yes, this axiom is consistent with Coq's logic.

Your intuition is correct. The principle you're describing is a form of coinductive extensionality. Just like functional extensionality, it is not provable in Coq's standard logic (the Calculus of Inductive Constru...

You will be pleased to hear that nothing “magical” happens here – adding the axiom

Axiom Stream_bisim_eq :
  ∀ A (s t : Stream A), Stream_bisim A s t → s = t.

or, more generally, for any coinductive type “bisimilar ⇒ Leibniz‐equal,” does not introduce an inconsistency into Coq. In fact it is no stronger than ordinary functional extensionality, and it even follows from it. Here ...

This is a great question about the consistency of adding extensionality principles for coinductive types in Coq.

Short answer: Yes, adding extensionality axioms for coinductive datatypes (like your Stream_bisim_eq) is generally considered consistent with Coq's logic, though there are some important caveats.

Why it's believed to be consistent

1. Observational equivalence: As you cor...