From: Ferruccio Guidi Date: Fri, 4 Mar 2016 13:39:02 +0000 (+0000) Subject: rtmap (platform-indepent multple relocation): application and composition X-Git-Tag: make_still_working~639 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad3d1cac216cf3882e4adf691b27c00838c6b9b1;p=helm.git rtmap (platform-indepent multple relocation): application and composition --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/complement_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/complement_1.etc new file mode 100644 index 000000000..a10c80f17 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/complement_1.etc @@ -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 @{ 'Complement $t }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc new file mode 100644 index 000000000..349f2b3bf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/isuniform_1.etc @@ -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 @{ 'IsUniform $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/norm_1.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/norm_1.etc new file mode 100644 index 000000000..d0f0719f1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/norm_1.etc @@ -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 19 C ∥ )" + with precedence 70 + for @{ 'Norm $C }. 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 new file mode 100644 index 000000000..16120c08d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/runion_3.etc @@ -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/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma index bdc740c82..050568754 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/drop_1.ma". include "ground_2/lib/streams.ma". include "ground_2/lib/arith.ma". @@ -23,17 +24,16 @@ definition hd (A:Type[0]): stream A → A ≝ definition tl (A:Type[0]): stream A → stream A ≝ λt. match t with [ seq _ t ⇒ t ]. -let rec tln (A:Type[0]) (i:nat) on i: stream A → stream A ≝ ?. -cases i -i [ #t @t | #i * #_ #t @(tln … i t) ] -qed. +interpretation "tail (streams)" 'Drop t = (tl ? t). (* basic properties *********************************************************) -lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t. -#A * // -qed. +lemma hd_rew (A) (a) (t): a = hd A (a@t). +// qed. -lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2). -#A #i elim i -i // -#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/ +lemma tl_rew (A) (a) (t): t = tl A (a@t). +// qed. + +lemma eq_stream_split (A) (t): (hd … t) @ ↓t ≐⦋A⦌ t. +#A * // qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_1.ma deleted file mode 100644 index a10c80f17..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/complement_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 @{ 'Complement $t }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppred_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppred_1.ma new file mode 100644 index 000000000..7e82080a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppred_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 @{ 'DropPred $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_2.ma new file mode 100644 index 000000000..1b10938b7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/droppreds_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 46 T )" + non associative with precedence 46 + for @{ 'DropPreds $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drops_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drops_2.ma new file mode 100644 index 000000000..9b20a4324 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drops_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 46 T )" + non associative with precedence 46 + for @{ 'Drops $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma deleted file mode 100644 index d0f0719f1..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_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 19 C ∥ )" - with precedence 70 - for @{ 'Norm $C }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_1.ma deleted file mode 100644 index 349f2b3bf..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isuniform_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 46 f ⦄ )" - non associative with precedence 45 - for @{ 'IsUniform $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_3.ma new file mode 100644 index 000000000..c680542e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_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 @{ 'RIntersection $L1 $L2 $L }. 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 deleted file mode 100644 index 16120c08d..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.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( 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/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma index aaa1ba9b6..8d7dacc4e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma @@ -13,8 +13,7 @@ (**************************************************************************) include "ground_2/notation/functions/lift_1.ma". -include "ground_2/lib/arith.ma". -include "ground_2/lib/streams.ma". +include "ground_2/lib/streams_tls.ma". (* RELOCATION N-STREAM ******************************************************) @@ -88,3 +87,11 @@ lemma iota_push: ∀R,a,b,f. a f = case_type0 R a b (↑f). lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (⫯f). #R #a #b * // qed. + +(* Specific properties ******************************************************) + +lemma tl_push: ∀f. f = ↓↑f. +// qed. + +lemma tl_next: ∀f. ↓f = ↓⫯f. +* // qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma index b599e03cc..a9b022b4d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -12,82 +12,69 @@ (* *) (**************************************************************************) -include "ground_2/notation/relations/rafter_3.ma". -include "ground_2/lib/streams_hdtl.ma". -include "ground_2/relocation/nstream_at.ma". +include "ground_2/relocation/nstream_istot.ma". +include "ground_2/relocation/rtmap_after.ma". (* RELOCATION N-STREAM ******************************************************) let corec compose: rtmap → rtmap → rtmap ≝ ?. #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2 -@(tln … (⫯n2) f1) +@(↓*[⫯n2] f1) defined. interpretation "functional composition (nstream)" 'compose f1 f2 = (compose f1 f2). -coinductive after: relation3 rtmap rtmap rtmap ≝ -| after_refl: ∀f1,f2,f,g1,g2,g. - after f1 f2 f → g1 = ↑f1 → g2 = ↑f2 → g = ↑f → after g1 g2 g -| after_push: ∀f1,f2,f,g1,g2,g. - after f1 f2 f → g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → after g1 g2 g -| after_next: ∀f1,f2,f,g1,g. - after f1 f2 f → g1 = ⫯f1 → g = ⫯f → after g1 f2 g -. - -interpretation "relational composition (nstream)" - 'RAfter f1 f2 f = (after f1 f2 f). - (* Basic properies on compose ***********************************************) -lemma compose_unfold: ∀f1,f2,n2. f1∘(n2@f2) = f1@❴n2❵@tln … (⫯n2) f1∘f2. -#f1 #f2 #n2 >(stream_expand … (f1∘(n2@f2))) normalize // +lemma compose_rew: ∀f1,f2,n2. f1@❴n2❵@(↓*[⫯n2]f1)∘f2 = f1∘(n2@f2). +#f1 #f2 #n2 <(stream_rew … (f1∘(n2@f2))) normalize // qed. lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f. -* #n1 #f1 * #n2 #f2 #f >compose_unfold >compose_unfold -#H destruct normalize // +#f1 * #n2 #f2 #f (stream_expand … (f1∘(n2@f2))) normalize +lemma compose_inv_rew: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f → + f1@❴n2❵ = n ∧ (↓*[⫯n2]f1)∘f2 = f. +#f1 #f2 #f #n2 #n <(stream_rew … (f1∘(n2@f2))) normalize #H destruct /2 width=1 by conj/ qed-. lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f → - n = n1 ∧ f1∘f2 = f. -#f1 #f2 #f #n1 #n >compose_unfold + n1 = n ∧ f1∘f2 = f. +#f1 #f2 #f #n1 #n compose_unfold -#H destruct /2 width=1 by conj/ + ⫯(n1+f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f. +#f1 #f2 #f #n1 #n2 #n compose_unfold -#H destruct /2 width=1 by conj/ +lemma compose_inv_S1: ∀f1,f2,f,n2,n. (⫯f1)∘(n2@f2) = n@f → + ⫯(f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f. +#f1 #f2 #f #n2 #n next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=7 by after_next/ ] qed-. theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2. /2 width=1 by after_total_aux/ qed. -(* Basic inversion lemmas on after ******************************************) - -fact after_inv_OOx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ↑f2 → - ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f. -#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1 -[ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct - <(injective_push … Hx1) <(injective_push … Hx2) -x2 -x1 - /2 width=3 by ex2_intro/ -| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct - elim (discr_next_push … Hx2) -| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct - elim (discr_next_push … Hx1) -] -qed-. - -lemma after_inv_OOx: ∀f1,f2,g. ↑f1 ⊚ ↑f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ↑f. -/2 width=5 by after_inv_OOx_aux/ qed-. - -fact after_inv_OSx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. g1 = ↑f1 → g2 = ⫯f2 → - ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. -#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1 -[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct - elim (discr_push_next … 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_next_push … Hx1) -] -qed-. - -lemma after_inv_OSx: ∀f1,f2,g. ↑f1 ⊚ ⫯f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. -/2 width=5 by after_inv_OSx_aux/ qed-. - -fact after_inv_Sxx_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. g1 = ⫯f1 → - ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. -#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1 -[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct - elim (discr_push_next … Hx1) -| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct - elim (discr_push_next … Hx1) -| #g #Hf #H1 #H #x1 #Hx1 destruct - <(injective_next … Hx1) -x1 - /2 width=3 by ex2_intro/ -] -qed-. - -lemma after_inv_Sxx: ∀f1,f2,g. ⫯f1 ⊚ f2 ≡ g → ∃∃f. f1 ⊚ f2 ≡ f & g = ⫯f. -/2 width=5 by after_inv_Sxx_aux/ qed-. - -(* Advanced inversion lemmas on after ***************************************) - -fact after_inv_OOO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → - ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ↑f → f1 ⊚ f2 ≡ f. -#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2 -#x #Hf #Hx destruct >(injective_push … Hx) -f // -qed-. - -fact after_inv_OOS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → - ∀f1,f2,f. g1 = ↑f1 → g2 = ↑f2 → g = ⫯f → ⊥. -#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2 -#x #Hf #Hx destruct elim (discr_next_push … Hx) -qed-. - -fact after_inv_OSS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → - ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ⫯f → f1 ⊚ f2 ≡ f. -#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2 -#x #Hf #Hx destruct >(injective_next … Hx) -f // -qed-. - -fact after_inv_OSO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → - ∀f1,f2,f. g1 = ↑f1 → g2 = ⫯f2 → g = ↑f → ⊥. -#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_OSx_aux … Hg … H1 H2) -g1 -g2 -#x #Hf #Hx destruct elim (discr_push_next … Hx) -qed-. - -fact after_inv_SxS_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → - ∀f1,f. g1 = ⫯f1 → g = ⫯f → f1 ⊚ f2 ≡ f. -#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1 -#x #Hf #Hx destruct >(injective_next … Hx) -f // -qed-. - -fact after_inv_SxO_aux: ∀g1,f2,g. g1 ⊚ f2 ≡ g → - ∀f1,f. g1 = ⫯f1 → g = ↑f → ⊥. -#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_Sxx_aux … Hg … H1) -g1 -#x #Hf #Hx destruct elim (discr_push_next … Hx) -qed-. - -fact after_inv_OxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → - ∀f1,f. g1 = ↑f1 → g = ↑f → - ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2. -#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H -[ elim (after_inv_OSO_aux … Hg … H1 … H) -g1 -g -f1 -f // -| lapply (after_inv_OOO_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ -] -qed-. +(* Specific inversion lemmas ************************************************) -lemma after_inv_OxO: ∀f1,g2,f. ↑f1 ⊚ g2 ≡ ↑f → - ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ↑f2. -/2 width=5 by after_inv_OxO_aux/ qed-. - -fact after_inv_OxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → - ∀f1,f. g1 = ↑f1 → g = ⫯f → - ∃∃f2. f1 ⊚ f2 ≡ f & g2 = ⫯f2. -#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H -[ lapply (after_inv_OSS_aux … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ -| elim (after_inv_OOS_aux … Hg … H1 … H) -g1 -g -f1 -f // -] -qed-. - -fact after_inv_xxO_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ↑f → - ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2. -* * [2: #m1 ] #g1 #g2 #g #Hg #f #H -[ elim (after_inv_SxO_aux … Hg … H) -g2 -g -f // -| elim (after_inv_OxO_aux … Hg … H) -g /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma after_inv_xxO: ∀g1,g2,f. g1 ⊚ g2 ≡ ↑f → - ∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ↑f2. -/2 width=3 by after_inv_xxO_aux/ qed-. - -fact after_inv_xxS_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. g = ⫯f → - (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨ - ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1. -* * [2: #m1 ] #g1 #g2 #g #Hg #f #H -[ /4 width=5 by after_inv_SxS_aux, or_intror, ex2_intro/ -| elim (after_inv_OxS_aux … Hg … H) -g - /3 width=5 by or_introl, ex3_2_intro/ -] -qed-. - -lemma after_inv_xxS: ∀g1,g2,f. g1 ⊚ g2 ≡ ⫯f → - (∃∃f1,f2. f1 ⊚ f2 ≡ f & g1 = ↑f1 & g2 = ⫯f2) ∨ - ∃∃f1. f1 ⊚ g2 ≡ f & g1 = ⫯f1. -/2 width=3 by after_inv_xxS_aux/ qed-. - -fact after_inv_Oxx_aux: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. g1 = ↑f1 → - (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨ - (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f). -#g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H -[ elim (after_inv_OSx_aux … Hg … H) -g1 - /3 width=5 by or_intror, ex3_2_intro/ -| elim (after_inv_OOx_aux … Hg … H) -g1 - /3 width=5 by or_introl, ex3_2_intro/ -] -qed-. - -lemma after_inv_Oxx: ∀f1,g2,g. ↑f1 ⊚ g2 ≡ g → - (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ↑f2 & g = ↑f) ∨ - (∃∃f2,f. f1 ⊚ f2 ≡ f & g2 = ⫯f2 & g = ⫯f). -/2 width=3 by after_inv_Oxx_aux/ qed-. - -fact after_inv_xOx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ↑f2 → - f1 ⊚ f2 ≡ f ∧ n1 = n. +lemma after_inv_xpx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ↑f2 = g2 → + f1 ⊚ f2 ≡ f ∧ n1 = n. #f1 #g2 #f #n1 elim n1 -n1 -[ #n #Hf #f2 #H2 elim (after_inv_OOx_aux … Hf … H2) -g2 [3: // |2: skip ] - #g #Hf #H elim (push_inv_seq_sn … H) -H destruct /2 width=1 by conj/ -| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ] - #g1 #Hg #H1 elim (next_inv_seq_sn … H1) -H1 - #x #Hx #H destruct elim (IH … Hg) [2: // |3: skip ] -IH -Hg +[ #n #Hf #f2 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ] + #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/ +| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] + #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1 + #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg #H destruct /2 width=1 by conj/ ] qed-. -lemma after_inv_xOx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ↑f2 ≡ n@f → - f1 ⊚ f2 ≡ f ∧ n1 = n. -/2 width=3 by after_inv_xOx_aux/ qed-. - -fact after_inv_xSx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ⫯f2 → - ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m). +lemma after_inv_xnx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ⫯f2 = g2 → + ∃∃m. f1 ⊚ f2 ≡ m@f & ⫯(n1+m) = n. #f1 #g2 #f #n1 elim n1 -n1 -[ #n #Hf #f2 #H2 elim (after_inv_OSx_aux … Hf … H2) -g2 [3: // |2: skip ] - #g #Hf #H elim (next_inv_seq_sn … H) -H +[ #n #Hf #f2 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ] + #g #Hf #H elim (next_inv_seq_dx … H) -H #x #Hx #Hg destruct /2 width=3 by ex2_intro/ -| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_Sxx_aux … Hf) -Hf [3: // |2: skip ] - #g #Hg #H elim (next_inv_seq_sn … H) -H - #x #Hx #H destruct elim (IH … Hg) -IH -Hg [3: // |2: skip ] +| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] + #g #Hg #H elim (next_inv_seq_dx … H) -H + #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ] #m #Hf #Hm destruct /2 width=3 by ex2_intro/ ] qed-. -lemma after_inv_xSx: ∀f1,f2,f,n1,n. n1@f1 ⊚ ⫯f2 ≡ n@f → - ∃∃m. f1 ⊚ f2 ≡ m@f & n = ⫯(n1+m). -/2 width=3 by after_inv_xSx_aux/ qed-. - -lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ n2 = 0. +lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ 0 = n2. #f1 #f2 #f #n2 #n elim n -n -[ #H elim (after_inv_OxO … H) -H - #g2 #Hf #H elim (push_inv_seq_sn … H) -H /2 width=1 by conj/ -| #n #IH #H lapply (after_inv_SxS_aux … H ????) -H /2 width=5 by/ -] -qed-. - -(* Forward lemmas on application ********************************************) - -lemma after_at_fwd: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f → - ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i. -#f #i1 #i #H elim H -f -i1 -i -[ #f #f2 #f1 #H elim (after_inv_xxO … H) -H - /2 width=3 by at_refl, ex2_intro/ -| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxO … H) -H - #g2 #g1 #Hg #H1 #H2 destruct elim (IH … Hg) -f - /3 width=3 by at_S1, ex2_intro/ -| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_xxS … H) -H * - [ #g2 #g1 #Hg #H2 #H1 destruct elim (IH … Hg) -f - /3 width=3 by at_S1, at_next, ex2_intro/ - | #g1 #Hg #H destruct elim (IH … Hg) -f - /3 width=3 by at_next, ex2_intro/ - ] +[ #H elim (after_inv_pxp … H) -H [ |*: // ] + #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ +| #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/ ] qed-. -lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2,f. f2 ⊚ f1 ≡ f → - ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i. -#f1 #i1 #i2 #H elim H -f1 -i1 -i2 -[ #f1 * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H /2 width=3 by ex2_intro/ -| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xOx … H) -H - #Hf #H destruct elim (IH … Hf) -f1 /3 width=3 by at_S1, ex2_intro/ -| #f1 #i1 #i2 #_ #IH * #n2 #f2 * #n #f #H elim (after_inv_xSx … H) -H - #m #Hf #Hm destruct elim (IH … Hf) -f1 - /4 width=3 by at_plus2, at_S1, at_next, ex2_intro/ -] -qed-. - -lemma after_fwd_at: ∀f1,f2,i1,i2,i. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i → - ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i. -#f1 #f2 #i1 #i2 #i #Hi1 #Hi2 #f #Ht elim (after_at1_fwd … Hi1 … Ht) -f1 -#j #H #Hj >(at_mono … H … Hi2) -i2 // -qed-. - -lemma after_fwd_at1: ∀f2,f,i1,i2,i. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i → - ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2. -#f2 #f #i1 #i2 #i #Hi1 #Hi2 #f1 #Ht elim (after_at_fwd … Hi1 … Ht) -f -#j1 #Hij1 #H >(at_inj … Hi2 … H) -i // -qed-. +(* Specific forward lemmas **************************************************) -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 #H elim H -f -i1 -i -[ #f #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H - #g2 #g1 #_ #H1 #H2 destruct >(at_inv_OOx … Ht1) -f -g1 -i2 // -| #f #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_xxO … H) -H - #g2 #g1 #Hu #H1 #H2 destruct elim (at_inv_SOx … Ht1) -Ht1 - /3 width=3 by at_push/ -| #f #i1 #i #_ #IH #f1 #i2 #Hf1 #f2 #H elim (after_inv_xxS … H) -H * - [ #g2 #g1 #Hg #H2 #H1 destruct elim (at_inv_xSx … Hf1) -Hf1 - /3 width=3 by at_push/ - | #g2 #Hg #H destruct /3 width=3 by at_next/ - ] -] -qed-. - -(* Advanced forward lemmas on after *****************************************) - -lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → n = f1@❴n2❵. -#f1 #f2 #f #n2 #n #H lapply (after_fwd_at … 0 … H) -H [1,4: // |2,3: skip ] +lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n. +#f1 #f2 #f #n2 #n #H lapply (after_fwd_at ? n2 0 … H) -H [1,2,3: // ] /3 width=2 by at_inv_O1, sym_eq/ qed-. -lemma after_fwd_tl: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f → - tln … n2 f1 ⊚ f2 ≡ f. +lemma after_fwd_tls: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f → + (↓*[n2]f1) ⊚ f2 ≡ f. #f #f2 #n2 elim n2 -n2 -[ #f1 #n1 #n #H elim (after_inv_xOx … H) -H // -| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xSx_aux … H ??) -H [3: // |2: skip ] +[ #f1 #n1 #n #H elim (after_inv_xpx … H) -H // +| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xnx … H) -H [2,3: // ] #m #Hm #H destruct /2 width=3 by/ ] qed-. -lemma after_inv_apply: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → - a = (a1@f1)@❴a2❵ ∧ tln … a2 f1 ⊚ f2 ≡ f. -/3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-. - -(* Main properties on after *************************************************) - -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_xxO_aux … Hg0 … H0) -g0 - #f1 #f2 #Hf0 #H1 #H2 - cases (after_inv_OOx_aux … 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_xxO_aux … Hg0 … H0) -g0 - #f1 #f2 #Hf0 #H1 #H2 - cases (after_inv_OSx_aux … 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_xxS_aux … Hg0 … H0) -g0 * - [ #f1 #f2 #Hf0 #H1 #H2 - cases (after_inv_Sxx_aux … 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_xxO_aux … Hg0 … H0) -g0 - #f2 #f3 #Hf0 #H2 #H3 - cases (after_inv_OOx_aux … 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_xxS_aux … Hg0 … H0) -g0 * - [ #f2 #f3 #Hf0 #H2 #H3 - cases (after_inv_OOx_aux … Hg … H1 H2) -g1 -g2 - #f #Hf #H /3 width=7 by after_push/ - | #f2 #Hf0 #H2 - cases (after_inv_OSx_aux … 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_Sxx_aux … Hg … H1) -g1 - #f #Hg #H /3 width=6 by after_next/ -] -qed-. - -(* Main inversion lemmas on after *******************************************) - -let corec after_mono: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g → - f1 ≐ g1 → f2 ≐ g2 → f ≐ g ≝ ?. -* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2 -cases (after_inv_apply … Hf) -Hf #Hn #Hf -cases (after_inv_apply … Hg) -Hg #Hm #Hg -cases (eq_stream_inv_seq ????? H1) -H1 -cases (eq_stream_inv_seq ????? H2) -H2 -/4 width=8 by apply_eq_repl, tln_eq_repl, eq_seq/ -qed-. - -let corec after_inj: ∀f1,f2,f,g1,g2,g. f1 ⊚ f2 ≡ f → g1 ⊚ g2 ≡ g → - f1 ≐ g1 → f ≐ g → f2 ≐ g2 ≝ ?. -* #n1 #f1 * #n2 #f2 * #n #f * #m1 #g1 * #m2 #g2 * #m #g #Hf #Hg #H1 #H2 -cases (after_inv_apply … Hf) -Hf #Hn #Hf -cases (after_inv_apply … Hg) -Hg #Hm #Hg -cases (eq_stream_inv_seq ????? H1) -H1 #Hnm1 #Hfg1 -cases (eq_stream_inv_seq ????? H2) -H2 #Hnm #Hfg -lapply (apply_inj_aux … Hn Hm Hnm ?) -n -m -/4 width=8 by tln_eq_repl, eq_seq/ -qed-. - -theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f. -/2 width=8 by after_mono/ qed-. - -(* Properties on after ******************************************************) - -lemma after_isid_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ≐ f → 𝐈⦃f1⦄. -#f2 #f1 #f #Ht #H2 @isid_at_total -#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -f1 -/3 width=6 by at_inj, eq_stream_sym/ -qed. - -lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄. -#f2 #f1 #f #Ht #H1 @isid_at_total -#i2 #i #Hi2 lapply (at_total i2 f1) -#H0 lapply (at_increasing … H0) -#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht) -/3 width=7 by at_eq_repl_back, at_mono, at_id_le/ -qed. - -(* Inversion lemmas on after ************************************************) - -let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?. -* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H -/3 width=7 by after_push, after_refl/ -qed-. - -let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?. -* #n2 #f2 * * -[ #f1 #H cases (isid_inv_seq … H) -H - /3 width=7 by after_refl/ -| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/ -] -qed-. - -lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f. -/3 width=8 by isid_after_sn, after_mono/ -qed-. - -lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f. -/3 width=8 by isid_after_dx, after_mono/ -qed-. - -axiom after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄. +lemma after_inv_apply: ∀f1,f2,f,n1,n2,n. n1@f1 ⊚ n2@f2 ≡ n@f → + (n1@f1)@❴n2❵ = n ∧ (↓*[n2]f1) ⊚ f2 ≡ f. +/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma index cec531469..4d979cefb 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma @@ -16,7 +16,7 @@ include "ground_2/relocation/rtmap_eq.ma". (* RELOCATION N-STREAM ******************************************************) -(* Specific properties on eq ************************************************) +(* Specific properties ******************************************************) fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1@f1 ≗ n2@f2 → n1 = n2 ∧ f1 ≗ f2. #f1 #f2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2 diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma index 0001b90b9..d2bd0837e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma @@ -98,8 +98,6 @@ lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵). qed. (* Main inversion lemmas ****************************************************) -(* -lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 → - j1 = j2 → f1 ≗ f2 → i1 = i2. -/2 width=6 by at_inj/ qed-. -*) + +theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2. +/2 width=4 by at_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma index 492a00e91..45a72459e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -220,10 +220,10 @@ let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ] qed-. -(* Properties on minus ******************************************************) +(* Properties on tls ********************************************************) -lemma after_minus: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → - f1 ⊚ f2 ≡ f → f1-n ⊚ f2 ≡ f-n. +lemma after_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 (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/ @@ -385,8 +385,8 @@ cases (after_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H | 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/ +@(after_inj_O_aux (⫱*[n]g1) … (⫱*[n]g)) -after_inj_O_aux +/2 width=1 by after_tls, istot_tls, at_pxx_tls/ qed-. fact after_inj_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1) → 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 3bc16b8ec..00ee4edb2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma @@ -85,8 +85,6 @@ 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) @@ -117,8 +115,7 @@ 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-. -(* --------------------------------------------------------------------------*) - +(* Note: the following inversion lemmas must be checked *) 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. @@ -270,9 +267,9 @@ theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i → #Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/ qed-. -(* Properties on minus ******************************************************) +(* Properties on tls ********************************************************) -lemma at_pxx_minus: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, f-n⦄ ≡ 0. +lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0. #n elim n -n // #n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/ 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 cfe2b3771..5ad6aa83c 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_minus.ma". +include "ground_2/relocation/rtmap_tls.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 07b24f973..d4e80390f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma @@ -36,14 +36,14 @@ qed-. (* Properties on tl *********************************************************) -lemma istot_tl: ∀f. 𝐓⦃f⦄ → 𝐓⦃↓f⦄. +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 ******************************************************) +(* Properties on tls ********************************************************) -lemma istot_minus: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃f-n⦄. +lemma istot_tls: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃⫱*[n]f⦄. #n elim n -n /3 width=1 by istot_tl/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma deleted file mode 100644 index 91f2c8479..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma +++ /dev/null @@ -1,40 +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_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 index 779cc4f6f..588f0d224 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/notation/functions/drop_1.ma". +include "ground_2/notation/functions/droppred_1.ma". include "ground_2/relocation/rtmap_eq.ma". (* RELOCATION MAP ***********************************************************) @@ -21,21 +21,21 @@ definition tl: rtmap → rtmap. @case_type0 #f @f defined. -interpretation "tail (rtmap)" 'Drop f = (tl f). +interpretation "tail (rtmap)" 'DropPred f = (tl f). (* Basic properties *********************************************************) -lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ↓f. +lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ⫱f. // qed. -lemma tl_push_rew: ∀f. f = ↓↑f. +lemma tl_push_rew: ∀f. f = ⫱↑f. #f + + Platform-independent multiple relocation (rtmap). + Multiple relocation with streams of naturals. @@ -19,7 +22,7 @@ Multiple relocation with lists of booleans. - Natural numbers with infinity. + Natural numbers with infinity (ynat). Specification starts. 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 d35679f25..699d0767b 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,10 +23,12 @@ table { class "grass" [ { "multiple relocation" * } { [ { "" * } { - [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] - [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] + [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "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 ( ? ∘ ? )" * ] +(* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] +*) [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma index 8d17df7ff..07fed2a50 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/notation/functions/predecessor_1.ma". -include "ground_2/lib/arith.ma". include "ground_2/ynat/ynat.ma". (* NATURAL NUMBERS WITH INFINITY ********************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma index be5bef707..f08e63293 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/notation/functions/successor_1.ma". include "ground_2/ynat/ynat_pred.ma". (* NATURAL NUMBERS WITH INFINITY ********************************************) diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index d4f38b0ba..768850779 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1505,14 +1505,14 @@ let load_predefined_virtuals () = let predefined_classes = [ ["&"; "⅋"; ]; ["|"; "∥"; ]; - ["!"; "¡"; "⫯"; "⫰"; ]; + ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ]; ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; ["+"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⊟"; ]; - ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ]; + ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≗"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ; @@ -1520,7 +1520,7 @@ let predefined_classes = [ ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; - ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ]; + ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "（"; ]; @@ -1533,7 +1533,7 @@ let predefined_classes = [ ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; - ["∨"; "⩖"; "⋓"; ] ; + ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;