From a4ba77d9df157e443e6fb39dc7376996faea9973 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 4 Mar 2016 15:14:13 +0000 Subject: [PATCH] commitcompleted: some files were missing :( --- .../lambdadelta/ground_2/lib/streams_tls.ma | 41 +++++++++++++++++++ .../ground_2/relocation/nstream_sand.ma | 15 +++++++ .../ground_2/relocation/rtmap_sand.ma | 40 ++++++++++++++++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 2 +- 4 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sand.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma new file mode 100644 index 000000000..96b9abe98 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_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/drops_2.ma". +include "ground_2/lib/streams_hdtl.ma". + +(* STREAMS ******************************************************************) + +let rec tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?. +cases n -n [ #t @t | #n #t @tl @(tls … n t) ] +qed. + +interpretation "recursive tail (strams)" 'Drops n f = (tls ? 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_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sand.ma new file mode 100644 index 000000000..181e8ceff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sand.ma @@ -0,0 +1,15 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/rtmap_sand.ma". diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma new file mode 100644 index 000000000..b830da071 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rintersection_3.ma". +include "ground_2/relocation/rtmap_sle.ma". + +coinductive sand: relation3 rtmap rtmap rtmap ≝ +| sand_pp: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → sand g1 g2 g +| sand_np: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → sand g1 g2 g +| sand_pn: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → sand g1 g2 g +| sand_nn: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → sand g1 g2 g +. + +interpretation "intersection (rtmap)" + 'RIntersection f1 f2 f = (sand f1 f2 f). + +(* Basic properties *********************************************************) + +let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?. +#f cases (pn_split f) * #g #H +[ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H // +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 |*: // ] +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 699d0767b..1612ee6a8 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 @@ -24,7 +24,7 @@ table { [ { "multiple relocation" * } { [ { "" * } { [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "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 ( ? ∘ ? )" * ] + [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "nstream_sand" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] -- 2.39.2