From: Ferruccio Guidi Date: Mon, 4 Feb 2019 16:06:36 +0000 (+0100) Subject: minor corrections and updates X-Git-Tag: make_still_working~257 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e8fb201bad04ec30867659c2d42ef45a4b6c3393 minor corrections and updates intensional and extensional equivalence on lists coincide --- 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/stream.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream.ma new file mode 100644 index 000000000..757bfe724 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/stream_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_eq.ma new file mode 100644 index 000000000..cee2483f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_eq.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_hdtl.ma new file mode 100644 index 000000000..ff518a243 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_hdtl.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_tls.ma new file mode 100644 index 000000000..36492559a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/stream_tls.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma deleted file mode 100644 index e1b3a6812..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma deleted file mode 100644 index 878185ca1..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma +++ /dev/null @@ -1,71 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma deleted file mode 100644 index f128e5f73..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma +++ /dev/null @@ -1,39 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma deleted file mode 100644 index f2a910aa0..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma +++ /dev/null @@ -1,41 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. 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 ******************************************************)