From 859c5cbb8ebffeddd1dd9cbc462e046b0709b4e4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 4 Mar 2016 19:52:33 +0000 Subject: [PATCH] small improvements and corrections ... --- .../lambdadelta/ground_2/lib/streams.ma | 52 -------------- .../lambdadelta/ground_2/lib/streams_eq.ma | 71 +++++++++++++++++++ .../lambdadelta/ground_2/lib/streams_hdtl.ma | 2 +- .../ground_2/relocation/rtmap_sand.ma | 3 +- .../lambdadelta/ground_2/web/ground_2_src.tbl | 4 +- 5 files changed, 75 insertions(+), 57 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma index ec7194229..d342a9934 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "ground_2/notation/constructors/cons_2.ma". -include "ground_2/notation/relations/exteq_3.ma". include "ground_2/lib/star.ma". (* STREAMS ******************************************************************) @@ -24,59 +23,8 @@ coinductive stream (A:Type[0]): Type[0] ≝ interpretation "cons (nstream)" 'Cons b t = (seq ? b t). -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)" - 'ExtEq 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 *********************************************************) lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a @ u ] = t. #A * // qed. - -let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?. -#A * #b #t @eq_seq // -qed. - -let corec 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 **********************************************************) - -let corec 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_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma new file mode 100644 index 000000000..839811603 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_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/exteq_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)" + 'ExtEq 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 *********************************************************) + +let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?. +#A * #b #t @eq_seq // +qed. + +let corec 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 **********************************************************) + +let corec 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 index 050568754..3a31efc35 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/functions/drop_1.ma". -include "ground_2/lib/streams.ma". +include "ground_2/lib/streams_eq.ma". include "ground_2/lib/arith.ma". (* STREAMS ******************************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma index b830da071..85ad506a2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma @@ -35,6 +35,5 @@ qed. let corec sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f ≝ ?. #f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g -[ @sand_pp | @sand_pn | @sand_np | @sand_nn ] -[4,11,18,25: @sand_sym // |1,2,3,8,9,10,15,16,17,22,23,24: skip |*: // ] +[ @sand_pp | @sand_pn | @sand_np | @sand_nn ] /2 width=7 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 1612ee6a8..cbff64690 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -23,7 +23,7 @@ table { class "grass" [ { "multiple relocation" * } { [ { "" * } { - [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] + [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "nstream_sand" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" @@ -37,7 +37,7 @@ table { class "yellow" [ { "extensions to the library" * } { [ { "" * } { - [ "stream ( ? @ ? ) ( ? ≐ ? )" "stream_hdtl" * ] + [ "stream ( ? @ ? )" "stream_eq ( ? ≐ ? )" "stream_hdtl ( ↓? )" "stream_tls ( ↓*[?]? )" * ] [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )" * ] [ "star" "lstar" * ] -- 2.39.2