From: Ferruccio Guidi Date: Tue, 23 Feb 2016 15:36:51 +0000 (+0000) Subject: precommit for rtmap ... X-Git-Tag: make_still_working~641 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=91ab6965be539b7ed0f3208e1c1fffd17aa151f7 precommit for rtmap ... --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index fad49e616..325e07d38 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -109,6 +109,9 @@ qed. lemma lt_S_S: ∀x,y. x < y → ⫯x < ⫯y. /2 width=1 by le_S_S/ qed. +lemma lt_S: ∀n,m. n < m → n < ⫯m. +/2 width=1 by le_S/ qed. + lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1. /3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed. @@ -145,6 +148,21 @@ qed-. lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥. /3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-. +lemma lt_inv_O1: ∀n. 0 < n → ∃m. ⫯m = n. +* /2 width=2 by ex_intro/ +#H cases (lt_le_false … H) -H // +qed-. + +lemma lt_inv_S1: ∀m,n. ⫯m < n → ∃∃p. m < p & ⫯p = n. +#m * /3 width=3 by lt_S_S_to_lt, ex2_intro/ +#H cases (lt_le_false … H) -H // +qed-. + +lemma lt_inv_gen: ∀y,x. x < y → ∃∃z. x ≤ z & ⫯z = y. +* /3 width=3 by le_S_S_to_le, ex2_intro/ +#x #H elim (lt_le_false … H) -H // +qed-. + lemma pred_inv_refl: ∀m. pred m = m → m = 0. * // normalize #m #H elim (lt_refl_false m) // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma index 38540eecd..ec7194229 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma @@ -42,19 +42,16 @@ definition eq_stream_repl_fwd (A) (R:predicate …) ≝ (* Basic inversion lemmas ***************************************************) -fact eq_stream_inv_seq_aux: ∀A,t1,t2. t1 ≐⦋A⦌ t2 → - ∀u1,u2,a1,a2. t1 = a1@u1 → t2 = a2@u2 → - a1 = a2 ∧ u1 ≐ u2. +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-. -lemma eq_stream_inv_seq: ∀A,t1,t2,b1,b2. b1@t1 ≐⦋A⦌ b2@t2 → b1 = b2 ∧ t1 ≐ t2. -/2 width=5 by eq_stream_inv_seq_aux/ qed-. - (* Basic properties *********************************************************) -lemma stream_expand (A) (t:stream A): t = match t with [ seq a u ⇒ a @ u ]. +lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a @ u ] = t. #A * // qed. @@ -74,8 +71,8 @@ lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd 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_seq /2 width=3 by/ +#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. 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 e23b7bb2d..bdc740c82 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma @@ -35,6 +35,5 @@ qed. lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2). #A #i elim i -i // -#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq ????? H) -H -/2 width=1 by/ +#i #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/notation/relations/funexteq_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/funexteq_2.ma new file mode 100644 index 000000000..c0c1aeb81 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/funexteq_2.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( f1 ≗ break term 46 f2 )" + non associative with precedence 45 + for @{ 'FunExtEq $f1 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/istotal_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/istotal_1.ma new file mode 100644 index 000000000..dd89fc23e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/istotal_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 f ⦄ )" + non associative with precedence 45 + for @{ 'IsTotal $f }. 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 b27633d11..b599e03cc 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -458,3 +458,44 @@ qed-. theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f. /2 width=8 by after_mono/ qed-. + +(* Properties on after ******************************************************) + +lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄. +#f2 #f1 #f #Ht #H2 @isid_at_total +#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1 +/3 width=6 by at_inj, eq_stream_sym/ +qed. + +lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄. +#f2 #f1 #f #Ht #H1 @isid_at_total +#i2 #i #Hi2 lapply (at_total i2 f1) +#H0 lapply (at_increasing … H0) +#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht) +/3 width=7 by at_eq_repl_back, at_mono, at_id_le/ +qed. + +(* Inversion lemmas on after ************************************************) + +let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?. +* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H +/3 width=7 by after_push, after_refl/ +qed-. + +let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?. +* #n2 #f2 * * +[ #f1 #H cases (isid_inv_seq … H) -H + /3 width=7 by after_refl/ +| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/ +] +qed-. + +lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f. +/3 width=8 by isid_after_sn, after_mono/ +qed-. + +lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f. +/3 width=8 by isid_after_dx, after_mono/ +qed-. + +axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma deleted file mode 100644 index 9cb77e391..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma +++ /dev/null @@ -1,298 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.tcs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground_2/notation/functions/apply_2.ma". -include "ground_2/notation/relations/rat_3.ma". -include "ground_2/relocation/nstream_lift.ma". - -(* RELOCATION N-STREAM ******************************************************) - -let rec apply (i: nat) on i: rtmap → nat ≝ ?. -* #n #f cases i -i -[ @n -| #i lapply (apply i f) -apply -i -f - #i @(⫯(n+i)) -] -defined. - -interpretation "functional application (nstream)" - 'Apply f i = (apply i f). - -inductive at: rtmap → relation nat ≝ -| at_refl: ∀f. at (↑f) 0 0 -| at_push: ∀f,i1,i2. at f i1 i2 → at (↑f) (⫯i1) (⫯i2) -| at_next: ∀f,i1,i2. at f i1 i2 → at (⫯f) i1 (⫯i2) -. - -interpretation "relational application (nstream)" - 'RAt i1 f i2 = (at f i1 i2). - -(* Basic properties on apply ************************************************) - -lemma apply_eq_repl (i): eq_stream_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵). -#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H -elim (eq_stream_inv_seq ????? H) -H normalize // -#Hn #Hf /4 width=1 by eq_f2, eq_f/ -qed. - -lemma apply_S1: ∀f,n,i. (⫯n@f)@❴i❵ = ⫯((n@f)@❴i❵). -#n #f * // -qed. - -(* Basic inversion lemmas on at *********************************************) - -fact at_inv_OOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. i1 = 0 → f = ↑g → i2 = 0. -#f #i1 #i2 * -f -i1 -i2 // -[ #f #i1 #i2 #_ #g #H destruct -| #f #i1 #i2 #_ #g #_ #H elim (discr_next_push … H) -] -qed-. - -lemma at_inv_OOx: ∀f,i2. @⦃0, ↑f⦄ ≡ i2 → i2 = 0. -/2 width=6 by at_inv_OOx_aux/ qed-. - -fact at_inv_SOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j1. i1 = ⫯j1 → f = ↑g → - ∃∃j2. @⦃j1, g⦄ ≡ j2 & i2 = ⫯j2. -#f #i1 #i2 * -f -i1 -i2 -[ #f #g #j1 #H destruct -| #f #i1 #i2 #Hi #g #j1 #H #Hf <(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/ -| #f #i1 #i2 #_ #g #j1 #_ #H elim (discr_next_push … H) -] -qed-. - -lemma at_inv_SOx: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ i2 → - ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2. -/2 width=5 by at_inv_SOx_aux/ qed-. - -fact at_inv_xSx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. f = ⫯g → - ∃∃j2. @⦃i1, g⦄ ≡ j2 & i2 = ⫯j2. -#f #i1 #i2 * -f -i1 -i2 -[ #f #g #H elim (discr_push_next … H) -| #f #i1 #i2 #_ #g #H elim (discr_push_next … H) -| #f #i1 #i2 #Hi #g #H <(injective_next … H) -g /2 width=3 by ex2_intro/ -] -qed-. - -lemma at_inv_xSx: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ i2 → - ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2. -/2 width=3 by at_inv_xSx_aux/ qed-. - -(* Advanced inversion lemmas on at ******************************************) - -lemma at_inv_OOS: ∀f,i2. @⦃0, ↑f⦄ ≡ ⫯i2 → ⊥. -#f #i2 #H lapply (at_inv_OOx … H) -H -#H destruct -qed-. - -lemma at_inv_SOS: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. -#f #i1 #i2 #H elim (at_inv_SOx … H) -H -#j2 #H2 #H destruct // -qed-. - -lemma at_inv_SOO: ∀f,i1. @⦃⫯i1, ↑f⦄ ≡ 0 → ⊥. -#f #i1 #H elim (at_inv_SOx … H) -H -#j2 #_ #H destruct -qed-. - -lemma at_inv_xSS: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. -#f #i1 #i2 #H elim (at_inv_xSx … H) -H -#j2 #H #H2 destruct // -qed-. - -lemma at_inv_xSO: ∀f,i1. @⦃i1, ⫯f⦄ ≡ 0 → ⊥. -#f #i1 #H elim (at_inv_xSx … H) -H -#j2 #_ #H destruct -qed-. - -lemma at_inv_xOx: ∀f,i1,i2. @⦃i1, ↑f⦄ ≡ i2 → - (i1 = 0 ∧ i2 = 0) ∨ - ∃∃j1,j2. @⦃j1, f⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2. -#f * [2: #i1 ] #i2 #H -[ elim (at_inv_SOx … H) -H - #j2 #H2 #H destruct /3 width=5 by or_intror, ex3_2_intro/ -| >(at_inv_OOx … H) -i2 /3 width=1 by conj, or_introl/ -] -qed-. - -lemma at_inv_xOO: ∀f,i. @⦃i, ↑f⦄ ≡ 0 → i = 0. -#f #i #H elim (at_inv_xOx … H) -H * // -#j1 #j2 #_ #_ #H destruct -qed-. - -lemma at_inv_xOS: ∀f,i1,i2. @⦃i1, ↑f⦄ ≡ ⫯i2 → - ∃∃j1. @⦃j1, f⦄ ≡ i2 & i1 = ⫯j1. -#f #i1 #i2 #H elim (at_inv_xOx … H) -H * -[ #_ #H destruct -| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/ -] -qed-. - -(* alternative definition ***************************************************) - -lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≡ i2. -#i2 elim i2 -i2 /2 width=1 by at_refl, at_next/ -qed. - -lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, n@f⦄ ≡ ⫯(n+i2). -#n elim n -n /3 width=1 by at_push, at_next/ -qed. - -lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≡ i2 → i2 = n. -#f #n elim n -n /2 width=2 by at_inv_OOx/ -#n #IH #i2 (at_inv_O1 … H) -i2 // -| #i1 #i2 #H elim (at_inv_S1 … H) -H - #j1 #Ht #H destruct - /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/ -] -qed-. - -lemma at_increasing_strict: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ i2 → - i1 < i2 ∧ @⦃i1, f⦄ ≡ ⫰i2. -#f #i1 #i2 #H elim (at_inv_xSx … H) -H -#j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/ -qed-. - -lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≡ i → n = 0. -#f #n * -[ #H <(at_inv_O1 … H) -f -n // -| #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-. - -(* Basic properties on at ***************************************************) - -lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i. -#f #i1 #i #n #m #H elim m -m /2 width=1 by at_next/ -qed. - -(* Advanced properties on at ************************************************) - -lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1. -#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ] -* #n #f #H lapply (at_fwd_id … H) -#H0 destruct /4 width=1 by at_S1, at_inv_SOS/ -qed-. - -(* Main properties on at ****************************************************) - -let corec at_ext: ∀f1,f2. (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≐ f2 ≝ ?. -* #n1 #f1 * #n2 #f2 #Hi lapply (Hi 0 n1 n2 ? ?) // -#H lapply (at_ext f1 f2 ?) /2 width=1 by eq_seq/ -at_ext -#j #j1 #j2 #H1 #H2 @(injective_plus_r … n2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *) -qed-. - -theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀f1,f2. f1 ≐ f2 → ∀j1,j2. @⦃i1, f1⦄ ≡ j1 → @⦃i2, f2⦄ ≡ j2 → j1 < j2. -#i1 #i2 #H @(lt_elim … H) -i1 -i2 -[ #i2 * #n1 #f1 * #n2 #f2 #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 * #n1 #f1 * #n2 #f2 #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: ∀f1,i1,j1. @⦃i1, f1⦄ ≡ j1 → ∀f2,i2,j2. @⦃i2, f2⦄ ≡ j2 → f1 ≐ f2 → j2 < j1 → i2 < i1. -#f1 #i1 #j1 #H elim H -f1 -i1 -j1 -[ #f1 #f2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) // -| #f1 #i1 #j1 #_ #IH * #n2 #f2 #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=5 by lt_S_S_to_lt, lt_S_S/ - ] -| * #n1 #f1 #i1 #j1 #_ #IH * #n2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht - #H0 #Ht destruct (stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize // -qed. - -(* Basic properties on isid *************************************************) - -lemma isid_eq_repl_back: eq_stream_repl_back … isid. -/2 width=3 by eq_stream_canc_sn/ qed-. - -lemma isid_eq_repl_fwd: eq_stream_repl_fwd … isid. -/3 width=3 by isid_eq_repl_back, eq_stream_repl_sym/ qed-. - -lemma isid_id: 𝐈⦃𝐈𝐝⦄. -// qed. - -lemma isid_push: ∀f. 𝐈⦃f⦄ → 𝐈⦃↑f⦄. -#f #H normalize >id_unfold /2 width=1 by eq_seq/ -qed. - -(* Basic inversion lemmas on isid *******************************************) - -lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ n = 0. -#f #n normalize >id_unfold in ⊢ (???%→?); -#H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/ -qed-. - -lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄. -* #n #f #H elim (isid_inv_seq … H) -H // -qed-. - -lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥. -* #n #f #H elim (isid_inv_seq … H) -H -#_ #H destruct -qed-. - -lemma isid_inv_gen: ∀f. 𝐈⦃f⦄ → ∃∃g. 𝐈⦃g⦄ & f = ↑g. -* #n #f #H elim (isid_inv_seq … H) -H -#Hf #H destruct /2 width=3 by ex2_intro/ -qed-. - -lemma isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≐ f2. -/2 width=3 by eq_stream_canc_dx/ qed-. - -(* inversion lemmas on at ***************************************************) - -let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?. -* #n #f #Ht lapply (Ht 0) -#H lapply (at_inv_O1 … H) -H -#H0 >id_unfold @eq_seq -[ cases H0 -n // -| @id_inv_at -id_inv_at - #i lapply (Ht (⫯i)) -Ht cases H0 -n - #H elim (at_inv_SOx … H) -H // -] -qed-. - -lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i. -#i elim i -i -[ * #n #f #H elim (isid_inv_seq … H) -H // -| #i #IH * #n #f #H elim (isid_inv_seq … H) -H - /3 width=1 by at_S1/ -] -qed-. - -lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ 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: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄. -/2 width=1 by id_inv_at/ qed. - -lemma isid_at_total: ∀f. (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄. -#f #Ht @isid_at -#i lapply (at_total i f) -#H >(Ht … H) in ⊢ (???%); -Ht // -qed. - -(* Properties on after ******************************************************) - -lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄. -#f2 #f1 #f #Ht #H2 @isid_at_total -#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1 -/3 width=6 by at_inj, eq_stream_sym/ +lemma id_rew: ↑𝐈𝐝 = 𝐈𝐝. +<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize // qed. -lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄. -#f2 #f1 #f #Ht #H1 @isid_at_total -#i2 #i #Hi2 lapply (at_total i2 f1) -#H0 lapply (at_increasing … H0) -#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht) -/3 width=7 by at_eq_repl_back, at_mono, at_id_le/ +lemma id_eq_rew: ↑𝐈𝐝 ≗ 𝐈𝐝. +cases id_rew in ⊢ (??%); // qed. - -(* Inversion lemmas on after ************************************************) - -let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?. -* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H -/3 width=7 by after_push, after_refl/ -qed-. - -let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?. -* #n2 #f2 * * -[ #f1 #H cases (isid_inv_seq … H) -H - /3 width=7 by after_refl/ -| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/ -] -qed-. - -lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f. -/3 width=8 by isid_after_sn, after_mono/ -qed-. - -lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f. -/3 width=8 by isid_after_dx, after_mono/ -qed-. - -axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma new file mode 100644 index 000000000..91487980d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/rtmap_isid.ma". + +(* RELOCATION N-STREAM ******************************************************) + +(* Specific inversion lemmas ************************************************) + +lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ 0 = n. +#f #n #H elim (isid_inv_gen … H) -H +#g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma new file mode 100644 index 000000000..c64c7011c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/functions/apply_2.ma". +include "ground_2/relocation/nstream_eq.ma". +include "ground_2/relocation/rtmap_istot.ma". + +(* RELOCATION N-STREAM ******************************************************) + +let rec apply (i: nat) on i: rtmap → nat ≝ ?. +* #n #f cases i -i +[ @n +| #i lapply (apply i f) -apply -i -f + #i @(⫯(n+i)) +] +defined. + +interpretation "functional application (nstream)" + 'Apply f i = (apply i f). + +(* Specific properties on at ************************************************) + +lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≡ i2. +#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/ +qed. + +lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, n@f⦄ ≡ ⫯(n+i2). +#n elim n -n /3 width=7 by at_push, at_next/ +qed. + +lemma at_total: ∀i1,f. @⦃i1, f⦄ ≡ f@❴i1❵. +#i1 elim i1 -i1 +[ * // | #i #IH * /3 width=1 by at_S1/ ] +qed. + +lemma at_istot: ∀f. 𝐓⦃f⦄. +/2 width=2 by ex_intro/ qed. + +lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i. +#f #i1 #i #n #m #H elim m -m /2 width=5 by at_next/ +qed. + +(* Specific inversion lemmas on at ******************************************) + +lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≡ i2 → n = i2. +#f #n elim n -n /2 width=6 by at_inv_ppx/ +#n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ] +#j2 #Hj * -i2 /3 width=1 by eq_f/ +qed-. + +lemma at_inv_S1: ∀f,n,j1,i2. @⦃⫯j1, n@f⦄ ≡ i2 → + ∃∃j2. @⦃j1, f⦄ ≡ j2 & ⫯(n+j2) = i2. +#f #n elim n -n /2 width=5 by at_inv_npx/ +#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ] +#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj +#i2 #Hi * -j2 /2 width=3 by ex2_intro/ +qed-. + +lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → f@❴i1❵ = i2. +/2 width=6 by at_mono/ qed-. + +(* Spercific forward lemmas on at *******************************************) + +lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≡ i2 → i1 + n ≤ i2. +#f #n * +[ #i2 #H <(at_inv_O1 … H) -i2 // +| #i1 #i2 #H elim (at_inv_S1 … H) -H + #j1 #Ht * -i2 /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/ +] +qed-. + +lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≡ i → 0 = n. +#f #n #i #H elim (at_fwd_id_ex … H) -H +#g #H elim (push_inv_seq_dx … H) -H // +qed-. + +(* Basic properties *********************************************************) + +lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵). +#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H +elim (eq_inv_seq_aux … H) -H normalize // +#Hn #Hf /4 width=1 by eq_f2, eq_f/ +qed. + +lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵). +* #n #f * // +qed. + +(* Main inversion lemmas ****************************************************) + +lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 → + j1 = j2 → f1 ≗ f2 → i1 = i2. +/2 width=6 by at_inj/ 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 index dc462b3da..efb7b3810 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma @@ -29,23 +29,15 @@ interpretation "next (nstream)" 'Successor f = (next f). (* Basic properties *********************************************************) -lemma push_eq_repl: eq_stream_repl … (λf1,f2. ↑f1 ≐ ↑f2). -/2 width=1 by eq_seq/ qed. - -lemma next_eq_repl: eq_stream_repl … (λf1,f2. ⫯f1 ≐ ⫯f2). -* #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H -/2 width=1 by eq_seq/ -qed. - -lemma push_rew: ∀f. ↑f = 0@f. +lemma push_rew: ∀f. 0@f = ↑f. // qed. -lemma next_rew: ∀f,n. ⫯(n@f) = (⫯n)@f. +lemma next_rew: ∀f,n. (⫯n)@f = ⫯(n@f). // qed. - +(* lemma next_rew_sn: ∀f,n1,n2. n1 = ⫯n2 → n1@f = ⫯(n2@f). // qed. - +*) (* Basic inversion lemmas ***************************************************) lemma injective_push: injective ? ? push. @@ -64,50 +56,22 @@ lemma injective_next: injective ? ? next. * #n1 #f1 * #n2 #f2 normalize #H destruct // qed-. -lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → n = 0 ∧ g = f. -#f #g #n >push_rew #H destruct /2 width=1 by conj/ -qed-. - -lemma push_inv_seq_dx: ∀f,g,n. ↑f = n@g → n = 0 ∧ g = f. -#f #g #n >push_rew #H destruct /2 width=1 by conj/ -qed-. - -lemma next_inv_seq_sn: ∀f,g,n. n@g = ⫯f → ∃∃m. n = ⫯m & f = m@g. -* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/ -qed-. - -lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. n = ⫯m & f = m@g. -* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/ -qed-. - -lemma push_inv_dx: ∀x,f. x ≐ ↑f → ∃∃g. x = ↑g & g ≐ f. -* #m #x #f #H elim (eq_stream_inv_seq ????? H) -H -/2 width=3 by ex2_intro/ -qed-. - -lemma push_inv_sn: ∀f,x. ↑f ≐ x → ∃∃g. x = ↑g & f ≐ g. -#f #x #H lapply (eq_stream_sym … H) -H -#H elim (push_inv_dx … H) -H -/3 width=3 by eq_stream_sym, ex2_intro/ +lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → 0 = n ∧ g = f. +#f #g #n (injective_push … Hf) -g destruct /2 width=3 by ex2_intro/ +| #f #i1 #i2 #_ #g #j2 * #_ #x #x1 #_ #H elim (discr_push_next … H) +] +qed-. + +lemma at_inv_xnx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ⫯g = f → + ∃∃j2. @⦃i1, g⦄ ≡ j2 & ⫯j2 = i2. +#f #i1 #i2 * -f -i1 -i2 +[ #f #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H) +| #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H) +| #f #i1 #i2 #Hi #g #j2 * * #x #H >(injective_next … H) -g /2 width=3 by ex2_intro/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma at_inv_ppn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g,j2. 0 = i1 → ↑g = f → ⫯j2 = i2 → ⊥. +#f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2 +#H destruct +qed-. + +lemma at_inv_npn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g,j1,j2. ⫯j1 = i1 → ↑g = f → ⫯j2 = i2 → @⦃j1, g⦄ ≡ j2. +#f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1 +#x2 #Hg * -i2 #H destruct // +qed-. + +lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥. +#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1 +#x2 #Hg * -i2 #H destruct +qed-. + +lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g,j2. ⫯g = f → ⫯j2 = i2 → @⦃i1, g⦄ ≡ j2. +#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xnx … Hf … H) -f +#x2 #Hg * -i2 #H destruct // +qed-. + +lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = i2 → + ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f. +#f elim (pn_split … f) * +#g #H #i1 #i2 #Hf #j2 #H1 #H2 +[ elim (at_inv_ppn … Hf … H1 H H2) +| /3 width=5 by at_inv_xnn, ex2_intro/ +] +qed-. + +lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g. ⫯g = f → 0 = i2 → ⊥. +#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f +#x2 #Hg * -i2 #H destruct +qed-. + +lemma at_inv_nxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀j1. ⫯j1 = i1 → 0 = i2 → ⊥. +#f elim (pn_split f) * +#g #H #i1 #i2 #Hf #j1 #H1 #H2 +[ elim (at_inv_npp … Hf … H1 H H2) +| elim (at_inv_xnp … Hf … H H2) +] +qed-. + +lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1,j2. ⫯j1 = i1 → ⫯j2 = i2 → + (∃∃g. @⦃j1, g⦄ ≡ j2 & ↑g = f) ∨ + ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f. +#f elim (pn_split f) * +/4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/ +qed-. + +lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f → + (0 = i1 ∧ 0 = i2) ∨ + ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2. +#f * [2: #i1 ] #i2 #Hf #g #H +[ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/ +| >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/ +] +qed-. + +lemma at_inv_xpp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f → 0 = i2 → 0 = i1. +#f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * // +#j1 #j2 #_ #_ * -i2 #H destruct +qed-. + +lemma at_inv_xpn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j2. ↑g = f → ⫯j2 = i2 → + ∃∃j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1. +#f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xpx … Hf … H) -f * +[ #_ * -i2 #H destruct +| #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_xxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i2 → + ∃∃g. 0 = i1 & ↑g = f. +#f elim (pn_split f) * +#g #H #i1 #i2 #Hf #H2 +[ /3 width=6 by at_inv_xpp, ex2_intro/ +| elim (at_inv_xnp … Hf … H H2) +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma at_increasing: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2. +#i2 elim i2 -i2 +[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // +| #i2 #IH * // + #i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ] + /3 width=2 by le_S_S, le_S/ +] +qed-. + +lemma at_increasing_strict: ∀g,i1,i2. @⦃i1, g⦄ ≡ i2 → ∀f. ⫯f = g → + i1 < i2 ∧ @⦃i1, f⦄ ≡ ⫰i2. +#g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H +/4 width=2 by conj, at_increasing, le_S_S/ +qed-. + +lemma at_fwd_id_ex: ∀f,i. @⦃i, f⦄ ≡ i → ∃g. ↑g = f. +#f elim (pn_split f) * /2 width=2 by ex_intro/ +#g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H +#j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg +#H elim (lt_le_false … H) -H // +qed-. + +(* Basic properties *********************************************************) + +let corec at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2) ≝ ?. +#i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2 +[ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/ +| #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/ +| #f1 #i1 #i2 #Hf1 #g1 #j2 #H #H2 #f2 #H12 cases (eq_inv_nx … H12 … H) -g1 /3 width=5 by at_next/ +] +qed-. + +lemma at_eq_repl_fwd: ∀i1,i2. eq_repl_fwd (λf. @⦃i1, f⦄ ≡ i2). +#i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/ +qed-. + +lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1. +#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ] +#f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/ +qed-. + +(* Main properties **********************************************************) + +theorem at_monotonic: ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → + f1 ≗ f2 → i1 < i2 → j1 < j2. +#j2 elim j2 -j2 +[ #i2 #f2 #Hf2 elim (at_inv_xxp … Hf2) -Hf2 // + #g #H21 #_ #j1 #i1 #f1 #_ #_ #Hi elim (lt_le_false … Hi) -Hi // +| #j2 #IH #i2 #f2 #Hf2 * // + #j1 #i1 #f1 #Hf1 #Hf #Hi elim (lt_inv_gen … Hi) + #x2 #_ #H21 elim (at_inv_nxn … Hf2 … H21) -Hf2 [1,3: * |*: // ] + #g2 #Hg2 #H2 + [ elim (eq_inv_xp … Hf … H2) -f2 + #g1 #Hg #H1 elim (at_inv_xpn … Hf1 … H1) -f1 + /4 width=8 by lt_S_S_to_lt, lt_S_S/ + | elim (eq_inv_xn … Hf … H2) -f2 + /4 width=8 by at_inv_xnn, lt_S_S/ + ] +] +qed-. + +theorem at_inv_monotonic: ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → + f1 ≗ f2 → j1 < j2 → i1 < i2. +#j1 elim j1 -j1 +[ #i1 #f1 #Hf1 elim (at_inv_xxp … Hf1) -Hf1 // + #g1 * -i1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_O1 … Hj) -Hj + #x2 #H22 elim (eq_inv_px … Hf … H1) -f1 + #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 // +| #j1 #IH * + [ #f1 #Hf1 elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ] + #g1 #Hg1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj + elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/ + | #i1 #f1 #Hf1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj + #y2 #Hj #H22 elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ] + #g1 #Hg1 #H1 + [ elim (eq_inv_px … Hf … H1) -f1 + #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 -H22 + /3 width=7 by lt_S_S/ + | elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/ + ] + ] +] +qed-. + +theorem at_mono: ∀f1,f2. f1 ≗ f2 → ∀i,i1. @⦃i, f1⦄ ≡ i1 → ∀i2. @⦃i, f2⦄ ≡ i2 → i2 = i1. +#f1 #f2 #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_sym/ +qed-. + +theorem at_inj: ∀f1,f2. f1 ≗ f2 → ∀i1,i. @⦃i1, f1⦄ ≡ i → ∀i2. @⦃i2, f2⦄ ≡ i → i1 = i2. +#f1 #f2 #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_sym/ +qed-. + +(* Advanced inversion lemmas on isid ****************************************) + +lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i. +#i elim i -i +[ #f #H elim (isid_inv_gen … H) -H /2 width=2 by at_refl/ +| #i #IH #f #H elim (isid_inv_gen … H) -H /3 width=7 by at_push/ +] +qed. + +lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2. +/3 width=6 by isid_inv_at, at_mono/ qed-. + +(* Advancedd properties on isid *********************************************) + +let corec isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄ ≝ ?. +#f #Hf lapply (Hf 0) +#H cases (at_fwd_id_ex … H) -H +#g #H @(isid_push … H) /3 width=7 by at_inv_npn/ +qed-. + +(* Advanced properties on id ************************************************) + +lemma id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈𝐝 ≗ f. +/3 width=1 by isid_at, eq_id_inv_isid/ qed-. + +lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i. +/2 width=1 by isid_inv_at/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma new file mode 100644 index 000000000..44a83c7ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma @@ -0,0 +1,143 @@ +(**************************************************************************) +(* ___ *) +(* ||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/funexteq_2.ma". +include "ground_2/relocation/nstream_lift.ma". + +(* RELOCATION MAP ***********************************************************) + +coinductive eq: relation rtmap ≝ +| eq_push: ∀f1,f2,g1,g2. eq f1 f2 → ↑f1 = g1 → ↑f2 = g2 → eq g1 g2 +| eq_next: ∀f1,f2,g1,g2. eq f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → eq g1 g2 +. + +interpretation "extensional equivalence (rtmap)" + 'FunExtEq f1 f2 = (eq f1 f2). + +definition eq_repl (R:relation …) ≝ + ∀f1,f2. f1 ≗ f2 → R f1 f2. + +definition eq_repl_back (R:predicate …) ≝ + ∀f1. R f1 → ∀f2. f1 ≗ f2 → R f2. + +definition eq_repl_fwd (R:predicate …) ≝ + ∀f1. R f1 → ∀f2. f2 ≗ f1 → R f2. + +(* Basic properties *********************************************************) + +let corec eq_refl: reflexive … eq ≝ ?. +#f cases (pn_split f) * +#g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg // +qed. + +let corec eq_sym: symmetric … eq ≝ ?. +#f1 #f2 * -f1 -f2 +#f1 #f2 #g1 #g2 #Hf #H1 #H2 +[ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/ +qed-. + +lemma eq_repl_sym: ∀R. eq_repl_back R → eq_repl_fwd R. +/3 width=3 by eq_sym/ qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma eq_inv_px: ∀g1,g2. g1 ≗ g2 → ∀f1. ↑f1 = g1 → + ∃∃f2. f1 ≗ f2 & ↑f2 = g2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #Hf * * -g1 -g2 +#x1 #H +[ lapply (injective_push … H) -H /2 width=3 by ex2_intro/ +| elim (discr_push_next … H) +] +qed-. + +lemma eq_inv_nx: ∀g1,g2. g1 ≗ g2 → ∀f1. ⫯f1 = g1 → + ∃∃f2. f1 ≗ f2 & ⫯f2 = g2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #Hf * * -g1 -g2 +#x1 #H +[ elim (discr_next_push … H) +| lapply (injective_next … H) -H /2 width=3 by ex2_intro/ +] +qed-. + +lemma eq_inv_xp: ∀g1,g2. g1 ≗ g2 → ∀f2. ↑f2 = g2 → + ∃∃f1. f1 ≗ f2 & ↑f1 = g1. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #Hf * * -g1 -g2 +#x2 #H +[ lapply (injective_push … H) -H /2 width=3 by ex2_intro/ +| elim (discr_push_next … H) +] +qed-. + +lemma eq_inv_xn: ∀g1,g2. g1 ≗ g2 → ∀f2. ⫯f2 = g2 → + ∃∃f1. f1 ≗ f2 & ⫯f1 = g1. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #Hf * * -g1 -g2 +#x2 #H +[ elim (discr_next_push … H) +| lapply (injective_next … H) -H /2 width=3 by ex2_intro/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma eq_inv_pp: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≗ f2. +#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1 +#x2 #Hx2 * -g2 +#H lapply (injective_push … H) -H // +qed-. + +lemma eq_inv_nn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≗ f2. +#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1 +#x2 #Hx2 * -g2 +#H lapply (injective_next … H) -H // +qed-. + +lemma eq_inv_pn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥. +#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1 +#x2 #Hx2 * -g2 +#H elim (discr_next_push … H) +qed-. + +lemma eq_inv_np: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥. +#g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1 +#x2 #Hx2 * -g2 +#H elim (discr_push_next … H) +qed-. + +lemma eq_inv_gen: ∀f1,f2. f1 ≗ f2 → + (∃∃g1,g2. g1 ≗ g2 & ↑g1 = f1 & ↑g2 = f2) ∨ + ∃∃g1,g2. g1 ≗ g2 & ⫯g1 = f1 & ⫯g2 = f2. +#f1 elim (pn_split f1) * #g1 #H1 #f2 #Hf +[ elim (eq_inv_px … Hf … H1) -Hf /3 width=5 by or_introl, ex3_2_intro/ +| elim (eq_inv_nx … Hf … H1) -Hf /3 width=5 by or_intror, ex3_2_intro/ +] +qed-. + +(* Main properties **********************************************************) + +let corec eq_trans: Transitive … eq ≝ ?. +#f1 #f * -f1 -f +#f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2 +[ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g +/3 width=5 by eq_push, eq_next/ +qed-. + +theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2. +/3 width=3 by eq_trans, eq_sym/ qed-. + +theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2. +/3 width=3 by eq_trans, eq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma new file mode 100644 index 000000000..c08e32055 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nstream_id.ma". +include "ground_2/relocation/rtmap_isid.ma". + +(* RELOCATION MAP ***********************************************************) + +(* Basic properties *********************************************************) + +lemma id_isid: 𝐈⦃𝐈𝐝⦄. +/3 width=5 by eq_push_isid/ qed. + +(* Alternative definition of isid *******************************************) + +lemma eq_id_isid: ∀f. 𝐈𝐝 ≗ f → 𝐈⦃f⦄. +/2 width=3 by isid_eq_repl_back/ qed. + +lemma eq_id_inv_isid: ∀f. 𝐈⦃f⦄ → 𝐈𝐝 ≗ f. +/2 width=1 by isid_inv_eq_repl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma new file mode 100644 index 000000000..357f0fd20 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/isidentity_1.ma". +include "ground_2/relocation/rtmap_eq.ma". + +(* RELOCATION MAP ***********************************************************) + +coinductive isid: predicate rtmap ≝ +| isid_push: ∀f,g. isid f → ↑f = g → isid g +. + +interpretation "test for identity (rtmap)" + 'IsIdentity f = (isid f). + +(* Basic inversion lemmas ***************************************************) + +lemma isid_inv_gen: ∀g. 𝐈⦃g⦄ → ∃∃f. 𝐈⦃f⦄ & ↑f = g. +#g * -g +#f #g #Hf * /2 width=3 by ex2_intro/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma isid_inv_push: ∀g. 𝐈⦃g⦄ → ∀f. ↑f = g → 𝐈⦃f⦄. +#g #H elim (isid_inv_gen … H) -H +#f #Hf * -g #g #H >(injective_push … H) -H // +qed-. + +lemma isid_inv_next: ∀g. 𝐈⦃g⦄ → ∀f. ⫯f = g → ⊥. +#g #H elim (isid_inv_gen … H) -H +#f #Hf * -g #g #H elim (discr_next_push … H) +qed-. + +let corec isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2 ≝ ?. +#f1 #f2 #H1 #H2 +cases (isid_inv_gen … H1) -H1 +cases (isid_inv_gen … H2) -H2 +/3 width=5 by eq_push/ +qed-. + +(* Basic properties *********************************************************) + +let corec isid_eq_repl_back: eq_repl_back … isid ≝ ?. +#f1 #H cases (isid_inv_gen … H) -H +#g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_px … Hf … H1) -f1 +/3 width=3 by isid_push/ +qed-. + +lemma isid_eq_repl_fwd: eq_repl_fwd … isid. +/3 width=3 by isid_eq_repl_back, eq_repl_sym/ qed-. + +(* Alternative definition ***************************************************) + +let corec eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄ ≝ ?. +#f #H cases (eq_inv_px … H) -H /4 width=3 by isid_push, eq_trans/ +qed. + +let corec eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f ≝ ?. +#f * -f +#f #g #Hf #Hg @(eq_push … Hg) [2: @eq_push_inv_isid // | skip ] +@eq_f // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma new file mode 100644 index 000000000..85d70d4da --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||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/istotal_1.ma". +include "ground_2/relocation/rtmap_at.ma". + +(* RELOCATION MAP ***********************************************************) + +definition istot: predicate rtmap ≝ λf. ∀i. ∃j. @⦃i, f⦄ ≡ j. + +interpretation "test for totality (rtmap)" + 'IsTotal f = (istot f). + +(* Basic inversion lemmas ***************************************************) + +lemma istot_inv_push: ∀g. 𝐓⦃g⦄ → ∀f. ↑f = g → 𝐓⦃f⦄. +#g #Hg #f #H #i elim (Hg (⫯i)) -Hg +#j #Hg elim (at_inv_npx … Hg … H) -Hg -H /2 width=3 by ex_intro/ +qed-. + +lemma istot_inv_next: ∀g. 𝐓⦃g⦄ → ∀f. ⫯f = g → 𝐓⦃f⦄. +#g #Hg #f #H #i elim (Hg i) -Hg +#j #Hg elim (at_inv_xnx … Hg … H) -Hg -H /2 width=2 by ex_intro/ +qed-. + +(* Advanced forward lemmas on at ********************************************) + +let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ → + (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≗ f2 ≝ ?. +#f1 cases (pn_split f1) * #g1 #H1 +#f2 cases (pn_split f2) * #g2 #H2 +#Hf1 #Hf2 #Hi +[ @(eq_push … H1 H2) @at_ext -at_ext /2 width=3 by istot_inv_push/ -Hf1 -Hf2 + #i #i1 #i2 #Hg1 #Hg2 lapply (Hi (⫯i) (⫯i1) (⫯i2) ??) /2 width=7 by at_push/ +| cases (Hf2 0) -Hf1 -Hf2 -at_ext + #j2 #Hf2 cases (at_increasing_strict … Hf2 … H2) -H2 + lapply (Hi 0 0 j2 … Hf2) /2 width=2 by at_refl/ -Hi -Hf2 -H1 + #H2 #H cases (lt_le_false … H) -H // +| cases (Hf1 0) -Hf1 -Hf2 -at_ext + #j1 #Hf1 cases (at_increasing_strict … Hf1 … H1) -H1 + lapply (Hi 0 j1 0 Hf1 ?) /2 width=2 by at_refl/ -Hi -Hf1 -H2 + #H1 #H cases (lt_le_false … H) -H // +| @(eq_next … H1 H2) @at_ext -at_ext /2 width=3 by istot_inv_next/ -Hf1 -Hf2 + #i #i1 #i2 #Hg1 #Hg2 lapply (Hi i (⫯i1) (⫯i2) ??) /2 width=5 by at_next/ +] +qed-. + +(* Main properties on at ****************************************************) + +lemma at_dec: ∀f,i1,i2. 𝐓⦃f⦄ → Decidable (@⦃i1, f⦄ ≡ i2). +#f #i1 #i2 #Hf lapply (Hf i1) -Hf * +#j2 #Hf elim (eq_nat_dec i2 j2) +[ #H destruct /2 width=1 by or_introl/ +| /4 width=6 by at_mono, or_intror/ +] +qed-. + +lemma is_at_dec_le: ∀f,i2,i. 𝐓⦃f⦄ → (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, f⦄ ≡ i2). +#f #i2 #i #Hf elim i -i +[ #Ht @or_intror * /3 width=3 by at_increasing/ +| #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/ + #Hi2 @IH -IH #i1 #H #Hi elim (le_to_or_lt_eq … H) -H /2 width=3 by/ + #H destruct -Ht /2 width=1 by/ +] +qed-. + +lemma is_at_dec: ∀f,i2. 𝐓⦃f⦄ → Decidable (∃i1. @⦃i1, f⦄ ≡ i2). +#f #i2 #Hf @(is_at_dec_le ?? (⫯i2)) /2 width=4 by lt_le_false/ +qed-. + +(* Advanced properties on isid **********************************************) + +lemma isid_at_total: ∀f. 𝐓⦃f⦄ → (∀i1,i2. @⦃i1, f⦄ ≡ i2 → i1 = i2) → 𝐈⦃f⦄. +#f #H1f #H2f @isid_at +#i lapply (H1f i) -H1f * +#j #Hf >(H2f … Hf) in ⊢ (???%); -H2f // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma new file mode 100644 index 000000000..b27488644 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma @@ -0,0 +1,84 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/relocation/rtmap_isid.ma". + +(* RELOCATION MAP ***********************************************************) + +coinductive sle: relation rtmap ≝ +| sle_push: ∀f1,f2,g1,g2. sle f1 f2 → ↑f1 = g1 → ↑f2 = g2 → sle g1 g2 +| sle_next: ∀f1,f2,g1,g2. sle f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → sle g1 g2 +| sle_weak: ∀f1,f2,g1,g2. sle f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sle g1 g2 +. + +interpretation "inclusion (rtmap)" + 'subseteq t1 t2 = (sle t1 t2). + +(* Basic inversion lemmas ***************************************************) + +lemma sle_inv_xp: ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 → + ∃∃f1. f1 ⊆ f2 & ↑f1 = g1. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x2 #Hx2 destruct +[ lapply (injective_push … Hx2) -Hx2 /2 width=3 by ex2_intro/ ] +elim (discr_push_next … Hx2) +qed-. + +lemma sle_inv_nx: ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 → + ∃∃f2. f1 ⊆ f2 & ⫯f2 = g2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #Hx1 destruct +[2: lapply (injective_next … Hx1) -Hx1 /2 width=3 by ex2_intro/ ] +elim (discr_next_push … Hx1) +qed-. + +lemma sle_inv_pn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct +[ elim (discr_next_push … Hx2) +| elim (discr_push_next … Hx1) +| lapply (injective_push … Hx1) -Hx1 + lapply (injective_next … Hx2) -Hx2 // +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma sle_inv_pp: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ⊆ f2. +#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_xp … H … H2) -g2 +#x1 #H #Hx1 destruct lapply (injective_push … Hx1) -Hx1 // +qed-. + +lemma sle_inv_nn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2. +#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_nx … H … H1) -g1 +#x2 #H #Hx2 destruct lapply (injective_next … Hx2) -Hx2 // +qed-. + +(* properties on isid *******************************************************) + +let corec sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2 ≝ ?. +#f1 * -f1 +#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * +/3 width=5 by sle_weak, sle_push/ +qed. + +(* inversion lemmas on isid *************************************************) + +let corec sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1⦄ ≝ ?. +#f1 #f2 * -f1 -f2 +#f1 #f2 #g1 #g2 #Hf * * #H +[2,3: elim (isid_inv_next … H) // ] +lapply (isid_inv_push … H ??) -H +/3 width=3 by isid_push/ +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 bba1fcca1..b1b08518f 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,8 @@ table { class "grass" [ { "multiple relocation" * } { [ { "" * } { - [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ] + [ "rtmap_eq ( ? ≗ ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" * ] + [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ] [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]