From e8fb201bad04ec30867659c2d42ef45a4b6c3393 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Feb 2019 17:06:36 +0100 Subject: [PATCH] minor corrections and updates intensional and extensional equivalence on lists coincide --- .../lambdadelta/ground_2/lib/list_eq.ma | 57 +++++++++++++++++++ .../ground_2/lib/{streams.ma => stream.ma} | 2 +- .../lib/{streams_eq.ma => stream_eq.ma} | 4 +- .../lib/{streams_hdtl.ma => stream_hdtl.ma} | 4 +- .../lib/{streams_tls.ma => stream_tls.ma} | 4 +- .../ground_2/relocation/nstream.ma | 2 +- 6 files changed, 65 insertions(+), 8 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/list_eq.ma rename matita/matita/contribs/lambdadelta/ground_2/lib/{streams.ma => stream.ma} (95%) rename matita/matita/contribs/lambdadelta/ground_2/lib/{streams_eq.ma => stream_eq.ma} (97%) rename matita/matita/contribs/lambdadelta/ground_2/lib/{streams_hdtl.ma => stream_hdtl.ma} (94%) rename matita/matita/contribs/lambdadelta/ground_2/lib/{streams_tls.ma => stream_tls.ma} (93%) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list_eq.ma new file mode 100644 index 000000000..d1b2be454 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list_eq.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/stream.ma index e1b3a6812..757bfe724 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream.ma @@ -21,7 +21,7 @@ coinductive stream (A:Type[0]): Type[0] ≝ | seq: A → stream A → stream A . -interpretation "cons (nstream)" 'OPlusRight A a u = (seq A a u). +interpretation "cons (stream)" 'OPlusRight A a u = (seq A a u). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_eq.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/stream_eq.ma index 878185ca1..cee2483f3 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_eq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/relations/ringeq_3.ma". -include "ground_2/lib/streams.ma". +include "ground_2/lib/stream.ma". (* STREAMS ******************************************************************) @@ -21,7 +21,7 @@ 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)" +interpretation "extensional equivalence (stream)" 'RingEq A t1 t2 = (eq_stream A t1 t2). definition eq_stream_repl (A) (R:relation …) ≝ diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_hdtl.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/stream_hdtl.ma index f128e5f73..ff518a243 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_hdtl.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/functions/downspoon_2.ma". -include "ground_2/lib/streams_eq.ma". +include "ground_2/lib/stream_eq.ma". include "ground_2/lib/arith.ma". (* STREAMS ******************************************************************) @@ -24,7 +24,7 @@ definition hd (A:Type[0]): stream 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). +interpretation "tail (stream)" 'DownSpoon A t = (tl A t). (* basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_tls.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/stream_tls.ma index f2a910aa0..36492559a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_tls.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/functions/downspoonstar_3.ma". -include "ground_2/lib/streams_hdtl.ma". +include "ground_2/lib/stream_hdtl.ma". (* STREAMS ******************************************************************) @@ -21,7 +21,7 @@ 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). +interpretation "iterated tail (stram)" 'DownSpoonStar A n f = (tls A n f). (* basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma index 3803c254b..c5ccb7373 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma @@ -13,7 +13,7 @@ (**************************************************************************) 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 ******************************************************) -- 2.39.2