From 4b8544042a6f3c5f5d303d4120c69abbc34ce15b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 29 Jan 2016 14:48:27 +0000 Subject: [PATCH] lift functions and identity map --- .../lambdadelta/ground_2/lib/arith.ma | 9 ++ .../lambdadelta/ground_2/lib/streams.ma | 24 +-- .../ground_2/notation/functions/identity_0.ma | 19 +++ .../ground_2/notation/functions/lift_1.ma | 19 +++ .../ground_2/relocation/nstream_after.ma | 5 +- .../ground_2/relocation/nstream_at.ma | 76 ++++++--- .../ground_2/relocation/nstream_id.ma | 145 ++++++++++++++++++ .../ground_2/relocation/nstream_lift.ma | 61 ++++++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 2 +- 9 files changed, 322 insertions(+), 38 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/identity_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/lift_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index d181e88cf..fad49e616 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -190,6 +190,15 @@ lemma lt_elim: ∀R:relation nat. ] qed-. +lemma le_elim: ∀R:relation nat. + (∀n2. R O (n2)) → + (∀n1,n2. R n1 n2 → R (⫯n1) (⫯n2)) → + ∀n1,n2. n1 ≤ n2 → R n1 n2. +#R #IH1 #IH2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2 +/4 width=1 by monotonic_pred/ -IH1 -IH2 +#n1 #H elim (lt_le_false … H) -H // +qed-. + (* Iterators ****************************************************************) (* Note: see also: lib/arithemetics/bigops.ma *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma index 30a045c54..4bb3883ce 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma @@ -25,17 +25,17 @@ coinductive stream (A:Type[0]): Type[0] ≝ interpretation "cons (nstream)" 'Cons b t = (seq ? b t). coinductive eq_stream (A): relation (stream A) ≝ -| eq_sec: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1@t1) (b2@t2) +| 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_back (A) (R:predicate …) (t1,t2) ≝ - t1 ≐⦋A⦌ t2 → R t1 → R t2. +definition eq_stream_repl_back (A) (R:predicate …) ≝ + ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 → R t2. -definition eq_stream_repl_fwd (A) (R:predicate …) (t1,t2) ≝ - t2 ≐⦋A⦌ t1 → R t1 → R t2. +definition eq_stream_repl_fwd (A) (R:predicate …) ≝ + ∀t1,t2. t2 ≐⦋A⦌ t1 → R t1 → R t2. (* Basic inversion lemmas ***************************************************) @@ -56,27 +56,27 @@ lemma stream_expand (A) (t:stream A): t = match t with [ seq a u ⇒ a @ u ]. qed. let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?. -#A * #b #t @eq_sec // +#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_sec /2 width=1 by/ +#t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/ qed-. -lemma eq_stream_repl_sym: ∀A,R,t1,t2. eq_stream_repl_back A R t1 t2 → eq_stream_repl_fwd A R t1 t2. -/3 width=1 by eq_stream_sym/ 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 #Hb1 #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -#Hb2 #Ht2 @eq_sec /2 width=3 by/ +#Hb2 #Ht2 @eq_seq /2 width=3 by/ qed-. theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≐ t1 → t ≐ t2 → t1 ≐⦋A⦌ t2. -/3 width=4 by eq_stream_trans, eq_stream_repl_sym/ qed-. +/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=4 by eq_stream_trans, eq_stream_repl_sym/ qed-. +/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/identity_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/identity_0.ma new file mode 100644 index 000000000..9d4aea574 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/identity_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( 𝐈𝐝 )" + non associative with precedence 90 + for @{ 'Identity }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/lift_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/lift_1.ma new file mode 100644 index 000000000..4d0fd7f04 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/lift_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( ↑ term 46 T )" + non associative with precedence 46 + for @{ 'Lift $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma index 154ba25e3..cf5a6b6eb 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -420,14 +420,15 @@ let corec after_mono: ∀t1,t2,x. t1 ⊚ t2 ≡ x → ∀y. t1 ⊚ t2 ≡ y → * #a1 #t1 * #a2 #t2 * #c #x #Hx * #d #y #Hy cases (after_inv_apply … Hx) -Hx #Hc #Hx cases (after_inv_apply … Hy) -Hy #Hd #Hy -/3 width=4 by eq_sec/ +/3 width=4 by eq_seq/ qed-. let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?. * #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy cases (after_inv_apply … Hx) -Hx #Hc #Hx cases (after_inv_apply … Hy) -Hy #Hd -cases (apply_inj_aux … Hc Hd) #Hy -a -d /3 width=4 by eq_sec/ +cases (apply_inj_aux … Hc Hd) // +#Hy -a -d /3 width=4 by eq_seq/ qed-. (* Main inversion lemmas on after *******************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma index ed1aa9b60..4b812836b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma @@ -157,7 +157,7 @@ qed-. lemma at_total: ∀i,t. @⦃i, t⦄ ≡ t@❴i❵. #i elim i -i [ * // | #i #IH * /3 width=1 by at_S1/ ] -qed. +qed. (* Advanced forward lemmas on at ********************************************) @@ -180,46 +180,76 @@ lemma at_increasing_strict: ∀t,b,i1,i2. @⦃i1, ⫯b @ t⦄ ≡ i2 → #j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/ qed-. +lemma at_fwd_id: ∀t,b,i. @⦃i, b@t⦄ ≡ i → b = 0. +#t #b * +[ #H <(at_inv_O1 … H) -t -b // +| #i #H elim (at_inv_S1 … H) -H + #j #H #H0 destruct lapply (at_increasing … H) -H + #H lapply (eq_minus_O … H) -H // +] +qed. + (* Main properties on at ****************************************************) +lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀t. @⦃i2, t⦄ ≡ i2 → @⦃i1, t⦄ ≡ i1. +#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ] +* #b #t #H lapply (at_fwd_id … H) +#H0 destruct /4 width=1 by at_S1, at_inv_SOS/ +qed-. + let corec at_ext: ∀t1,t2. (∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i1 = i2) → t1 ≐ t2 ≝ ?. * #b1 #t1 * #b2 #t2 #Hi lapply (Hi 0 b1 b2 ? ?) // -#H lapply (at_ext t1 t2 ?) /2 width=1 by eq_sec/ -at_ext +#H lapply (at_ext t1 t2 ?) /2 width=1 by eq_seq/ -at_ext #j #j1 #j2 #H1 #H2 @(injective_plus_r … b2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *) qed-. -theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀t,j1,j2. @⦃i1, t⦄ ≡ j1 → @⦃i2, t⦄ ≡ j2 → j1 < j2. +theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀t1,t2. t1 ≐ t2 → ∀j1,j2. @⦃i1, t1⦄ ≡ j1 → @⦃i2, t2⦄ ≡ j2 → j1 < j2. #i1 #i2 #H @(lt_elim … H) -i1 -i2 -[ #i2 *#b #t #j1 #j2 #H1 #H2 >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 // -| #i1 #i2 #IH * #b #t #j1 #j2 #H1 #H2 elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2 - #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=3 by lt_S_S, monotonic_lt_plus_r/ +[ #i2 * #b1 #t1 * #b2 #t2 #H elim (eq_stream_inv_seq ????? H) -H + #H #Ht #j1 #j2 #H1 #H2 destruct + >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 // +| #i1 #i2 #IH * #b1 #t1 * #b2 #t2 #H elim (eq_stream_inv_seq ????? H) -H + #H #Ht #j1 #j2 #H1 #H2 destruct + elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2 + #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=5 by lt_S_S, monotonic_lt_plus_r/ ] qed-. -theorem at_inv_monotonic: ∀t,i1,j1. @⦃i1, t⦄ ≡ j1 → ∀i2,j2. @⦃i2, t⦄ ≡ j2 → j2 < j1 → i2 < i1. -#t #i1 #j1 #H elim H -t -i1 -j1 -[ #t #i2 #j2 #_ #H elim (lt_le_false … H) // -| #t #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xOx … H) -H * +theorem at_inv_monotonic: ∀t1,i1,j1. @⦃i1, t1⦄ ≡ j1 → ∀t2,i2,j2. @⦃i2, t2⦄ ≡ j2 → t1 ≐ t2 → j2 < j1 → i2 < i1. +#t1 #i1 #j1 #H elim H -t1 -i1 -j1 +[ #t1 #t2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) // +| #t1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht + #H0 #Ht destruct elim (at_inv_xOx … H) -H * [ #H1 #H2 destruct // - | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=3 by lt_S_S_to_lt, lt_S_S/ + | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=5 by lt_S_S_to_lt, lt_S_S/ ] -| #t #b1 #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xSx … H) -H - #y2 #Hy #H destruct /3 width=3 by lt_S_S_to_lt/ +| #t1 #b1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht + #H0 #Ht destruct elim (at_inv_xSx … H) -H + #y2 #Hy #H destruct /3 width=5 by eq_seq, lt_S_S_to_lt/ ] qed-. -theorem at_mono: ∀t,i,i1. @⦃i, t⦄ ≡ i1 → ∀i2. @⦃i, t⦄ ≡ i2 → i2 = i1. -#t #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // -#Hi elim (lt_le_false i i) /2 width=6 by at_inv_monotonic/ +theorem at_mono: ∀t1,t2. t1 ≐ t2 → ∀i,i1. @⦃i, t1⦄ ≡ i1 → ∀i2. @⦃i, t2⦄ ≡ i2 → i2 = i1. +#t1 #t2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_stream_sym/ qed-. -theorem at_inj: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀i2. @⦃i2, t⦄ ≡ i → i1 = i2. -#t #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // -#Hi elim (lt_le_false i i) /2 width=6 by at_monotonic/ +theorem at_inj: ∀t1,t2. t1 ≐ t2 → ∀i1,i. @⦃i1, t1⦄ ≡ i → ∀i2. @⦃i2, t2⦄ ≡ i → i1 = i2. +#t1 #t2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_stream_sym/ qed-. lemma at_inv_total: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → i2 = t@❴i1❵. -/2 width=4 by at_mono/ qed-. +/2 width=6 by at_mono/ qed-. + +lemma at_repl_back: ∀i1,i2. eq_stream_repl_back ? (λt. @⦃i1, t⦄ ≡ i2). +#i1 #i2 #t1 #t2 #Ht #H1 lapply (at_total i1 t2) +#H2 <(at_mono … Ht … H1 … H2) -t1 -i2 // +qed-. + +lemma at_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λt. @⦃i1, t⦄ ≡ i2). +#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_repl_back/ +qed-. (* Advanced properties on at ************************************************) @@ -228,7 +258,7 @@ lemma at_dec: ∀t,i1,i2. Decidable (@⦃i1, t⦄ ≡ i2). #t #i1 #i2 lapply (at_total i1 t) #Ht elim (eq_nat_dec i2 (t@❴i1❵)) [ #H destruct /2 width=1 by or_introl/ -| /4 width=4 by at_mono, or_intror/ +| /4 width=6 by at_mono, or_intror/ ] qed-. @@ -248,5 +278,5 @@ qed-. (* Advanced properties on apply *********************************************) -fact apply_inj_aux: ∀t,i,i1,i2. i = t@❴i1❵ → i = t@❴i2❵ → i1 = i2. -/2 width=4 by at_inj/ qed-. +fact apply_inj_aux: ∀t1,t2. t1 ≐ t2 → ∀i,i1,i2. i = t1@❴i1❵ → i = t2@❴i2❵ → i1 = i2. +/2 width=6 by at_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma new file mode 100644 index 000000000..d76d12940 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma @@ -0,0 +1,145 @@ +(**************************************************************************) +(* ___ *) +(* ||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/identity_0.ma". +include "ground_2/notation/relations/isidentity_1.ma". +include "ground_2/relocation/nstream_lift.ma". +include "ground_2/relocation/nstream_after.ma". + +(* RELOCATION N-STREAM ******************************************************) + +let corec id: nstream ≝ ↑id. + +interpretation "identity (nstream)" + 'Identity = (id). + +definition isid: predicate nstream ≝ λt. t ≐ 𝐈𝐝. + +interpretation "test for identity (trace)" + 'IsIdentity t = (isid t). + +(* Basic properties on id ***************************************************) + +lemma id_unfold: 𝐈𝐝 = ↑𝐈𝐝. +>(stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize // +qed. + +(* Basic properties on isid *************************************************) + +lemma isid_id: 𝐈⦃𝐈𝐝⦄. +// qed. + +lemma isid_push: ∀t. 𝐈⦃t⦄ → 𝐈⦃↑t⦄. +#t #H normalize >id_unfold /2 width=1 by eq_seq/ +qed. + +(* Basic inversion lemmas on isid *******************************************) + +lemma isid_inv_seq: ∀t,a. 𝐈⦃a@t⦄ → 𝐈⦃t⦄ ∧ a = 0. +#t #a normalize >id_unfold in ⊢ (???%→?); +#H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/ +qed-. + +lemma isid_inv_push: ∀t. 𝐈⦃↑t⦄ → 𝐈⦃t⦄. +* #a #t #H elim (isid_inv_seq … H) -H // +qed-. + +lemma isid_inv_next: ∀t. 𝐈⦃⫯t⦄ → ⊥. +* #a #t #H elim (isid_inv_seq … H) -H +#_ #H destruct +qed-. + +(* inversion lemmas on at ***************************************************) + +let corec id_inv_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → t ≐ 𝐈𝐝 ≝ ?. +* #a #t #Ht lapply (Ht 0) +#H lapply (at_inv_O1 … H) -H +#H0 >id_unfold @eq_seq +[ cases H0 -a // +| @id_inv_at -id_inv_at + #i lapply (Ht (⫯i)) -Ht cases H0 -a + #H elim (at_inv_SOx … H) -H // +] +qed-. + +lemma isid_inv_at: ∀i,t. 𝐈⦃t⦄ → @⦃i, t⦄ ≡ i. +#i elim i -i +[ * #a #t #H elim (isid_inv_seq … H) -H // +| #i #IH * #a #t #H elim (isid_inv_seq … H) -H + /3 width=1 by at_S1/ +] +qed-. + +lemma isid_inv_at_mono: ∀t,i1,i2. 𝐈⦃t⦄ → @⦃i1, t⦄ ≡ i2 → i1 = i2. +/3 width=6 by isid_inv_at, at_mono/ qed-. + +(* Properties on at *********************************************************) + +lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i. +/2 width=1 by isid_inv_at/ qed. + +lemma isid_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → 𝐈⦃t⦄. +/2 width=1 by id_inv_at/ qed. + +lemma isid_at_total: ∀t. (∀i1,i2. @⦃i1, t⦄ ≡ i2 → i1 = i2) → 𝐈⦃t⦄. +#t #Ht @isid_at +#i lapply (at_total i t) +#H >(Ht … H) in ⊢ (???%); -Ht // +qed. + +(* Properties on after ******************************************************) + +lemma after_isid_dx: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t2 ≐ t → 𝐈⦃t1⦄. +#t2 #t1 #t #Ht #H2 @isid_at_total +#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -t1 +/3 width=6 by at_inj, eq_stream_sym/ +qed. + +lemma after_isid_sn: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t1 ≐ t → 𝐈⦃t2⦄. +#t2 #t1 #t #Ht #H1 @isid_at_total +#i2 #i #Hi2 lapply (at_total i2 t1) +#H0 lapply (at_increasing … H0) +#Ht1 lapply (after_fwd_at2 … (t1@❴i2❵) … H0 … Ht) +/3 width=7 by at_repl_back, at_mono, at_id_le/ +qed. + +(* Inversion lemmas on after ************************************************) + +let corec isid_after_sn: ∀t1,t2. 𝐈⦃t1⦄ → t1 ⊚ t2 ≡ t2 ≝ ?. +* #a1 #t1 * * [ | #a2 ] #t2 #H cases (isid_inv_seq … H) -H +#Ht1 #H1 +[ @(after_zero … H1) -H1 /2 width=1 by/ +| @(after_skip … H1) -H1 /2 width=5 by/ +] +qed-. + +let corec isid_after_dx: ∀t2,t1. 𝐈⦃t2⦄ → t1 ⊚ t2 ≡ t1 ≝ ?. +* #a2 #t2 * * +[ #t1 #H cases (isid_inv_seq … H) -H + #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/ +| #a1 #t1 #H @(after_drop … a1 a1) /2 width=5 by/ +] +qed-. + +lemma after_isid_inv_sn: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t1⦄ → t2 ≐ t. +/3 width=4 by isid_after_sn, after_mono/ +qed-. + +lemma after_isid_inv_dx: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t2⦄ → t1 ≐ t. +/3 width=4 by isid_after_dx, after_mono/ +qed-. +(* +lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄. +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma new file mode 100644 index 000000000..07a96e4d5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lift_1.ma". +include "ground_2/relocation/nstream_at.ma". + +(* RELOCATION N-STREAM ******************************************************) + +definition push: nstream → nstream ≝ λt. 0@t. + +interpretation "push (nstream)" 'Lift t = (push t). + +definition next: nstream → nstream. +* #a #t @(⫯a@t) +qed. + +interpretation "next (nstream)" 'Successor t = (next t). + +(* Basic properties on push *************************************************) + +lemma push_at_O: ∀t. @⦃0, ↑t⦄ ≡ 0. +// qed. + +lemma push_at_S: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃⫯i1, ↑t⦄ ≡ ⫯i2. +/2 width=1 by at_S1/ qed. + +(* Basic inversion lemmas on push *******************************************) + +lemma push_inv_at_S: ∀t,i1,i2. @⦃⫯i1, ↑t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2. +/2 width=1 by at_inv_SOS/ qed-. + +lemma injective_push: injective ? ? push. +#t1 #t2 normalize #H destruct // +qed-. + +(* Basic properties on next *************************************************) + +lemma next_at: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃i1, ⫯t⦄ ≡ ⫯i2. +* /2 width=1 by at_lift/ +qed. + +(* Basic inversion lemmas on next *******************************************) + +lemma next_inv_at: ∀t,i1,i2. @⦃i1, ⫯t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2. +* /2 width=1 by at_inv_xSS/ +qed-. + +lemma injective_next: injective ? ? next. +* #a1 #t1 * #a2 #t2 normalize #H destruct // +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 ae1acddff..50896c56c 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 @@ -12,7 +12,7 @@ table { class "green" [ { "multiple relocation" * } { [ { "" * } { - [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ] + [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ] [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ] -- 2.39.2