1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/notation/relations/ringeq_3.ma".
16 include "ground/lib/stream.ma".
18 (* EXTENSIONAL EQUIVALENCE FOR STREAMS **************************************)
20 coinductive stream_eq (A): relation (stream A) ≝
21 | stream_eq_cons (a1) (a2) (t1) (t2):
22 a1 = a2 → stream_eq A t1 t2 → stream_eq A (a1⨮t1) (a2⨮t2)
26 "extensional equivalence (streams)"
27 'RingEq A t1 t2 = (stream_eq A t1 t2).
29 definition stream_eq_repl (A) (R:relation …) ≝
30 ∀t1,t2. t1 ≗{A} t2 → R t1 t2.
32 definition stream_eq_repl_back (A) (R:predicate …) ≝
33 ∀t1. R t1 → ∀t2. t1 ≗{A} t2 → R t2.
35 definition stream_eq_repl_fwd (A) (R:predicate …) ≝
36 ∀t1. R t1 → ∀t2. t2 ≗{A} t1 → R t2.
38 (* Basic constructions ******************************************************)
40 corec lemma stream_eq_refl (A:?):
41 reflexive … (stream_eq A).
42 * #a #t @stream_eq_cons //
45 corec lemma stream_eq_sym (A):
46 symmetric … (stream_eq A).
48 #a1 #a2 #t1 #t2 #Ha #Ht
49 @stream_eq_cons /2 width=1 by/
52 lemma stream_eq_repl_sym (A) (R):
53 stream_eq_repl_back A R → stream_eq_repl_fwd A R.
54 /3 width=3 by stream_eq_sym/ qed-.
56 (* Basic inversions *********************************************************)
58 (*** eq_inv_seq_aux *)
59 lemma stream_eq_inv_cons_bi (A):
61 ∀u1,u2,b1,b2. b1⨮u1 = t1 → b2⨮u2 = t2 →
64 #a1 #a2 #t1 #t2 #Ha #Ht #u1 #u2 #b1 #b2 #H1 #H2 destruct /2 width=1 by conj/