+(******** How to compare coinductive types *********)
+
+(* Inhabitants of inductive types are compared using Leibniz's equality that,
+ on closed terms, coincides with convertibility. Two closed inductive terms
+ are equal iff they reduce to the same normal form.
+
+ Because of the lazy evaluation of coinductively defined terms, conversion
+ does not behave as expected on inhabitants of coinductive types. For example,
+ the following two definitions, both in normal form, produce the same
+ streamseq 0,1,0,1,… but are not equal because the normal forms are
+ syntactically different. *)
+
+let corec zero_one_streamseq1: streamseq ℕ ≝
+ sscons … 0 (sscons … 1 zero_one_streamseq1).
+
+let corec one_zero_streamseq: streamseq ℕ ≝
+ sscons … 1 (sscons … 0 one_zero_streamseq).
+
+definition zero_one_streamseq2: streamseq ℕ ≝ sscons … 0 one_zero_streamseq.
+
+(* In place of Leibniz equality, the right notion to compare coinductive terms
+ is bisimulation. Two terms t1,t2 are bisimilar if every observation on t1 can
+ be performed on t2 as well, and the observed subterms are co-recursively
+ bisimilar. In practice two coinductive terms are bisimilar if they are the same
+ constructor applied to bisimilar coinductive subterms.
+
+ We define bisimilarity for streamseqs using a coinductive predicate. *)
+coinductive ss_bisimilar (A: Type[0]) : streamseq A → streamseq A → Prop ≝
+ sscons_bisim:
+ ∀x,tl1,tl2.
+ ss_bisimilar … tl1 tl2 →
+ ss_bisimilar … (sscons … x tl1) (sscons … x tl2).
+
+(* The two streams above can be proved to be bisimilar. By using the
+ eta_streamseq trick twice, we expand both definitions once so to obtain the
+ new proof obligation 0,1,zero_one_streamseq1 = 0,1,zero_one_streamseq2.
+ Then we apply twice the sscons_bisim constructor to consume the leading 0 and 1,
+ finding again the original goal. Finally we conclude with the coinductive
+ hypothesis. The proof is productive because, after the two rewriting, it
+ reduces to two applications of the sscons_bisim constructor, immediately
+ followed by the recursive call. *)
+let corec zero_one_streamseq_eq: ss_bisimilar … zero_one_streamseq1 zero_one_streamseq2 ≝
+ ?.
+ <(eta_streamseq … zero_one_streamseq1) normalize
+ <(eta_streamseq … one_zero_streamseq) normalize
+ % % @zero_one_streamseq_eq
+qed.
+
+(* We can finally turn streamseqs into a setoid and lift every operation on
+ streamseqs to morphisms. We first prove reflexivity, symmetry and transitivity
+ of bisimulation because each proof must be given using let corec. *)
+let corec reflexive_ss_bisimilar (A: Type[0]): reflexive … (ss_bisimilar A) ≝ ?.
+ * #hd #tl % @reflexive_ss_bisimilar
+qed.
+
+let corec symmetric_ss_bisimilar (A: Type[0]): symmetric … (ss_bisimilar A) ≝ ?.
+ * #hd1 #tl1 * #hd2 #tl2 * #hd #tl1' #tl2' #H % @symmetric_ss_bisimilar @H
+qed.
+
+(* In the proof of transitivity we face a technical problem. After inverting one
+ of the bisimilarity hypothesis we are left with an equation of the form
+ sscons … hd1 tl1 = sscons … hd2 tl2 and we need to extract hd1 = hd2 and
+ tl1 = tl2 to conclude the proof. The destruct tactic does exactly this, but
+ it produces a proof term that is not recognized to be productive by Matita.
+ The trick is to cut the two equalities and to use destruct to prove them.
+ In this way the destruct tactic is used only in a side proof inside which there
+ is no recursive call, and the whole proof term is recognized to be productive. *)
+let corec transitive_ss_bisimilar (A: Type[0]): transitive … (ss_bisimilar A) ≝ ?.
+ * #hd1 #tl1 * #hd2 #tl2 * #hd3 #tl3
+ * #hd #tl1' #tl2' #H1
+ #H inversion H #hd' #tl1'' #tl2'' -H #H #EQ1 #_
+ cut (hd=hd' ∧ tl1''=tl2') [ destruct /2/ ] ** #EQ % @transitive_ss_bisimilar //
+qed.
+
+definition STREAMSEQ: Type[0] → setoid ≝
+ λA.
+ mk_setoid (streamseq A)
+ (mk_equivalence_relation … (ss_bisimilar A) …).
+ //
+qed.
+
+unification hint 0 ≔ A:Type[0];
+ X ≟ STREAMSEQ A
+(* ---------------------------------------- *) ⊢
+ streamseq A ≡ carrier X.
+
+(* As an example, we lift streamseq_nth to a morphism. *)
+definition STREAMSEQ_NTH: ∀A: Type[0]. STREAMSEQ A ⤞ (LEIBNIZ ℕ) ⤞ (LEIBNIZ A) ≝
+ λA. mk_bin_morphism ??? (streamseq_nth A) ….
+ #x1 #x2 #n1 #n2 #bisim * lapply bisim -bisim lapply x2 -x2 lapply x1 -x1 -n2 elim n1
+ [ #x1 #x2 #H inversion H //
+ | #m #IH #x1 #x2 #H inversion H #hd #tl1 #tl2 #bisim #EQ1 #EQ2 destruct @IH //]
+qed.
+
+(* Working with setoids introduce technical complications that one would rather
+ avoid. The alternative encoding of streams via sequences doen not solve the
+ issue. Sequences are functions and, to capture the mathematical meaning of
+ equality for sequences, functions need to be compare using functional
+ extensionality. Two functions are extensionally equal when they are pointiwse
+ equal, i.e. they map equal inputs to the same outputs. Intensional equality of
+ functions, instead, just compares the two codes.
+
+ For example, the next two enumerations 0,1,2,… are extensionally, but not
+ intensionally equal. *)
+definition enum_N1: seq ℕ ≝ λi. i.
+definition enum_N2: seq ℕ ≝ λi. i+0.
+
+(* Functional extensionality is defined in the standard library of Matita as
+ follows. *)
+definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
+λA,B.λf,g.∀a.f a = g a.
+
+(* The proof that the two sequences above are extensionally equal is trivial. *)
+lemma enum_N_equal: exteqF … enum_N1 enum_N2.
+ normalize //
+qed.
+
+(* Like for bisimulation, to work sistematically with functional extensionality
+ we need to turn the type of sequences into a setoid. The two alternatives are
+ actually equivalent with respect to this issue. *)
+