From ff1cd6f29b3aaef01e4674544d399f44949c5738 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 21 Mar 2016 19:36:29 +0000 Subject: [PATCH] rtmaps with finite colength --- .../lambdadelta/ground_2/lib/arith.ma | 21 ++++++ .../ground_2/notation/relations/isfinite_1.ma | 19 +++++ .../notation/relations/rcolength_2.ma | 19 +++++ .../ground_2/relocation/rtmap_fcla.ma | 71 +++++++++++++++++++ .../ground_2/relocation/rtmap_isfin.ma | 67 +++++++++++++++++ .../ground_2/relocation/rtmap_sor.ma | 60 ++++++++++++++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 6 +- 7 files changed, 260 insertions(+), 3 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/isfinite_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcolength_2.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 1ba525475..d70ea1bfa 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -23,6 +23,10 @@ interpretation "nat successor" 'Successor m = (S m). interpretation "nat predecessor" 'Predecessor m = (pred m). +interpretation "nat min" 'and x y = (min x y). + +interpretation "nat max" 'or x y = (max x y). + (* Iota equations ***********************************************************) lemma pred_O: pred 0 = 0. @@ -31,6 +35,17 @@ normalize // qed. lemma pred_S: ∀m. pred (S m) = m. // qed. +lemma max_O1: ∀n. n = (0 ∨ n). +// qed. + +lemma max_O2: ∀n. n = (n ∨ 0). +// qed. + +lemma max_SS: ∀n1,n2. ⫯(n1∨n2) = (⫯n1 ∨ ⫯n2). +#n1 #n2 elim (decidable_le n1 n2) #H normalize +[ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H // +qed. + (* Equations ****************************************************************) lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. @@ -112,6 +127,12 @@ lemma lt_S_S: ∀x,y. x < y → ⫯x < ⫯y. lemma lt_S: ∀n,m. n < m → n < ⫯m. /2 width=1 by le_S/ qed. +lemma max_S1_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (⫯n1 ∨ n2) ≤ ⫯n. +/4 width=2 by to_max, le_maxr, le_S_S, le_S/ qed-. + +lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ⫯n2) ≤ ⫯n. +/2 width=1 by max_S1_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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isfinite_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isfinite_1.ma new file mode 100644 index 000000000..eb6eec16f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isfinite_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 @{ 'IsFinite $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcolength_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcolength_2.ma new file mode 100644 index 000000000..f60b379c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcolength_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( 𝐂 ⦃ term 46 f ⦄ ≡ break term 46 n )" + non associative with precedence 45 + for @{ 'RCoLength $f $n }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma new file mode 100644 index 000000000..14542cf48 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/relations/rcolength_2.ma". +include "ground_2/relocation/rtmap_isid.ma". + +(* RELOCATION MAP ***********************************************************) + +inductive fcla: relation2 rtmap nat ≝ +| fcla_isid: ∀f. 𝐈⦃f⦄ → fcla f 0 +| fcla_push: ∀f,n. fcla f n → fcla (↑f) n +| fcla_next: ∀f,n. fcla f n → fcla (⫯f) (⫯n) +. + +interpretation "finite colength assignment (rtmap)" + 'RCoLength f n = (fcla f n). + +(* Basic inversion lemmas ***************************************************) + +lemma fcla_inv_px: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f. ↑f = g → 𝐂⦃f⦄ ≡ m. +#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/ +#g #m #_ #f #H elim (discr_push_next … H) +qed-. + +lemma fcla_inv_nx: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f. ⫯f = g → + ∃∃n. 𝐂⦃f⦄ ≡ n & ⫯n = m. +#g #m * -g -m /2 width=3 by ex2_intro/ +[ #g #Hg #f #H elim (isid_inv_next … H) -H // +| #g #m #_ #f #H elim (discr_next_push … H) +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma cla_inv_nn: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f,n. ⫯f = g → ⫯n = m → 𝐂⦃f⦄ ≡ n. +#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx … H … H1) -g +#x #Hf #H destruct // +qed-. + +lemma cla_inv_np: ∀g,m. 𝐂⦃g⦄ ≡ m → ∀f. ⫯f = g → 0 = m → ⊥. +#g #m #H #f #H1 elim (fcla_inv_nx … H … H1) -g +#x #_ #H1 #H2 destruct +qed-. + +lemma fcla_inv_xp: ∀g,m. 𝐂⦃g⦄ ≡ m → 0 = m → 𝐈⦃g⦄. +#g #m #H elim H -g -m /3 width=3 by isid_push/ +#g #m #_ #_ #H destruct +qed-. + +(* Basic properties *********************************************************) + +lemma fcla_eq_repl_back: ∀n. eq_repl_back … (λf. 𝐂⦃f⦄ ≡ n). +#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/ +#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px … H) | elim (eq_inv_nx … H) ] -H +/3 width=3 by fcla_push, fcla_next/ +qed-. + +lemma fcla_eq_repl_fwd: ∀n. eq_repl_fwd … (λf. 𝐂⦃f⦄ ≡ n). +#n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma new file mode 100644 index 000000000..45c8ea854 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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/isfinite_1.ma". +include "ground_2/relocation/rtmap_fcla.ma". + +(* RELOCATION MAP ***********************************************************) + +definition isfin: predicate rtmap ≝ + λf. ∃n. 𝐂⦃f⦄ ≡ n. + +interpretation "test for finite colength (rtmap)" + 'IsFinite f = (isfin f). + +(* Basic properties *********************************************************) + +lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄. +/3 width=2 by fcla_isid, ex_intro/ qed. + +lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄. +#f * /3 width=2 by fcla_push, ex_intro/ +qed. + +lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄. +#f * /3 width=2 by fcla_next, ex_intro/ +qed. + +lemma isfin_eq_repl_back: eq_repl_back … isfin. +#f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/ +qed-. + +lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin. +/3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-. + +(* Basic eliminators ********************************************************) + +lemma isfin_ind (R:predicate rtmap): (∀f. 𝐈⦃f⦄ → R f) → + (∀f. 𝐅⦃f⦄ → R f → R (↑f)) → + (∀f. 𝐅⦃f⦄ → R f → R (⫯f)) → + ∀f. 𝐅⦃f⦄ → R f. +#R #IH1 #IH2 #IH3 #f #H elim H -H +#n #H elim H -f -n /3 width=2 by ex_intro/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma isfin_inv_next: ∀g. 𝐅⦃g⦄ → ∀f. ⫯f = g → 𝐅⦃f⦄. +#g * #n #H #f #H0 elim (fcla_inv_nx … H … H0) -g +/2 width=2 by ex_intro/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma isfin_fwd_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄. +#g * /3 width=4 by fcla_inv_px, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma index 0bc38867e..b93214bea 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground_2/notation/relations/runion_3.ma". +include "ground_2/relocation/rtmap_isfin.ma". include "ground_2/relocation/rtmap_sle.ma". coinductive sor: relation3 rtmap rtmap rtmap ≝ @@ -71,6 +72,19 @@ try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) /2 width=3 by ex2_intro/ qed-. +(* Main inversion lemmas ****************************************************) + +corec theorem sor_mono: ∀f1,f2,x,y. f1 ⋓ f2 ≡ x → f1 ⋓ f2 ≡ y → x ≗ y. +#f1 #f2 #x #y * -f1 -f2 -x +#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H +[ cases (sor_inv_ppx … H … H1 H2) +| cases (sor_inv_npx … H … H1 H2) +| cases (sor_inv_pnx … H … H1 H2) +| cases (sor_inv_nnx … H … H1 H2) +] -g1 -g2 +/3 width=5 by eq_push, eq_next/ +qed-. + (* Basic properties *********************************************************) corec lemma sor_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋓ f2 ≡ f). @@ -116,3 +130,49 @@ corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f. #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/ qed-. + +(* Properies on identity ****************************************************) + +corec lemma sor_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⋓ f2 ≡ f2. +#f1 * -f1 +#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * +/3 width=7 by sor_pp, sor_pn/ +qed. + +corec lemma sor_isid_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⋓ f2 ≡ f1. +#f2 * -f2 +#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * +/3 width=7 by sor_pp, sor_np/ +qed. + +(* Properties on finite colength assignment *********************************) + +lemma sor_fcla_ex: ∀f1,n1. 𝐂⦃f1⦄ ≡ n1 → ∀f2,n2. 𝐂⦃f2⦄ ≡ n2 → + ∃∃f,n. f1 ⋓ f2 ≡ f & 𝐂⦃f⦄ ≡ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2. +#f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by sor_isid_sn, ex4_2_intro/ +#f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by fcla_push, fcla_next, ex4_2_intro, sor_isid_dx/ +#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 +[ /3 width=7 by fcla_push, sor_pp, ex4_2_intro/ +| /3 width=7 by fcla_next, sor_pn, max_S2_le_S, le_S_S, ex4_2_intro/ +| /3 width=7 by fcla_next, sor_np, max_S1_le_S, le_S_S, ex4_2_intro/ +| /4 width=7 by fcla_next, sor_nn, le_S, le_S_S, ex4_2_intro/ +] +qed-. + +lemma sor_fcla: ∀f1,n1. 𝐂⦃f1⦄ ≡ n1 → ∀f2,n2. 𝐂⦃f2⦄ ≡ n2 → ∀f. f1 ⋓ f2 ≡ f → + ∃∃n. 𝐂⦃f⦄ ≡ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2. +#f1 #n1 #Hf1 #f2 #n2 #Hf2 #f #Hf elim (sor_fcla_ex … Hf1 … Hf2) -Hf1 -Hf2 +/4 width=6 by sor_mono, fcla_eq_repl_back, ex3_intro/ +qed-. + +(* Properties on test for finite colength ***********************************) + +lemma sor_isfin_ex: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∃∃f. f1 ⋓ f2 ≡ f & 𝐅⦃f⦄. +#f1 #f2 * #n1 #H1 * #n2 #H2 elim (sor_fcla_ex … H1 … H2) -H1 -H2 +/3 width=4 by ex2_intro, ex_intro/ +qed-. + +lemma sor_isfin: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∀f. f1 ⋓ f2 ≡ f → 𝐅⦃f⦄. +#f1 #f2 #Hf1 #Hf2 #f #Hf elim (sor_isfin_ex … Hf1 … Hf2) -Hf1 -Hf2 +/3 width=6 by sor_mono, isfin_eq_repl_back/ +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 6d0741909..a41b50b2d 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,8 +23,8 @@ table { class "grass" [ { "multiple relocation" * } { [ { "" * } { - [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] - [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] + [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] + [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] @@ -39,7 +39,7 @@ table { [ { "" * } { [ "stream ( ? @ ? )" "stream_eq ( ? ≐ ? )" "stream_hdtl ( ↓? )" "stream_tls ( ↓*[?]? )" * ] [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] - [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )" * ] + [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )" * ] [ "star" "lstar" * ] } ] -- 2.39.2