--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/ringeq_3.ma".
+include "ground_2/lib/list.ma".
+
+(* EXTENSIONAL EQUIVALENCE OF LISTS *****************************************)
+
+rec definition eq_list A (l1,l2:list A) on l1 ≝
+match l1 with
+[ nil ⇒
+ match l2 with
+ [ nil ⇒ ⊤
+ | cons _ _ ⇒ ⊥
+ ]
+| cons a1 l1 ⇒
+ match l2 with
+ [ nil ⇒ ⊥
+ | cons a2 l2 ⇒ a1 = a2 ∧ eq_list A l1 l2
+ ]
+].
+
+interpretation "extensional equivalence (list)"
+ 'RingEq A l1 l2 = (eq_list A l1 l2).
+
+(* Basic properties *********************************************************)
+
+lemma eq_list_refl (A): reflexive … (eq_list A).
+#A #l elim l -l /2 width=1 by conj/
+qed.
+
+(* Main properties **********************************************************)
+
+theorem eq_eq_list (A,l1,l2): l1 = l2 → l1 ≗{A} l2.
+// qed.
+
+(* Main inversion propertiess ***********************************************)
+
+theorem eq_list_inv_eq (A,l1,l2): l1 ≗{A} l2 → l1 = l2.
+#A #l1 elim l1 -l1 [| #a1 #l1 #IH ] *
+[ //
+| #a2 #l2 #H elim H
+| #H elim H
+| #a2 #l2 * #Ha #Hl /3 width=1 by eq_f2/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/oplusright_3.ma".
+include "ground_2/lib/relations.ma".
+
+(* STREAMS ******************************************************************)
+
+coinductive stream (A:Type[0]): Type[0] ≝
+| seq: A → stream A → stream A
+.
+
+interpretation "cons (stream)" 'OPlusRight A a u = (seq A a u).
+
+(* Basic properties *********************************************************)
+
+lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
+#A * //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/ringeq_3.ma".
+include "ground_2/lib/stream.ma".
+
+(* STREAMS ******************************************************************)
+
+coinductive eq_stream (A): relation (stream A) ≝
+| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1⨮t1) (b2⨮t2)
+.
+
+interpretation "extensional equivalence (stream)"
+ 'RingEq A t1 t2 = (eq_stream A t1 t2).
+
+definition eq_stream_repl (A) (R:relation …) ≝
+ ∀t1,t2. t1 ≗{A} t2 → R t1 t2.
+
+definition eq_stream_repl_back (A) (R:predicate …) ≝
+ ∀t1. R t1 → ∀t2. t1 ≗{A} t2 → R t2.
+
+definition eq_stream_repl_fwd (A) (R:predicate …) ≝
+ ∀t1. R t1 → ∀t2. t2 ≗{A} t1 → R t2.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →
+ ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
+ u1 ≗ u2 ∧ a1 = a2.
+#A #t1 #t2 * -t1 -t2
+#t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/
+qed-.
+
+(* Basic properties *********************************************************)
+
+corec lemma eq_stream_refl: ∀A. reflexive … (eq_stream A).
+#A * #b #t @eq_seq //
+qed.
+
+corec lemma eq_stream_sym: ∀A. symmetric … (eq_stream A).
+#A #t1 #t2 * -t1 -t2
+#t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/
+qed-.
+
+lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd A R.
+/3 width=3 by eq_stream_sym/ qed-.
+
+(* Main properties **********************************************************)
+
+corec theorem eq_stream_trans: ∀A. Transitive … (eq_stream A).
+#A #t1 #t * -t1 -t
+#t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -b
+/3 width=7 by eq_seq/
+qed-.
+
+theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≗ t1 → t ≗ t2 → t1 ≗{A} t2.
+/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
+
+theorem eq_stream_canc_dx: ∀A,t,t1,t2. t1 ≗ t → t2 ≗ t → t1 ≗{A} t2.
+/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/downspoon_2.ma".
+include "ground_2/lib/stream_eq.ma".
+include "ground_2/lib/arith.ma".
+
+(* STREAMS ******************************************************************)
+
+definition hd (A:Type[0]): stream A → A ≝
+ λt. match t with [ seq a _ ⇒ a ].
+
+definition tl (A:Type[0]): stream A → stream A ≝
+ λt. match t with [ seq _ t ⇒ t ].
+
+interpretation "tail (stream)" 'DownSpoon A t = (tl A t).
+
+(* basic properties *********************************************************)
+
+lemma hd_rew (A) (a) (t): a = hd A (a⨮t).
+// qed.
+
+lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
+// qed.
+
+lemma eq_stream_split (A) (t): (hd … t) ⨮ ⫰t ≗{A} t.
+#A * //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/downspoonstar_3.ma".
+include "ground_2/lib/stream_hdtl.ma".
+
+(* STREAMS ******************************************************************)
+
+rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
+cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
+defined.
+
+interpretation "iterated tail (stram)" 'DownSpoonStar A n f = (tls A n f).
+
+(* basic properties *********************************************************)
+
+lemma tls_rew_O (A) (t): t = tls A 0 t.
+// qed.
+
+lemma tls_rew_S (A) (n) (t): ⫰⫰*[n]t = tls A (↑n) t.
+// qed.
+
+lemma tls_S1 (A) (n) (t): ⫰*[n]⫰t = tls A (↑n) t.
+#A #n elim n -n //
+qed.
+
+lemma tls_eq_repl (A) (n): eq_stream_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
+#A #n elim n -n //
+#n #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/oplusright_3.ma".
-include "ground_2/lib/relations.ma".
-
-(* STREAMS ******************************************************************)
-
-coinductive stream (A:Type[0]): Type[0] ≝
-| seq: A → stream A → stream A
-.
-
-interpretation "cons (nstream)" 'OPlusRight A a u = (seq A a u).
-
-(* Basic properties *********************************************************)
-
-lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
-#A * //
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/ringeq_3.ma".
-include "ground_2/lib/streams.ma".
-
-(* STREAMS ******************************************************************)
-
-coinductive eq_stream (A): relation (stream A) ≝
-| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1⨮t1) (b2⨮t2)
-.
-
-interpretation "extensional equivalence (nstream)"
- 'RingEq A t1 t2 = (eq_stream A t1 t2).
-
-definition eq_stream_repl (A) (R:relation …) ≝
- ∀t1,t2. t1 ≗{A} t2 → R t1 t2.
-
-definition eq_stream_repl_back (A) (R:predicate …) ≝
- ∀t1. R t1 → ∀t2. t1 ≗{A} t2 → R t2.
-
-definition eq_stream_repl_fwd (A) (R:predicate …) ≝
- ∀t1. R t1 → ∀t2. t2 ≗{A} t1 → R t2.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →
- ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
- u1 ≗ u2 ∧ a1 = a2.
-#A #t1 #t2 * -t1 -t2
-#t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/
-qed-.
-
-(* Basic properties *********************************************************)
-
-corec lemma eq_stream_refl: ∀A. reflexive … (eq_stream A).
-#A * #b #t @eq_seq //
-qed.
-
-corec lemma eq_stream_sym: ∀A. symmetric … (eq_stream A).
-#A #t1 #t2 * -t1 -t2
-#t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/
-qed-.
-
-lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd A R.
-/3 width=3 by eq_stream_sym/ qed-.
-
-(* Main properties **********************************************************)
-
-corec theorem eq_stream_trans: ∀A. Transitive … (eq_stream A).
-#A #t1 #t * -t1 -t
-#t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -b
-/3 width=7 by eq_seq/
-qed-.
-
-theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≗ t1 → t ≗ t2 → t1 ≗{A} t2.
-/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
-
-theorem eq_stream_canc_dx: ∀A,t,t1,t2. t1 ≗ t → t2 ≗ t → t1 ≗{A} t2.
-/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/downspoon_2.ma".
-include "ground_2/lib/streams_eq.ma".
-include "ground_2/lib/arith.ma".
-
-(* STREAMS ******************************************************************)
-
-definition hd (A:Type[0]): stream A → A ≝
- λt. match t with [ seq a _ ⇒ a ].
-
-definition tl (A:Type[0]): stream A → stream A ≝
- λt. match t with [ seq _ t ⇒ t ].
-
-interpretation "tail (streams)" 'DownSpoon A t = (tl A t).
-
-(* basic properties *********************************************************)
-
-lemma hd_rew (A) (a) (t): a = hd A (a⨮t).
-// qed.
-
-lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
-// qed.
-
-lemma eq_stream_split (A) (t): (hd … t) ⨮ ⫰t ≗{A} t.
-#A * //
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/downspoonstar_3.ma".
-include "ground_2/lib/streams_hdtl.ma".
-
-(* STREAMS ******************************************************************)
-
-rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
-cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
-defined.
-
-interpretation "iterated tail (strams)" 'DownSpoonStar A n f = (tls A n f).
-
-(* basic properties *********************************************************)
-
-lemma tls_rew_O (A) (t): t = tls A 0 t.
-// qed.
-
-lemma tls_rew_S (A) (n) (t): ⫰⫰*[n]t = tls A (↑n) t.
-// qed.
-
-lemma tls_S1 (A) (n) (t): ⫰*[n]⫰t = tls A (↑n) t.
-#A #n elim n -n //
-qed.
-
-lemma tls_eq_repl (A) (n): eq_stream_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
-#A #n elim n -n //
-#n #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
-qed.
(**************************************************************************)
include "ground_2/notation/functions/upspoon_1.ma".
-include "ground_2/lib/streams_tls.ma".
+include "ground_2/lib/stream_tls.ma".
(* RELOCATION N-STREAM ******************************************************)
projects / helm.git / commitdiff