From: Ferruccio Guidi Date: Tue, 10 Oct 2017 17:05:35 +0000 (+0000) Subject: - more results on relocation X-Git-Tag: make_still_working~439 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=66962864d3703b8f3b44e95d32c03ed50ceee6f1;p=helm.git - more results on relocation - refactoring --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 9a3f0810f..d9355a1a0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/notation/functions/successor_1.ma". +include "ground_2/notation/constructors/successor_1.ma". include "ground_2/notation/functions/predecessor_1.ma". include "arithmetics/nat.ma". include "ground_2/lib/relations.ma". diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/successor_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/successor_1.ma new file mode 100644 index 000000000..05e2c3146 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/successor_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 70 T )" + non associative with precedence 70 + for @{ 'Successor $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma deleted file mode 100644 index 05e2c3146..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successor_1.ma +++ /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( ⫯ term 70 T )" - non associative with precedence 70 - for @{ 'Successor $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successorstar_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successorstar_2.ma new file mode 100644 index 000000000..6f1a617b7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/successorstar_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 n ] term 70 T )" + non associative with precedence 70 + for @{ 'SuccessorStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isdivergent_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isdivergent_1.ma new file mode 100644 index 000000000..cd2838895 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isdivergent_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 @{ 'IsDivergent $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation.ma index ab25c0f44..c5affd746 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation.ma @@ -304,6 +304,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) }. +(* multiple existental quantifier (7, 6) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P6) }. + (* multiple existental quantifier (7, 7) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sand.ma deleted file mode 100644 index 181e8ceff..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sand.ma +++ /dev/null @@ -1,15 +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 *) -(* *) -(**************************************************************************) - -include "ground_2/relocation/rtmap_sand.ma". diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma new file mode 100644 index 000000000..160561664 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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_sor.ma". + +(* RELOCATION N-STREAM ******************************************************) + +axiom union: rtmap → rtmap → rtmap. + +interpretation "union (nstream)" + 'union f1 f2 = (union f1 f2). + +(* Specific properties on sor ***********************************************) + +axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≡ f1 ∪ f2. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma index 4864c9bae..44f491de5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma @@ -236,15 +236,26 @@ lemma coafter_mono_eq: ∀f1,f2,f. f1 ~⊚ f2 ≡ f → ∀g1,g2,g. g1 ~⊚ g2 f1 ≗ g1 → f2 ≗ g2 → f ≗ g. /4 width=4 by coafter_mono, coafter_eq_repl_back1, coafter_eq_repl_back2/ qed-. -(* Inversion lemmas with pushs **********************************************) - -lemma coafter_fwd_pushs: ∀n,g2,g1,g. g2 ~⊚ g1 ≡ g → @⦃0, g2⦄ ≡ n → - ∃f. ↑*[n]f = g. -#n elim n -n /2 width=2 by ex_intro/ -#n #IH #g2 #g1 #g #Hg #Hg2 -cases (at_inv_pxn … Hg2) -Hg2 [ |*: // ] #f2 #Hf2 #H2 -cases (coafter_inv_nxx … Hg … H2) -Hg -H2 #f #Hf #H0 destruct -elim (IH … Hf Hf2) -g1 -g2 -f2 /2 width=2 by ex_intro/ +(* Forward lemmas with pushs ************************************************) + +lemma coafter_fwd_pushs: ∀j,i,g2,f1,g. g2 ~⊚ ↑*[i]f1 ≡ g → @⦃i, g2⦄ ≡ j → + ∃f. ↑*[j] f = g. +#j elim j -j +[ #i #g2 #f1 #g #Hg #H + elim (at_inv_xxp … H) -H [|*: // ] #f2 #H1 #H2 destruct + /2 width=2 by ex_intro/ +| #j #IH * [| #i ] #g2 #f1 #g #Hg #H + [ elim (at_inv_pxn … H) -H [|*: // ] #f2 #Hij #H destruct + elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct + elim (IH … Hf Hij) -f1 -f2 -IH /2 width=2 by ex_intro/ + | elim (at_inv_nxn … H) -H [1,4: * |*: // ] #f2 #Hij #H destruct + [ elim (coafter_inv_ppx … Hg) -Hg [|*: // ] #f #Hf #H destruct + elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/ + | elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct + elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/ + ] + ] +] qed-. (* Inversion lemmas with tail ***********************************************) @@ -267,15 +278,26 @@ qed-. (* Properties with iterated tail ********************************************) -lemma coafter_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → - f1 ~⊚ f2 ≡ f → ⫱*[n]f1 ~⊚ f2 ≡ ⫱*[n]f. -#n elim n -n // -#n #IH #f1 #f2 #f #Hf1 #Hf -cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 -cases (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct -(injective_next … H) -H // +qed-. + +lemma isdiv_inv_push: ∀g. 𝛀⦃g⦄ → ∀f. ↑f = g → ⊥. +#g #H elim (isdiv_inv_gen … H) -H +#f #Hf * -g #g #H elim (discr_push_next … H) +qed-. + +(* Main inversion lemmas ****************************************************) + +corec theorem isdiv_inv_eq_repl: ∀f1,f2. 𝛀⦃f1⦄ → 𝛀⦃f2⦄ → f1 ≗ f2. +#f1 #f2 #H1 #H2 +cases (isdiv_inv_gen … H1) -H1 +cases (isdiv_inv_gen … H2) -H2 +/3 width=5 by eq_next/ +qed-. + +(* Basic properties *********************************************************) + +corec lemma isdiv_eq_repl_back: eq_repl_back … isdiv. +#f1 #H cases (isdiv_inv_gen … H) -H +#g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_nx … Hf … H1) -f1 +/3 width=3 by isdiv_next/ +qed-. + +lemma isdiv_eq_repl_fwd: eq_repl_fwd … isdiv. +/3 width=3 by isdiv_eq_repl_back, eq_repl_sym/ qed-. + +(* Alternative definition ***************************************************) + +corec lemma eq_next_isdiv: ∀f. ⫯f ≗ f → 𝛀⦃f⦄. +#f #H cases (eq_inv_nx … H) -H /4 width=3 by isdiv_next, eq_trans/ +qed. + +corec lemma eq_next_inv_isdiv: ∀f. 𝛀⦃f⦄ → ⫯f ≗ f. +#f * -f +#f #g #Hf #Hg @(eq_next … Hg) [2: @eq_next_inv_isdiv // | skip ] +@eq_f // +qed-. + +(* Properties with iterated next ********************************************) + +lemma isdiv_nexts: ∀n,f. 𝛀⦃f⦄ → 𝛀⦃⫯*[n]f⦄. +#n elim n -n /3 width=3 by isdiv_next/ +qed. + +(* Inversion lemmas with iterated next **************************************) + +lemma isdiv_inv_nexts: ∀n,g. 𝛀⦃⫯*[n]g⦄ → 𝛀⦃g⦄. +#n elim n -n /3 width=3 by isdiv_inv_next/ +qed. + +(* Properties with tail *****************************************************) + +lemma isdiv_tl: ∀f. 𝛀⦃f⦄ → 𝛀⦃⫱f⦄. +#f cases (pn_split f) * #g * -f #H +[ elim (isdiv_inv_push … H) -H // +| /2 width=3 by isdiv_inv_next/ +] +qed. + +(* Properties with iterated tail ********************************************) + +lemma isdiv_tls: ∀n,g. 𝛀⦃g⦄ → 𝛀⦃⫱*[n]g⦄. +#n elim n -n /3 width=1 by isdiv_tl/ +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 index b73e34cea..875378b98 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma @@ -35,17 +35,15 @@ qed-. (* Basic inversion lemmas ***************************************************) +lemma isfin_inv_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄. +#g * /3 width=4 by fcla_inv_px, ex_intro/ +qed-. + 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-. - (* Basic properties *********************************************************) lemma isfin_eq_repl_back: eq_repl_back … isfin. @@ -66,9 +64,23 @@ lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄. #f * /3 width=2 by fcla_next, ex_intro/ qed. +(* Properties with iterated push ********************************************) + +lemma isfin_pushs: ∀n,f. 𝐅⦃f⦄ → 𝐅⦃↑*[n]f⦄. +#n elim n -n /3 width=3 by isfin_push/ +qed. + +(* Inversion lemmas with iterated push **************************************) + +lemma isfin_inv_pushs: ∀n,g. 𝐅⦃↑*[n]g⦄ → 𝐅⦃g⦄. +#n elim n -n /3 width=3 by isfin_inv_push/ +qed. + +(* Properties with tail *****************************************************) + lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄. #f elim (pn_split f) * #g #H #Hf destruct -/3 width=3 by isfin_fwd_push, isfin_inv_next/ +/3 width=3 by isfin_inv_push, isfin_inv_next/ qed. (* Inversion lemmas with tail ***********************************************) @@ -77,7 +89,7 @@ lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄. #f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/ qed-. -(* Inversion lemmas with tls ********************************************************) +(* Inversion lemmas with iterated tail **************************************) lemma isfin_inv_tls: ∀n,f. 𝐅⦃⫱*[n]f⦄ → 𝐅⦃f⦄. #n elim n -n /3 width=1 by isfin_inv_tl/ 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 d713c1618..65e111bbf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma @@ -75,6 +75,18 @@ corec lemma eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f. @eq_f // qed-. +(* Properties with iterated push ********************************************) + +lemma isid_pushs: ∀n,f. 𝐈⦃f⦄ → 𝐈⦃↑*[n]f⦄. +#n elim n -n /3 width=3 by isid_push/ +qed. + +(* Inversion lemmas with iterated push **************************************) + +lemma isid_inv_pushs: ∀n,g. 𝐈⦃↑*[n]g⦄ → 𝐈⦃g⦄. +#n elim n -n /3 width=3 by isid_inv_push/ +qed. + (* Properties with tail *****************************************************) lemma isid_tl: ∀f. 𝐈⦃f⦄ → 𝐈⦃⫱f⦄. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_nexts.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_nexts.ma new file mode 100644 index 000000000..91e916d93 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_nexts.ma @@ -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/notation/functions/successorstar_2.ma". +include "ground_2/relocation/rtmap_eq.ma". + +(* RELOCATION MAP ***********************************************************) + +rec definition nexts (f:rtmap) (n:nat) on n: rtmap ≝ match n with +[ O ⇒ f | S m ⇒ ⫯(nexts f m) ]. + +interpretation "nexts (rtmap)" 'SuccessorStar n f = (nexts f n). + +(* Basic_inversion lemmas *****************************************************) + +lemma eq_inv_nexts_sn: ∀n,f1,g2. ⫯*[n] f1 ≗ g2 → + ∃∃f2. f1 ≗ f2 & ⫯*[n] f2 = g2. +#n elim n -n /2 width=3 by ex2_intro/ +#n #IH #f1 #g2 #H elim (eq_inv_nx … H) -H [|*: // ] +#f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma eq_inv_nexts_dx: ∀n,f2,g1. g1 ≗ ⫯*[n] f2 → + ∃∃f1. f1 ≗ f2 & ⫯*[n] f1 = g1. +#n elim n -n /2 width=3 by ex2_intro/ +#n #IH #f2 #g1 #H elim (eq_inv_xn … H) -H [|*: // ] +#f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct +/2 width=3 by ex2_intro/ +qed-. + +(* Basic properties *********************************************************) + +lemma nexts_O: ∀f. f = ⫯*[0] f. +// qed. + +lemma nexts_S: ∀f,n. ⫯⫯*[n] f = ⫯*[⫯n] f. +// qed. + +lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ⫯*[n] f1 ≗ ⫯*[n] f2). +#n elim n -n /3 width=5 by eq_next/ +qed. + +(* Advanced properties ******************************************************) + +lemma nexts_xn: ∀n,f. ⫯*[n] ⫯f = ⫯*[⫯n] f. +#n elim n -n // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma index 9772f34bd..a1e7ab669 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_pushs.ma @@ -22,6 +22,24 @@ rec definition pushs (f:rtmap) (n:nat) on n: rtmap ≝ match n with interpretation "pushs (rtmap)" 'LiftStar n f = (pushs f n). +(* Basic_inversion lemmas *****************************************************) + +lemma eq_inv_pushs_sn: ∀n,f1,g2. ↑*[n] f1 ≗ g2 → + ∃∃f2. f1 ≗ f2 & ↑*[n] f2 = g2. +#n elim n -n /2 width=3 by ex2_intro/ +#n #IH #f1 #g2 #H elim (eq_inv_px … H) -H [|*: // ] +#f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma eq_inv_pushs_dx: ∀n,f2,g1. g1 ≗ ↑*[n] f2 → + ∃∃f1. f1 ≗ f2 & ↑*[n] f1 = g1. +#n elim n -n /2 width=3 by ex2_intro/ +#n #IH #f2 #g1 #H elim (eq_inv_xp … H) -H [|*: // ] +#f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct +/2 width=3 by ex2_intro/ +qed-. + (* Basic properties *********************************************************) lemma pushs_O: ∀f. f = ↑*[0] f. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma index c5d9428a5..cebc3aa4a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground_2/relocation/rtmap_isid.ma". +include "ground_2/relocation/rtmap_isdiv.ma". (* RELOCATION MAP ***********************************************************) @@ -27,9 +28,10 @@ interpretation "inclusion (rtmap)" (* Basic properties *********************************************************) -corec lemma sle_refl: ∀f. f ⊆ f. -#f cases (pn_split f) * #g #H -[ @(sle_push … H H) | @(sle_next … H H) ] -H // +corec lemma sle_refl: ∀f1,f2. f1 ≗ f2 → f1 ⊆ f2. +#f1 #f2 * -f1 -f2 +#f1 #f2 #g1 #g2 #H12 #H1 #H2 +[ @(sle_push … H1 H2) | @(sle_next … H1 H2) ] -H1 -H2 /2 width=1 by/ qed. (* Basic inversion lemmas ***************************************************) @@ -147,3 +149,21 @@ corec lemma sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1 lapply (isid_inv_push … H ??) -H /3 width=3 by isid_push/ qed-. + +(* Properties with isdiv ****************************************************) + +corec lemma sle_isdiv_dx: ∀f2. 𝛀⦃f2⦄ → ∀f1. f1 ⊆ f2. +#f2 * -f2 +#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * +/3 width=5 by sle_weak, sle_next/ +qed. + +(* Inversion lemmas with isdiv **********************************************) + +corec lemma sle_inv_isdiv_sn: ∀f1,f2. f1 ⊆ f2 → 𝛀⦃f1⦄ → 𝛀⦃f2⦄. +#f1 #f2 * -f1 -f2 +#f1 #f2 #g1 #g2 #Hf * * #H +[1,3: elim (isdiv_inv_push … H) // ] +lapply (isdiv_inv_next … H ??) -H +/3 width=3 by isdiv_next/ +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 bc2a7dda6..10f1b0b0a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -266,19 +266,6 @@ corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f. [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/ qed-. -(* Main properties **********************************************************) - -axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 → - ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g. - -axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 → - ∀f1,f2. f1 ⋓ f2 ≡ f0 → - ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4. - -axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 → - ∀f2, f3. f2 ⋓ f3 ≡ f0 → - ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4. - (* Properties with tail *****************************************************) lemma sor_tl: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ⫱f1 ⋓ ⫱f2 ≡ ⫱f. @@ -461,3 +448,46 @@ qed. corec lemma sor_sle_sn: ∀f1,f2. f1 ⊆ f2 → f2 ⋓ f1 ≡ f2. #f1 #f2 * -f1 -f2 /3 width=7 by sor_pp, sor_nn, sor_np/ qed. + +(* Main properties **********************************************************) + +axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 → + ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g. + +axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 → + ∀f1,f2. f1 ⋓ f2 ≡ f0 → + ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4. + +axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 → + ∀f2, f3. f2 ⋓ f3 ≡ f0 → + ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4. + +corec theorem sor_distr_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g1,g2,g. g1 ⋓ g2 ≡ g → + ∀g0. g1 ⋓ g0 ≡ f1 → g2 ⋓ g0 ≡ f2 → g ⋓ g0 ≡ f. +#f1 #f2 #f cases (pn_split f) * #x #Hx #Hf #g1 #g2 #g #Hg #g0 #Hf1 #Hf2 +[ cases (sor_inv_xxp … Hf … Hx) -Hf #x1 #x2 #Hf #Hx1 #Hx2 + cases (sor_inv_xxp … Hf1 … Hx1) -f1 #y1 #y0 #Hf1 #Hy1 #Hy0 + cases (sor_inv_xpp … Hf2 … Hy0 … Hx2) -f2 #y2 #Hf2 #Hy2 + cases (sor_inv_ppx … Hg … Hy1 Hy2) -g1 -g2 #y #Hg #Hy + @(sor_pp … Hy Hy0 Hx) -g -g0 -f /2 width=8 by/ +| cases (pn_split g) * #y #Hy + [ cases (sor_inv_xxp … Hg … Hy) -Hg #y1 #y2 #Hg #Hy1 #Hy2 + cases (sor_xxn_tl … Hf … Hx) * #x1 #x2 #_ #Hx1 #Hx2 + [ cases (sor_inv_pxn … Hf1 … Hy1 Hx1) -g1 #y0 #Hf1 #Hy0 + cases (sor_inv_pnx … Hf2 … Hy2 Hy0) -g2 -x2 #x2 #Hf2 #Hx2 + | cases (sor_inv_pxn … Hf2 … Hy2 Hx2) -g2 #y0 #Hf2 #Hy0 + cases (sor_inv_pnx … Hf1 … Hy1 Hy0) -g1 -x1 #x1 #Hf1 #Hx1 + ] + lapply (sor_inv_nnn … Hf … Hx1 Hx2 Hx) -f1 -f2 #Hf + @(sor_pn … Hy Hy0 Hx) -g -g0 -f /2 width=8 by/ + | lapply (sor_tl … Hf) -Hf #Hf + lapply (sor_tl … Hg) -Hg #Hg + lapply (sor_tl … Hf1) -Hf1 #Hf1 + lapply (sor_tl … Hf2) -Hf2 #Hf2 + cases (pn_split g0) * #y0 #Hy0 + [ @(sor_np … Hy Hy0 Hx) /2 width=8 by/ + | @(sor_nn … Hy Hy0 Hx) /2 width=8 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 4cfc0f6eb..a90603dd0 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 @@ -20,8 +20,15 @@ table { class "green" [ { "multiple relocation" * } { [ { "" * } { - [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )" * ] - [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" * ] + [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_nexts ( ⫯*[?]? )" + "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isdiv ( 𝛀⦃?⦄ )" + "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" + "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" + "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )" + * ] + [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" + "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" + * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index eaa102c4e..3f8eef198 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -34,6 +34,7 @@ 7 3 7 4 7 5 + 7 6 7 7 7 9 7 10 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index 4954c0cc4..4ff65068f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -250,6 +250,14 @@ inductive ex7_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3 interpretation "multiple existental quantifier (7, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +(* multiple existental quantifier (7, 6) *) + +inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ + | ex7_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + (* multiple existental quantifier (7, 7) *) inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝