From: Ferruccio Guidi Date: Thu, 10 Mar 2016 21:16:20 +0000 (+0000) Subject: - ground_2: some additions X-Git-Tag: make_still_working~632 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=064980eacc2efe70ffee96134d75dfa37506fc36;p=helm.git - ground_2: some additions - basic_2/grammar: added missing files --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/ceq.ma new file mode 100644 index 000000000..abd6b25b3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/ceq.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/grammar/lenv.ma". + +(* CONTEXT-SENSITIVE EQUIVALENCES FOR TERMS *********************************) + +definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2. + +definition cfull: relation3 lenv term term ≝ λL,T1,T2. ⊤. + +(* Basic properties *********************************************************) + +lemma ceq_refl (L): reflexive … (ceq L). +// qed. + +lemma cfull_refl (L): reflexive … (cfull L). +// qed. + +lemma ceq_sym (L): symmetric … (ceq L). +// qed-. + +lemma cfull_sym (L): symmetric … (cfull L). +// qed-. + +lemma cfull_top (R:relation3 lenv term term) (L) (T1) (T2): + R L T1 T2 → cfull L T1 T2. +// qed-. + +lemma ceq_cfull (L) (T1) (T2): ceq L T1 T2 → cfull L T1 T2. +// qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/ceq_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/ceq_ceq.ma new file mode 100644 index 000000000..142f3b863 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/ceq_ceq.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/grammar/ceq.ma". + +(* CONTEXT-SENSITIVE EQUIVALENCES FOR TERMS *********************************) + +(* Main properties **********************************************************) + +theorem ceq_trans (L): Transitive … (ceq L). +// qed-. + +lemma ceq_canc_sn (L): left_cancellable … (ceq L). +// qed-. + +lemma ceq_canc_dx (L): right_cancellable … (ceq L). +// qed-. + +theorem cfull_trans (L): Transitive … (cfull L). +// qed-. + +lemma cfull_canc_sn (L): left_cancellable … (cfull L). +// qed-. + +lemma cfull_canc_dx (L): right_cancellable … (cfull L). +// qed-. \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.etc deleted file mode 100644 index 16120c08d..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.etc +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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( L1 ⋓ break term 46 L2 ≡ break term 46 L )" - non associative with precedence 45 - for @{ 'RUnion $L1 $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index 9bbecddca..bf7f3b11f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -21,6 +21,12 @@ definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2. + +definition left_cancellable: ∀A. ∀R: relation A. Prop ≝ λA,R. + ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 → R a1 a2. + +definition right_cancellable: ∀A. ∀R: relation A. Prop ≝ λA,R. + ∀a1,a0. R a1 a0 → ∀a2. R a2 a0 → R a1 a2. definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma new file mode 100644 index 000000000..16120c08d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.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( L1 ⋓ break term 46 L2 ≡ break term 46 L )" + non associative with precedence 45 + for @{ 'RUnion $L1 $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma index 85ad506a2..5f707a571 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma @@ -25,6 +25,52 @@ coinductive sand: relation3 rtmap rtmap rtmap ≝ interpretation "intersection (rtmap)" 'RIntersection f1 f2 f = (sand f1 f2 f). +(* Basic inversion lemmas ***************************************************) + +lemma sand_inv_ppx: ∀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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +lemma sand_inv_npx: ∀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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +lemma sand_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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +lemma sand_inv_nnx: ∀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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + (* Basic properties *********************************************************) let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma new file mode 100644 index 000000000..7b437099e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -0,0 +1,85 @@ +(**************************************************************************) +(* ___ *) +(* ||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/runion_3.ma". +include "ground_2/relocation/rtmap_sle.ma". + +coinductive sor: relation3 rtmap rtmap rtmap ≝ +| sor_pp: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → sor g1 g2 g +| sor_np: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ⫯f = g → sor g1 g2 g +| sor_pn: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ⫯f = g → sor g1 g2 g +| sor_nn: ∀f1,f2,f,g1,g2,g. sor f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → sor g1 g2 g +. + +interpretation "union (rtmap)" + 'RUnion f1 f2 f = (sor f1 f2 f). + +(* Basic inversion lemmas ***************************************************) + +lemma sor_inv_ppx: ∀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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +lemma sor_inv_npx: ∀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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +lemma sor_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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +lemma sor_inv_nnx: ∀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 #Hf #H1 #H2 #H0 #x1 #x2 #Hx1 #Hx2 destruct +try (>(injective_push … Hx1) -x1) try (>(injective_next … Hx1) -x1) +try elim (discr_push_next … Hx1) try elim (discr_next_push … Hx1) +try (>(injective_push … Hx2) -x2) try (>(injective_next … Hx2) -x2) +try elim (discr_push_next … Hx2) try elim (discr_next_push … Hx2) +/2 width=3 by ex2_intro/ +qed-. + +(* Basic properties *********************************************************) + +let corec sor_refl: ∀f. f ⋓ f ≡ f ≝ ?. +#f cases (pn_split f) * #g #H +[ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H // +qed. + +let corec sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f ≝ ?. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g +[ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/ +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 cbff64690..cfbe19cf3 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_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "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_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 ( ∁ ? )" * ]