From b9526dac808d40bf89dc378cf9c5ea0c121526a4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 2 Mar 2016 21:32:00 +0000 Subject: [PATCH] - second precommit for rtmap - we park relocation by streams of booleans --- .../ground_2/etc/relocation/rtmap_le.etc | 59 +++ .../trace.ma => etc/relocation/trace.etc} | 0 .../relocation/trace_after.etc} | 0 .../relocation/trace_at.etc} | 0 .../relocation/trace_isid.etc} | 0 .../relocation/trace_isun.etc} | 0 .../relocation/trace_sle.etc} | 0 .../relocation/trace_snot.etc} | 0 .../relocation/trace_sor.etc} | 0 .../ground_2/notation/functions/drop_1.ma | 19 + .../ground_2/relocation/nstream.ma | 70 +++ .../ground_2/relocation/nstream_istot.ma | 3 +- .../ground_2/relocation/nstream_lift.ma | 77 ---- .../lambdadelta/ground_2/relocation/rtmap.ma | 21 + .../ground_2/relocation/rtmap_after.ma | 404 ++++++++++++++++++ .../ground_2/relocation/rtmap_at.ma | 124 ++++-- .../ground_2/relocation/rtmap_eq.ma | 6 +- .../ground_2/relocation/rtmap_isid.ma | 2 +- .../ground_2/relocation/rtmap_istot.ma | 13 + .../ground_2/relocation/rtmap_minus.ma | 40 ++ .../ground_2/relocation/rtmap_tl.ma | 41 ++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 4 +- 22 files changed, 757 insertions(+), 126 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace.ma => etc/relocation/trace.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_after.ma => etc/relocation/trace_after.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_at.ma => etc/relocation/trace_at.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_isid.ma => etc/relocation/trace_isid.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_isun.ma => etc/relocation/trace_isun.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_sle.ma => etc/relocation/trace_sle.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_snot.ma => etc/relocation/trace_snot.etc} (100%) rename matita/matita/contribs/lambdadelta/ground_2/{relocation/trace_sor.ma => etc/relocation/trace_sor.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/drop_1.ma delete mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc new file mode 100644 index 000000000..6fe63a523 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tl.ma". + +(* RELOCATION MAP ***********************************************************) + +inductive le (f1): predicate rtmap ≝ +| le_eq: ∀f2. f1 ≗ f2 → le f1 f2 +| le_tl: ∀f2,g2. le f1 f2 → ↓g2 = f2 → le f1 g2 +. + +interpretation "less or equal to (rtmap)" 'leq x y = (le x y). + +(* Basic properties *********************************************************) + +lemma le_refl: reflexive … le. +/2 width=1 by eq_refl, le_eq/ qed. + +lemma le_eq_repl_back_dx: ∀f1. eq_repl_back (λf2. f1 ≤ f2). +#f #f1 #Hf1 elim Hf1 -f1 +/4 width=3 by le_tl, le_eq, tl_eq_repl, eq_trans/ +qed-. + +lemma le_eq_repl_fwd_dx: ∀f1. eq_repl_fwd (λf2. f1 ≤ f2). +#f1 @eq_repl_sym /2 width=3 by le_eq_repl_back_dx/ +qed-. + +lemma le_eq_repl_back_sn: ∀f2. eq_repl_back (λf1. f1 ≤ f2). +#f #f1 #Hf1 elim Hf1 -f +/4 width=3 by le_tl, le_eq, tl_eq_repl, eq_canc_sn/ +qed-. + +lemma le_eq_repl_fwd_sn: ∀f2. eq_repl_fwd (λf1. f1 ≤ f2). +#f2 @eq_repl_sym /2 width=3 by le_eq_repl_back_sn/ +qed-. + +lemma le_tl_comp: ∀f1,f2. f1 ≤ f2 → ∀g1,g2. ↓f1 = g1 → ↓f2 = g2 → g1 ≤ g2. +#f1 #f2 #H elim H -f2 +/3 width=3 by le_tl, le_eq, tl_eq_repl/ +qed. + +(* Main properties **********************************************************) + +theorem le_trans: Transitive … le. +#f1 #f #H elim H -f +/4 width=5 by le_tl_comp, le_eq_repl_fwd_sn, le_tl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_after.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_after.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_at.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_at.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isid.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isid.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isun.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isun.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sle.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sle.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_snot.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_snot.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sor.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma rename to matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sor.etc diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drop_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drop_1.ma new file mode 100644 index 000000000..1cc9141bb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drop_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 @{ 'Drop $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma index 7ba0d13eb..aaa1ba9b6 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma @@ -12,9 +12,79 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/lift_1.ma". include "ground_2/lib/arith.ma". include "ground_2/lib/streams.ma". (* RELOCATION N-STREAM ******************************************************) definition rtmap: Type[0] ≝ stream nat. + +definition push: rtmap → rtmap ≝ λf. 0@f. + +interpretation "push (nstream)" 'Lift f = (push f). + +definition next: rtmap → rtmap. +* #n #f @(⫯n@f) +qed. + +interpretation "next (nstream)" 'Successor f = (next f). + +(* Basic properties *********************************************************) + +lemma push_rew: ∀f. 0@f = ↑f. +// qed. + +lemma next_rew: ∀f,n. (⫯n)@f = ⫯(n@f). +// qed. + +(* Basic inversion lemmas ***************************************************) + +lemma injective_push: injective ? ? push. +#f1 #f2 normalize #H destruct // +qed-. + +lemma discr_push_next: ∀f1,f2. ↑f1 = ⫯f2 → ⊥. +#f1 * #n2 #f2 normalize #H destruct +qed-. + +lemma discr_next_push: ∀f1,f2. ⫯f1 = ↑f2 → ⊥. +* #n1 #f1 #f2 normalize #H destruct +qed-. + +lemma injective_next: injective ? ? next. +* #n1 #f1 * #n2 #f2 normalize #H destruct // +qed-. + +lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → 0 = n ∧ g = f. +#f #g #n (injective_push … Hx1) >(injective_push … Hx2) -x2 -x1 + /2 width=3 by ex2_intro/ +| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct + elim (discr_push_next … Hx2) +| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct + elim (discr_push_next … Hx1) +] +qed-. + +lemma after_inv_pnx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → + ∃∃f. f1 ⊚ f2 ≡ f & ⫯f = g. +#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1 +[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct + elim (discr_next_push … Hx2) +| #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct + >(injective_push … Hx1) >(injective_next … Hx2) -x2 -x1 + /2 width=3 by ex2_intro/ +| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct + elim (discr_push_next … Hx1) +] +qed-. + +lemma after_inv_nxx: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. ⫯f1 = g1 → + ∃∃f. f1 ⊚ f2 ≡ f & ⫯f = g. +#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1 +[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct + elim (discr_next_push … Hx1) +| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct + elim (discr_next_push … Hx1) +| #g #Hf #H1 #H #x1 #Hx1 destruct + >(injective_next … Hx1) -x1 + /2 width=3 by ex2_intro/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma after_inv_ppp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⊚ f2 ≡ f. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_ppx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct <(injective_push … Hx) -f // +qed-. + +lemma after_inv_ppn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_ppx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct elim (discr_push_next … Hx) +qed-. + +lemma after_inv_pnn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⊚ f2 ≡ f. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_pnx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct <(injective_next … Hx) -f // +qed-. + +lemma after_inv_pnp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_pnx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct elim (discr_next_push … Hx) +qed-. + +lemma after_inv_nxn: ∀g1,f2,g. g1 ⊚ f2 ≡ g → + ∀f1,f. ⫯f1 = g1 → ⫯f = g → f1 ⊚ f2 ≡ f. +#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_nxx … Hg … H1) -g1 +#x #Hf #Hx destruct <(injective_next … Hx) -f // +qed-. + +lemma after_inv_nxp: ∀g1,f2,g. g1 ⊚ f2 ≡ g → + ∀f1,f. ⫯f1 = g1 → ↑f = g → ⊥. +#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_nxx … Hg … H1) -g1 +#x #Hf #Hx destruct elim (discr_next_push … Hx) +qed-. + +lemma after_inv_pxp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f. ↑f1 = g1 → ↑f = g → + ∃∃f2. f1 ⊚ f2 ≡ f & ↑f2 = g2. +#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H +[ elim (after_inv_pnp … Hg … H1 … H) -g1 -g -f1 -f // +| lapply (after_inv_ppp … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ +] +qed-. + +lemma after_inv_pxn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f. ↑f1 = g1 → ⫯f = g → + ∃∃f2. f1 ⊚ f2 ≡ f & ⫯f2 = g2. +#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H +[ lapply (after_inv_pnn … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ +| elim (after_inv_ppn … Hg … H1 … H) -g1 -g -f1 -f // +] +qed-. + +lemma after_inv_xxp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. ↑f = g → + ∃∃f1,f2. f1 ⊚ f2 ≡ f & ↑f1 = g1 & ↑f2 = g2. +* * [2: #m1 ] #g1 #g2 #g #Hg #f #H +[ elim (after_inv_nxp … Hg … H) -g2 -g -f // +| elim (after_inv_pxp … Hg … H) -g /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma after_inv_xxn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. ⫯f = g → + (∃∃f1,f2. f1 ⊚ f2 ≡ f & ↑f1 = g1 & ⫯f2 = g2) ∨ + ∃∃f1. f1 ⊚ g2 ≡ f & ⫯f1 = g1. +* * [2: #m1 ] #g1 #g2 #g #Hg #f #H +[ /4 width=5 by after_inv_nxn, or_intror, ex2_intro/ +| elim (after_inv_pxn … Hg … H) -g + /3 width=5 by or_introl, ex3_2_intro/ +] +qed-. + +lemma after_inv_pxx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. ↑f1 = g1 → + (∃∃f2,f. f1 ⊚ f2 ≡ f & ↑f2 = g2 & ↑f = g) ∨ + (∃∃f2,f. f1 ⊚ f2 ≡ f & ⫯f2 = g2 & ⫯f = g). +#g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H +[ elim (after_inv_pnx … Hg … H) -g1 + /3 width=5 by or_intror, ex3_2_intro/ +| elim (after_inv_ppx … Hg … H) -g1 + /3 width=5 by or_introl, ex3_2_intro/ +] +qed-. + +(* Main properties **********************************************************) + +let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → + ∀f1,f2. f1 ⊚ f2 ≡ f0 → + ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?. +#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4 +[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg + cases (after_inv_xxp … Hg0 … H0) -g0 + #f1 #f2 #Hf0 #H1 #H2 + cases (after_inv_ppx … Hg … H2 H3) -g2 -g3 + #f #Hf #H /3 width=7 by after_refl/ +| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg + cases (after_inv_xxp … Hg0 … H0) -g0 + #f1 #f2 #Hf0 #H1 #H2 + cases (after_inv_pnx … Hg … H2 H3) -g2 -g3 + #f #Hf #H /3 width=7 by after_push/ +| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg + cases (after_inv_xxn … Hg0 … H0) -g0 * + [ #f1 #f2 #Hf0 #H1 #H2 + cases (after_inv_nxx … Hg … H2) -g2 + #f #Hf #H /3 width=7 by after_push/ + | #f1 #Hf0 #H1 /3 width=6 by after_next/ + ] +] +qed-. + +let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 → + ∀f2, f3. f2 ⊚ f3 ≡ f0 → + ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?. +#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4 +[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg + cases (after_inv_xxp … Hg0 … H0) -g0 + #f2 #f3 #Hf0 #H2 #H3 + cases (after_inv_ppx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=7 by after_refl/ +| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg + cases (after_inv_xxn … Hg0 … H0) -g0 * + [ #f2 #f3 #Hf0 #H2 #H3 + cases (after_inv_ppx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=7 by after_push/ + | #f2 #Hf0 #H2 + cases (after_inv_pnx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=6 by after_next/ + ] +| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg + cases (after_inv_nxx … Hg … H1) -g1 + #f #Hg #H /3 width=6 by after_next/ +] +qed-. + +(* Main inversion lemmas on after *******************************************) + +let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y ≝ ?. +#f1 #f2 #x #y * -f1 -f2 -x +#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy +[ cases (after_inv_ppx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_push/ +| cases (after_inv_pnx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_next/ +| cases (after_inv_nxx … Hy … H1) -g1 /3 width=8 by eq_next/ +] +qed-. + +(* Properties on minus ******************************************************) + +lemma after_minus: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → + f1 ⊚ f2 ≡ f → f1-n ⊚ f2 ≡ f-n. +#n elim n -n // +#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] +#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/ +qed. + +(* Inversion lemmas on isid *************************************************) + +let corec isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2 ≝ ?. +#f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2 +/3 width=7 by after_push, after_refl/ +qed-. + +let corec isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1 ≝ ?. +#f2 * -f2 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * #g1 #H1 +[ /3 width=7 by after_refl/ +| @(after_next … H1 H1) /3 width=3 by isid_push/ +] +qed-. + +lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f. +/3 width=6 by isid_after_sn, after_mono/ +qed-. + +lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≗ f. +/3 width=6 by isid_after_dx, after_mono/ +qed-. + +let corec after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ≝ ?. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H +[ /4 width=6 by isid_inv_push, isid_push/ ] +cases (isid_inv_next … H … H0) +qed-. + +let corec after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄ ≝ ?. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H +[ /4 width=6 by isid_inv_push, isid_push/ ] +cases (isid_inv_next … H … H0) +qed-. + +lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄. +/3 width=4 by after_fwd_isid2, after_fwd_isid1, conj/ qed-. + +(* Forward lemmas on at *****************************************************) + +lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f → + ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i. +#i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21 +[ elim (at_inv_xxn … Hf) -Hf [1,3:* |*: // ] + [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ] +| elim (at_inv_xxp … Hf) -Hf // + #g #H1 #H +] +[2: elim (after_inv_xxn … Hf21 … H) -f * + [ #g2 #g1 #Hg21 #H2 #H1 | #g2 #Hg21 #H2 ] +|*: elim (after_inv_xxp … Hf21 … H) -f + #g2 #g1 #Hg21 #H2 #H1 +] +[4: -Hg21 |*: elim (IH … Hg … Hg21) -g -IH ] +/3 width=9 by at_refl, at_push, at_next, ex2_intro/ +qed-. + +lemma after_fwd_at: ∀i,i2,i1,f1,f2. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i → + ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i. +#i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf +[ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ] + #g2 [ #j2 ] #Hg2 [ #H22 ] #H20 + [ elim (at_inv_xxn … Hf1 … H22) -i2 * + #g1 [ #j1 ] #Hg1 [ #H11 ] #H10 + [ elim (after_inv_ppx … Hf … H20 H10) -f1 -f2 /3 width=7 by at_push/ + | elim (after_inv_pnx … Hf … H20 H10) -f1 -f2 /3 width=6 by at_next/ + ] + | elim (after_inv_nxx … Hf … H20) -f2 /3 width=7 by at_next/ + ] +| elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H22 #H20 + elim (at_inv_xxp … Hf1 … H22) -i2 #g1 #H11 #H10 + elim (after_inv_ppx … Hf … H20 H10) -f1 -f2 /2 width=2 by at_refl/ +] +qed-. + +lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 → + ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i. +#f #i1 #i #Hf #f1 #i2 #Hf1 #f2 #H elim (after_at_fwd … Hf … H) -f +#j1 #H #Hf2 <(at_mono … Hf1 … H) -i1 -i2 // +qed-. + +lemma after_fwd_at1: ∀i,i2,i1,f,f2. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i → + ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2. +#i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1 +[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] + #g [ #j1 ] #Hg [ #H01 ] #H00 + elim (at_inv_xxn … Hf2) -Hf2 [1,3,5,7: * |*: // ] + #g2 [1,3: #j2 ] #Hg2 [1,2: #H22 ] #H20 + [ elim (after_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=7 by at_push/ + | elim (after_inv_pxn … Hf1 … H20 H00) -f2 -f /3 width=5 by at_next/ + | elim (after_inv_nxp … Hf1 … H20 H00) + | /4 width=9 by after_inv_nxn, at_next/ + ] +| elim (at_inv_xxp … Hf) -Hf // #g #H01 #H00 + elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H21 #H20 + elim (after_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=2 by at_refl/ +] +qed-. + +(* Forward lemmas on istot **************************************************) + +lemma after_istot_fwd: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f2⦄ → 𝐓⦃f1⦄ → 𝐓⦃f⦄. +#f2 #f1 #f #Hf #Hf2 #Hf1 #i1 elim (Hf1 i1) -Hf1 +#i2 #Hf1 elim (Hf2 i2) -Hf2 +/3 width=7 by after_fwd_at, ex_intro/ +qed-. + +lemma after_fwd_istot_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f1⦄. +#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf +#i2 #Hf elim (after_at_fwd … Hf … H) -f /2 width=2 by ex_intro/ +qed-. + +lemma after_fwd_istot_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f2⦄. +#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf +#i #Hf elim (after_at_fwd … Hf … H) -f +#i2 #Hf1 #Hf2 lapply (at_increasing … Hf1) -f1 +#Hi12 elim (at_le_ex … Hf2 … Hi12) -i2 /2 width=2 by ex_intro/ +qed-. + +lemma after_inv_istot: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f2⦄ ∧ 𝐓⦃f1⦄. +/3 width=4 by after_fwd_istot_sn, after_fwd_istot_dx, conj/ qed-. + +lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2. 𝐓⦃f2⦄ → ∀f. f2 ⊚ f1 ≡ f → + ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i. +#f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2 +/3 width=8 by after_fwd_at, ex2_intro/ +qed-. + +lemma after_fwd_isid_sn: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f1 ≗ f → 𝐈⦃f2⦄. +#f2 #f1 #f #H #Hf elim (after_inv_istot … Hf H) -H +#Hf2 #Hf1 #H @isid_at_total // -Hf2 +#i2 #i #Hf2 elim (Hf1 i2) -Hf1 +#i0 #Hf1 lapply (at_increasing … Hf1) +#Hi20 lapply (after_fwd_at2 … i0 … Hf1 … Hf) -Hf +/3 width=7 by at_eq_repl_back, at_mono, at_id_le/ +qed-. + +lemma after_fwd_isid_dx: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f2 ≗ f → 𝐈⦃f1⦄. +#f2 #f1 #f #H #Hf elim (after_inv_istot … Hf H) -H +#Hf2 #Hf1 #H2 @isid_at_total // -Hf1 +#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Hf) -f1 +/3 width=8 by at_inj, at_eq_repl_back/ +qed-. + +let corec after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1 ≝ ?. +#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f +cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1 +lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1 +cases (H2g1 0) #n #Hn +cases (after_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H +[ cases (after_inv_pxp … H2f … H1 H) -f1 -f #g22 #H2g #H22 + @(eq_push … H21 H22) -f21 -f22 +| cases (after_inv_pxn … H2f … H1 H) -f1 -f #g22 #H2g #H22 + @(eq_next … H21 H22) -f21 -f22 +] +@(after_inj_O_aux (g1-n) … (g-n)) -after_inj_O_aux +/2 width=1 by after_minus, istot_minus, at_pxx_minus/ +qed-. + +fact after_inj_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1) → + ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_after_inj f1. +#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0 +#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f +elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1 +elim (after_inv_nxx … H1f … H1) -H1f #g #H1g #H +lapply (after_inv_nxn … H2f … H1 H) -f #H2g +/3 width=6 by istot_inv_next/ +qed-. + +theorem after_inj: ∀f1. H_after_inj f1. +#f1 #H cases (H 0) /3 width=7 by after_inj_aux, after_inj_O_aux/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma index f6377be85..3bc16b8ec 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma @@ -61,15 +61,21 @@ lemma at_inv_ppn: ∀f,i1,i2. @⦃i1, f⦄ ≡ 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_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 +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-. @@ -79,6 +85,13 @@ lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → #x2 #Hg * -i2 #H destruct // qed-. +(* --------------------------------------------------------------------------*) + +lemma at_inv_pxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i1 → 0 = i2 → ∃g. ↑g = f. +#f elim (pn_split … f) * /2 width=2 by ex_intro/ +#g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2) +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) * @@ -88,12 +101,6 @@ lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = ] 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) * @@ -110,6 +117,8 @@ lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1,j2. ⫯j1 = i1 → /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. @@ -141,6 +150,16 @@ lemma at_inv_xxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i2 → ] qed-. +lemma at_inv_xxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. ⫯j2 = i2 → + (∃∃g,j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ↑g = f) ∨ + ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f. +#f elim (pn_split f) * +#g #H #i1 #i2 #Hf #j2 #H2 +[ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/ +| lapply (at_inv_xnn … Hf … H H2) -i2 /3 width=3 by or_intror, ex2_intro/ +] +qed-. + (* Basic forward lemmas *****************************************************) lemma at_increasing: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2. @@ -179,6 +198,24 @@ 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_le_ex: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀i1. i1 ≤ i2 → + ∃∃j1. @⦃i1, f⦄ ≡ j1 & j1 ≤ j2. +#j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf +[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] + #g [ #x2 ] #Hg [ #H2 ] #H0 + [ * /3 width=3 by at_refl, ex2_intro/ + #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12 + #Hi12 elim (IH … Hg … Hi12) -x2 -IH + /3 width=7 by at_push, ex2_intro, le_S_S/ + | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2 + /3 width=5 by at_next, ex2_intro, le_S_S/ + ] +| elim (at_inv_xxp … Hf) -Hf // + #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12) + /3 width=3 by at_refl, ex2_intro/ +] +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/ @@ -186,57 +223,60 @@ qed-. (* Main properties **********************************************************) -theorem at_monotonic: ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → - f1 ≗ f2 → i1 < i2 → j1 < j2. +theorem at_monotonic: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀j1,i1. @⦃i1, f⦄ ≡ j1 → + 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 +[ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f // + #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi // +| #j2 #IH #i2 #f #H2f * // + #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi) + #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ] + #g #H2g #H + [ elim (at_inv_xpn … H1f … H) -f /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/ + | /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. +theorem at_inv_monotonic: ∀j1,i1,f. @⦃i1, f⦄ ≡ j1 → ∀j2,i2. @⦃i2, f⦄ ≡ j2 → + 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 // +[ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f // + #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj + #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f // | #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 + [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ] + #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj + /3 width=7 by at_inv_xnn/ + | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj + #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ] + #g #Hg #H + [ elim (at_inv_xpn … H2f … H H22) -f -H22 /3 width=7 by lt_S_S/ - | elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/ + | /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/ +theorem at_mono: ∀f,i,i1. @⦃i, f⦄ ≡ i1 → ∀i2. @⦃i, f⦄ ≡ i2 → i2 = i1. +#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /3 width=6 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/ +theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i → i1 = i2. +#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/ qed-. +(* Properties on minus ******************************************************) + +lemma at_pxx_minus: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, f-n⦄ ≡ 0. +#n elim n -n // +#n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/ +qed. + (* Advanced inversion lemmas on isid ****************************************) lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma index 44a83c7ff..4430c2f8a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/relations/funexteq_2.ma". -include "ground_2/relocation/nstream_lift.ma". +include "ground_2/relocation/rtmap.ma". (* RELOCATION MAP ***********************************************************) @@ -136,8 +136,8 @@ let corec eq_trans: Transitive … eq ≝ ?. /3 width=5 by eq_push, eq_next/ qed-. -theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2. +theorem eq_canc_sn: ∀f2. eq_repl_back (λf. f ≗ f2). /3 width=3 by eq_trans, eq_sym/ qed-. -theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2. +theorem eq_canc_dx: ∀f1. eq_repl_fwd (λf. f1 ≗ f). /3 width=3 by eq_trans, eq_sym/ 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 index 357f0fd20..cfe2b3771 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/relations/isidentity_1.ma". -include "ground_2/relocation/rtmap_eq.ma". +include "ground_2/relocation/rtmap_minus.ma". (* RELOCATION MAP ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma index 85d70d4da..07b24f973 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma @@ -34,6 +34,19 @@ lemma istot_inv_next: ∀g. 𝐓⦃g⦄ → ∀f. ⫯f = g → 𝐓⦃f⦄. #j #Hg elim (at_inv_xnx … Hg … H) -Hg -H /2 width=2 by ex_intro/ qed-. +(* Properties on tl *********************************************************) + +lemma istot_tl: ∀f. 𝐓⦃f⦄ → 𝐓⦃↓f⦄. +#f cases (pn_split f) * +#g * -f /2 width=3 by istot_inv_next, istot_inv_push/ +qed. + +(* Properties on minus ******************************************************) + +lemma istot_minus: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃f-n⦄. +#n elim n -n /3 width=1 by istot_tl/ +qed. + (* Advanced forward lemmas on at ********************************************) let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ → diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma new file mode 100644 index 000000000..91f2c8479 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.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/relocation/rtmap_tl.ma". + +(* RELOCATION MAP ***********************************************************) + +let rec minus (f:rtmap) (n:nat) on n: rtmap ≝ match n with +[ O ⇒ f | S m ⇒ ↓(minus f m) ]. + +interpretation "minus (rtmap)" 'minus f n = (minus f n). + +(* Basic properties *********************************************************) + +lemma minus_rew_O: ∀f. f = f - 0. +// qed. + +lemma minus_rew_S: ∀f,n. ↓(f - n) = f - ⫯n. +// qed. + +lemma minus_eq_repl: ∀n. eq_repl (λf1,f2. f1 - n ≗ f2 - n). +#n elim n -n /3 width=1 by tl_eq_repl/ +qed. + +(* Advancedd properties *****************************************************) + +lemma minus_xn: ∀n,f. (↓f) - n = f - ⫯n. +#n elim n -n // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma new file mode 100644 index 000000000..779cc4f6f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.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/drop_1.ma". +include "ground_2/relocation/rtmap_eq.ma". + +(* RELOCATION MAP ***********************************************************) + +definition tl: rtmap → rtmap. +@case_type0 #f @f +defined. + +interpretation "tail (rtmap)" 'Drop f = (tl f). + +(* Basic properties *********************************************************) + +lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ↓f. +// qed. + +lemma tl_push_rew: ∀f. f = ↓↑f. +#f