From: Ferruccio Guidi Date: Thu, 4 Feb 2016 15:35:23 +0000 (+0000) Subject: - ground_2: relocation with nstream is now based on two basic functions (push and... X-Git-Tag: make_still_working~650 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a961a1237063702ed9c32a9a4b7994671cb40818;p=helm.git - ground_2: relocation with nstream is now based on two basic functions (push and next) - matex: scope management completed! stylesheet improved (also with colors) --- diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index b2117aa5e..0cfb11087 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -128,14 +128,14 @@ let mk_open st ris = if st.n = "" then ris else T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris -let mk_dec w s ris = +let mk_dec kind w s ris = let w = if !G.no_types then [] else w in - T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: ris + T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris let mk_inferred st c t ris = let u = typeof c t in let is_u = proc_term c u in - mk_dec is_u st.n ris + mk_dec "DECL" is_u st.n ris let rec proc_proof st ris c t = match t with | C.Appl [] @@ -149,7 +149,7 @@ let rec proc_proof st ris c t = match t with let s = alpha c s in let is_w = proc_term c w in let ris = mk_open st ris in - proc_proof (next st) (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t + proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t | C.Appl ts -> let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in let ris = T.Macro "STEP" :: mk_inferred st c t ris in @@ -166,7 +166,8 @@ let rec proc_proof st ris c t = match t with let ris = mk_open st ris in if A.not_prop1 c w then let is_v = proc_term c v in - proc_proof (next st) (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t + let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in + proc_proof (next st) ris (K.add_def s w v c) t else let ris_v = proc_proof (push st s) ris c v in proc_proof (next st) ris_v (K.add_def s w v c) t diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 505d68176..0785eea92 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,10 +1,21 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{matex}[2015/12/21 MaTeX Package] +\ProvidesPackage{matex}[2016/02/03 MaTeX Package] +\RequirePackage{xcolor} \ExecuteOptions{} \ProcessOptions* \makeatletter +\definecolor{ma@black}{HTML}{000000} +\definecolor{ma@blue}{HTML}{00005F} +\definecolor{ma@purple}{HTML}{3F005F} + +\newcommand*\ma@fwd{ma@black} +\newcommand*\ma@open{ma@blue} +\newcommand*\ma@exit{ma@blue} +\newcommand*\ma@prim{ma@purple} +\newcommand*\ma@qed{ma@blue} + \newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}} \newcommand*\ObjLabel[1]{\label{obj:#1}} @@ -12,7 +23,7 @@ \newtheorem{prop}{Proposition} \newenvironment{proof}{\setlength\parindent{0pt}}{} -\newenvironment{ma@step}{}{\vskip0pt} +\newenvironment{ma@step}[1]{\color{#1}}{\\} \newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}} @@ -37,14 +48,20 @@ \newcommand*\ma@with{ with } \newcommand*\ma@comma{, } \newcommand*\ma@stop{.\end{ma@step}} +\newcommand*\ma@head[4]{\def\ma@tmp{#4}% + \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{#2}% + \else\begin{ma@step}{#3}\textbf{#4}% + \fi +} +\newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop} -\newcommand*\DECL[3]{\def\ma@tmp{#1}\begin{ma@step}\textbf{\ifx\ma@tmp\empty\_conlusion\else #1\fi} of type #3} -\newcommand*\PRIM{\end{ma@step}} -\newcommand*\BODY[1]{\\is #1\end{ma@step}} -\newcommand*\STEP[1]{\\by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop} -\newcommand*\DEST[1]{\\by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop} -\newcommand*\OPEN[3]{\begin{ma@step}\textbf{#1} is the following scope #3.\end{ma@step}} -\newcommand*\EXIT[1]{\begin{ma@step}\textbf{end} of scope #1.\end{ma@step}} +\newcommand*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop} +\newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop} +\newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop} +\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\\} +\newcommand*\BODY[1]{being #1\ma@stop} +\newcommand*\STEP[1]{by #1\ma@tail} +\newcommand*\DEST[1]{by cases on #1\ma@tail} \makeatother 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 ae7add375..79e028a99 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -19,26 +19,20 @@ include "ground_2/relocation/nstream_at.ma". (* RELOCATION N-STREAM ******************************************************) let corec compose: rtmap → rtmap → rtmap ≝ ?. -#f1 * #b2 #f2 @(seq … (f1@❴b2❵)) @(compose ? f2) -compose -f2 -@(tln … (⫯b2) f1) -qed. +#f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2 +@(tln … (⫯n2) f1) +defined. interpretation "functional composition (nstream)" 'compose f1 f2 = (compose f1 f2). coinductive after: relation3 rtmap rtmap rtmap ≝ -| after_zero: ∀f1,f2,f,b1,b2,b. - after f1 f2 f → - b1 = 0 → b2 = 0 → b = 0 → - after (b1@f1) (b2@f2) (b@f) -| after_skip: ∀f1,f2,f,b1,b2,b,a2,a. - after f1 (a2@f2) (a@f) → - b1 = 0 → b2 = ⫯a2 → b = ⫯a → - after (b1@f1) (b2@f2) (b@f) -| after_drop: ∀f1,f2,f,b1,b,a1,a. - after (a1@f1) f2 (a@f) → - b1 = ⫯a1 → b = ⫯a → - after (b1@f1) f2 (b@f) +| 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)" @@ -46,70 +40,70 @@ interpretation "relational composition (nstream)" (* Basic properies on compose ***********************************************) -lemma compose_unfold: ∀f1,f2,a2. f1∘(a2@f2) = f1@❴a2❵@tln … (⫯a2) f1∘f2. -#f1 #f2 #a2 >(stream_expand … (f1∘(a2@f2))) normalize // +lemma compose_unfold: ∀f1,f2,n2. f1∘(n2@f2) = f1@❴n2❵@tln … (⫯n2) f1∘f2. +#f1 #f2 #n2 >(stream_expand … (f1∘(n2@f2))) normalize // qed. -lemma compose_drop: ∀f1,f2,f,a1,a. (a1@f1)∘f2 = a@f → (⫯a1@f1)∘f2 = ⫯a@f. -#f1 * #a2 #f2 #f #a1 #a >compose_unfold >compose_unfold +lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f. +* #n1 #f1 * #n2 #f2 #f >compose_unfold >compose_unfold #H destruct normalize // qed. (* Basic inversion lemmas on compose ****************************************) -lemma compose_inv_unfold: ∀f1,f2,f,a2,a. f1∘(a2@f2) = a@f → - f1@❴a2❵ = a ∧ tln … (⫯a2) f1∘f2 = f. -#f1 #f2 #f #a2 #a >(stream_expand … (f1∘(a2@f2))) normalize +lemma compose_inv_unfold: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f → + f1@❴n2❵ = n ∧ tln … (⫯n2) f1∘f2 = f. +#f1 #f2 #f #n2 #n >(stream_expand … (f1∘(n2@f2))) normalize #H destruct /2 width=1 by conj/ qed-. -lemma compose_inv_O2: ∀f1,f2,f,a1,a. (a1@f1)∘(O@f2) = a@f → - a = a1 ∧ f1∘f2 = f. -#f1 #f2 #f #a1 #a >compose_unfold +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 #H destruct /2 width=1 by conj/ qed-. -lemma compose_inv_S2: ∀f1,f2,f,a1,a2,a. (a1@f1)∘(⫯a2@f2) = a@f → - a = ⫯(a1+f1@❴a2❵) ∧ f1∘(a2@f2) = f1@❴a2❵@f. -#f1 #f2 #f #a1 #a2 #a >compose_unfold +lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f → + n = ⫯(n1+f1@❴n2❵) ∧ f1∘(n2@f2) = f1@❴n2❵@f. +#f1 #f2 #f #n1 #n2 #n >compose_unfold #H destruct /2 width=1 by conj/ qed-. -lemma compose_inv_S1: ∀f1,f2,f,a1,a2,a. (⫯a1@f1)∘(a2@f2) = a@f → - a = ⫯((a1@f1)@❴a2❵) ∧ (a1@f1)∘(a2@f2) = (a1@f1)@❴a2❵@f. -#f1 #f2 #f #a1 #a2 #a >compose_unfold +lemma compose_inv_S1: ∀f1,f2,f,n1,n2,n. (⫯n1@f1)∘(n2@f2) = n@f → + n = ⫯((n1@f1)@❴n2❵) ∧ (n1@f1)∘(n2@f2) = (n1@f1)@❴n2❵@f. +#f1 #f2 #f #n1 #n2 #n >compose_unfold #H destruct /2 width=1 by conj/ qed-. (* Basic properties on after ************************************************) lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → - ∀b. b@f1 ⊚ O@f2 ≡ b@f. -#f1 #f2 #f #Ht #b elim b -b /2 width=5 by after_drop, after_zero/ + ∀n. n@f1 ⊚ ↑f2 ≡ n@f. +#f1 #f2 #f #Ht #n elim n -n /2 width=7 by after_refl, after_next/ qed. -lemma after_S2: ∀f1,f2,f,b2,b. f1 ⊚ b2@f2 ≡ b@f → - ∀b1. b1@f1 ⊚ ⫯b2@f2 ≡ ⫯(b1+b)@f. -#f1 #f2 #f #b2 #b #Ht #b1 elim b1 -b1 /2 width=5 by after_drop, after_skip/ +lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → + ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f. +#f1 #f2 #f #n2 #n #Ht #n1 elim n1 -n1 /2 width=7 by after_next, after_push/ qed. -lemma after_apply: ∀b2,f1,f2,f. (tln … (⫯b2) f1) ⊚ f2 ≡ f → f1 ⊚ b2@f2 ≡ f1@❴b2❵@f. -#b2 elim b2 -b2 +lemma after_apply: ∀n2,f1,f2,f. (tln … (⫯n2) f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f. +#n2 elim n2 -n2 [ * /2 width=1 by after_O2/ -| #b2 #IH * /3 width=1 by after_S2/ +| #n2 #IH * /3 width=1 by after_S2/ ] qed-. let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?. -* #a1 #f1 * #a2 #f2 * #a #f cases a1 -a1 -[ cases a2 -a2 +* #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1 +[ cases n2 -n2 [ #H cases (compose_inv_O2 … H) -H - /3 width=1 by after_zero/ - | #a2 #H cases (compose_inv_S2 … H) -H - /3 width=5 by after_skip, eq_f/ + /3 width=7 by after_refl, eq_f2/ + | #n2 #H cases (compose_inv_S2 … H) -H + /3 width=7 by after_push/ ] -| #a1 #H cases (compose_inv_S1 … H) -H - /3 width=5 by after_drop, eq_f/ +| #n1 #H cases (compose_inv_S1 … H) -H + /4 width=7 by after_next, next_rew_sn/ ] qed-. @@ -118,167 +112,179 @@ theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2. (* Basic inversion lemmas on after ******************************************) -fact after_inv_O1_aux: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1. f1 = 0@g1 → - (∃∃g2,g. g1 ⊚ g2 ≡ g & f2 = 0@g2 & f = 0@g) ∨ - ∃∃g2,g,b2,b. g1 ⊚ b2@g2 ≡ b@g & f2 = ⫯b2@g2 & f = ⫯b@g. -#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1 -[ #b2 #b #Ht #H1 #H2 #H3 #g1 #H destruct /3 width=5 by ex3_2_intro, or_introl/ -| #b2 #b #a2 #a #Ht #H1 #H2 #H3 #g1 #H destruct /3 width=7 by ex3_4_intro, or_intror/ -| #b #a1 #a #_ #H1 #H3 #g1 #H destruct +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-. -fact after_inv_O1_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → - (∧∧ f1 ⊚ f2 ≡ f & b2 = 0 & b = 0) ∨ - ∃∃a2,a. f1 ⊚ a2@f2 ≡ a@f & b2 = ⫯a2 & b = ⫯a. -#f1 #f2 #f #b1 #b2 #b #Ht #H elim (after_inv_O1_aux … Ht) -Ht [4: // |2: skip ] * -[ #g2 #g #Hu #H1 #H2 destruct /3 width=1 by and3_intro, or_introl/ -| #g2 #g #a2 #a #Hu #H1 #H2 destruct /3 width=5 by ex3_2_intro, or_intror/ +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_O1: ∀g1,f2,f. 0@g1 ⊚ f2 ≡ f → - (∃∃g2,g. g1 ⊚ g2 ≡ g & f2 = 0@g2 & f = 0@g) ∨ - ∃∃g2,g,b2,b. g1 ⊚ b2@g2 ≡ b@g & f2 = ⫯b2@g2 & f = ⫯b@g. -/2 width=3 by after_inv_O1_aux/ 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_zero_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → b2 = 0 → - f1 ⊚ f2 ≡ f ∧ b = 0. -#f1 #f2 #f #b1 #b2 #b #Ht #H1 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 * -[ /2 width=1 by conj/ -| #a1 #a2 #_ #H0 destruct +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_zero: ∀g1,g2,f. 0@g1 ⊚ 0@g2 ≡ f → - ∃∃g. g1 ⊚ g2 ≡ g & f = 0@g. -#g1 #g2 #f #H elim (after_inv_O1 … H) -H * -[ #x2 #g #Hu #H1 #H2 destruct /2 width=3 by ex2_intro/ -| #x2 #g #a2 #a #Hu #H destruct -] -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-. -fact after_inv_skip_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b1 = 0 → ∀a2. b2 = ⫯a2 → - ∃∃a. f1 ⊚ a2@f2 ≡ a@f & b = ⫯a. -#f1 #f2 #f #b1 #b2 #b #Ht #H1 #a2 #H2 elim (after_inv_O1_aux2 … Ht H1) -Ht -H1 * -[ #_ #H0 destruct -| #x2 #x #H #H0 #H1 destruct /2 width=3 by ex2_intro/ -] -qed-. +(* Advanced inversion lemmas on after ***************************************) -lemma after_inv_skip: ∀g1,g2,f,b2. 0@g1 ⊚ ⫯b2@g2 ≡ f → - ∃∃g,b. g1 ⊚ b2@g2 ≡ b@g & f = ⫯b@g. -#g1 #g2 * #b #f #b2 #Ht elim (after_inv_skip_aux2 … Ht) [2,4: // |3: skip ] -Ht -#a #Ht #H destruct /2 width=4 by ex2_2_intro/ +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_S1_aux: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,b1. f1 = ⫯b1@g1 → - ∃∃g,b. b1@g1 ⊚ f2 ≡ b@g & f = ⫯b@g. -#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1 -[ #b2 #b #_ #H1 #H2 #H3 #g1 #a1 #H destruct -| #b2 #b #a2 #a #_ #H1 #H2 #H3 #g1 #a1 #H destruct -| #b #a1 #a #Ht #H1 #H3 #g1 #x1 #H destruct /2 width=4 by ex2_2_intro/ -] +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_S1_aux2: ∀f1,f2,f,b1,b. b1@f1 ⊚ f2 ≡ b@f → ∀a1. b1 = ⫯a1 → - ∃∃a. a1@f1 ⊚ f2 ≡ a@f & b = ⫯a. -#f1 #f2 #f #b1 #b #Ht #a #H elim (after_inv_S1_aux … Ht) -Ht [4: // |2,3: skip ] -#g #x #Hu #H0 destruct /2 width=3 by ex2_intro/ +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-. -lemma after_inv_S1: ∀g1,f2,f,b1. ⫯b1@g1 ⊚ f2 ≡ f → - ∃∃g,b. b1@g1 ⊚ f2 ≡ b@g & f = ⫯b@g. -/2 width=3 by after_inv_S1_aux/ qed-. - -fact after_inv_drop_aux2: ∀f1,f2,f,a1,a. a1@f1 ⊚ f2 ≡ a@f → ∀b1,b. a1 = ⫯b1 → a = ⫯b → - b1@f1 ⊚ f2 ≡ b@f. -#f1 #f2 #f #a1 #a #Ht #b1 #b #H1 #H elim (after_inv_S1_aux2 … Ht … H1) -a1 -#x #Ht #Hx destruct // +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-. -lemma after_inv_drop: ∀f1,f2,f,b1,b. ⫯b1@f1 ⊚ f2 ≡ ⫯b@f → b1@f1 ⊚ f2 ≡ b@f. -/2 width=5 by after_inv_drop_aux2/ 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_O3_aux1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g. f = 0@g → - ∃∃g1,g2. g1 ⊚ g2 ≡ g & f1 = 0@g1 & f2 = 0@g2. -#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1 -[ #b2 #b #Ht #H1 #H2 #H3 #g #H destruct /2 width=5 by ex3_2_intro/ -| #b2 #b #a2 #a #_ #H1 #H2 #H3 #g #H destruct -| #b #a1 #a #_ #H1 #H3 #g #H destruct -] +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_O3_aux2: ∀f1,f2,f,b1,b2,b. b1@f1 ⊚ b2@f2 ≡ b@f → b = 0 → - ∧∧ f1 ⊚ f2 ≡ f & b1 = 0 & b2 = 0. -#f1 #f2 #f #b1 #b2 #b #Ht #H1 elim (after_inv_O3_aux1 … Ht) [2: // |3: skip ] -b -#g1 #g2 #Ht #H1 #H2 destruct /2 width=1 by and3_intro/ +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-. -lemma after_inv_O3: ∀f1,f2,g. f1 ⊚ f2 ≡ 0@g → - ∃∃g1,g2. g1 ⊚ g2 ≡ g & f1 = 0@g1 & f2 = 0@g2. -/2 width=3 by after_inv_O3_aux1/ qed-. +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_S3_aux1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g,b. f = ⫯b@g → - (∃∃g1,g2,b2. g1 ⊚ b2@g2 ≡ b@g & f1 = 0@g1 & f2 = ⫯b2@g2) ∨ - ∃∃g1,b1. b1@g1 ⊚ f2 ≡ b@g & f1 = ⫯b1@g1. -#f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #b1 -[ #b2 #b #_ #H1 #H2 #H3 #g #a #H destruct -| #b2 #b #a2 #a #HT #H1 #H2 #H3 #g #x #H destruct /3 width=6 by ex3_3_intro, or_introl/ -| #b #a1 #a #HT #H1 #H3 #g #x #H destruct /3 width=4 by ex2_2_intro, or_intror/ +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_S3_aux2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → ∀b. a = ⫯b → - (∃∃b2. f1 ⊚ b2@f2 ≡ b@f & a1 = 0 & a2 = ⫯b2) ∨ - ∃∃b1. b1@f1 ⊚ a2@f2 ≡ b@f & a1 = ⫯b1. -#f1 #f2 #f #a1 #a2 #a #Ht #b #H elim (after_inv_S3_aux1 … Ht) [3: // |4,5: skip ] -a * -[ #g1 #g2 #b2 #Ht #H1 #H2 destruct /3 width=3 by ex3_intro, or_introl/ -| #g1 #b1 #Ht #H1 destruct /3 width=3 by ex2_intro, or_intror/ +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_S3: ∀f1,f2,g,b. f1 ⊚ f2 ≡ ⫯b@g → - (∃∃g1,g2,b2. g1 ⊚ b2@g2 ≡ b@g & f1 = 0@g1 & f2 = ⫯b2@g2) ∨ - ∃∃g1,b1. b1@g1 ⊚ f2 ≡ b@g & f1 = ⫯b1@g1. -/2 width=3 by after_inv_S3_aux1/ qed-. - -(* Advanced inversion lemmas on after ***************************************) +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_O2_aux2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ a2@f2 ≡ a@f → a2 = 0 → - a1 = a ∧ f1 ⊚ f2 ≡ f. -#f1 #f2 #f #a1 #a2 elim a1 -a1 -[ #a #H #H2 elim (after_inv_zero_aux2 … H … H2) -a2 /2 width=1 by conj/ -| #a1 #IH #a #H #H2 elim (after_inv_S1_aux2 … H) -H [3: // |2: skip ] - #b #H #H1 elim (IH … H) // -a2 - #H2 destruct /2 width=1 by conj/ +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_O2: ∀f1,g2,f. f1 ⊚ 0@g2 ≡ f → - ∃∃g1,g,a. f1 = a@g1 & f = a@g & g1 ⊚ g2 ≡ g. -* #a1 #f1 #f2 * #a #f #H elim (after_inv_O2_aux2 … H) -H // -/2 width=6 by ex3_3_intro/ +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_xOx_aux: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. g2 = ↑f2 → + 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 + #H destruct /2 width=1 by conj/ +] qed-. -lemma after_inv_const: ∀a,f1,b2,g2,f. a@f1 ⊚ b2@g2 ≡ a@f → b2 = 0. -#a elim a -a -[ #f1 #b2 #g2 #f #H elim (after_inv_O3 … H) -H - #g1 #x2 #_ #_ #H destruct // -| #a #IH #f1 #b2 #g2 #f #H elim (after_inv_S1 … H) -H - #x #b #Hx #H destruct >(IH … Hx) -f1 -g2 -x -b2 -b // +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). +#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 + #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 ] + #m #Hf #Hm destruct /2 width=3 by ex2_intro/ ] qed-. -lemma after_inv_S2: ∀f1,f2,f,a1,a2,a. a1@f1 ⊚ ⫯a2@f2 ≡ a@f → ∀b. a = ⫯(a1+b) → - f1 ⊚ a2@f2 ≡ b@f. -#f1 #f2 #f #a1 elim a1 -a1 -[ #a2 #a #Ht #b #Hb - elim (after_inv_skip_aux2 … Ht) -Ht [3,4: // |2: skip ] - #c #Ht #Hc destruct // -| #a1 #IH #a2 #a #Ht #b #Hb - lapply (after_inv_drop_aux2 … Ht … Hb) -a [ // | skip ] - /2 width=3 by/ +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. +#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-. @@ -287,16 +293,16 @@ qed-. 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_O3 … H) -H - /2 width=3 by at_zero, ex2_intro/ -| #f #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_O3 … H) -H - #g2 #g1 #Hu #H1 #H2 destruct elim (IH … Hu) -f +[ #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 #b #i1 #i #_ #IH #f2 #f1 #H elim (after_inv_S3 … H) -H * - [ #g2 #g1 #b2 #Hu #H1 #H2 destruct elim (IH … Hu) -f -b - /3 width=3 by at_S1, at_lift, ex2_intro/ - | #g1 #b1 #Hu #H destruct elim (IH … Hu) -f -b - /3 width=3 by at_lift, 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/ ] ] qed-. @@ -304,23 +310,12 @@ 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 #f2 #f #H elim (after_inv_O2 … H) -H /2 width=3 by ex2_intro/ -| #f1 #i1 #i2 #_ #IH * #b2 elim b2 -b2 - [ #f2 #f #H elim (after_inv_zero … H) -H - #g #Hu #H destruct elim (IH … Hu) -f1 - /3 width=3 by at_S1, at_skip, ex2_intro/ - | -IH #b2 #IH #f2 #f #H elim (after_inv_S1 … H) -H - #g #b #Hu #H destruct elim (IH … Hu) -f1 - /3 width=3 by at_lift, ex2_intro/ - ] -| #f1 #b1 #i1 #i2 #_ #IH * #b2 elim b2 -b2 - [ #f2 #f #H elim (after_inv_skip … H) -H - #g #a #Hu #H destruct elim (IH … Hu) -f1 -b1 - /3 width=3 by at_S1, at_lift, ex2_intro/ - | -IH #b2 #IH #f2 #f #H elim (after_inv_S1 … H) -H - #g #b #Hu #H destruct elim (IH … Hu) -f1 -b1 - /3 width=3 by at_lift, ex2_intro/ - ] +[ #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-. @@ -339,99 +334,104 @@ qed-. lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i. #f #i1 #i #H elim H -f -i1 -i -[ #f #f1 #i2 #Ht1 #f2 #H elim (after_inv_O3 … H) -H +[ #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_O3 … H) -H +| #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_skip/ -| #f #b #i1 #i #_ #IH #f1 #i2 #Ht1 #f2 #H elim (after_inv_S3 … H) -H * - [ #g2 #g1 #a1 #Hu #H1 #H2 destruct elim (at_inv_xSx … Ht1) -Ht1 - /3 width=3 by at_skip/ - | #g2 #a2 #Hu #H destruct /3 width=3 by at_lift/ + /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,a2,a. f1 ⊚ a2@f2 ≡ a@f → a = f1@❴a2❵. -#f1 #f2 #f #a2 #a #Ht lapply (after_fwd_at … 0 … Ht) -Ht [4: // | // |2,3: skip ] +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 ] /3 width=2 by at_inv_O1, sym_eq/ qed-. -lemma after_fwd_tl: ∀f,f2,a2,f1,a1,a. a1@f1 ⊚ a2@f2 ≡ a@f → - tln … a2 f1 ⊚ f2 ≡ f. -#f #f2 #a2 elim a2 -a2 -[ #f1 #a1 #a #Ht elim (after_inv_O2_aux2 … Ht) -Ht // -| #a2 #IH * #b1 #f1 #a1 #a #Ht - lapply (after_fwd_hd … Ht) #Ha - lapply (after_inv_S2 … Ht … Ha) -a - /2 width=3 by/ +lemma after_fwd_tl: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f → + tln … 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 ] + #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-. +/3 width=3 by after_fwd_tl, after_fwd_hd, conj/ qed-. (* Main properties on after *************************************************) -let corec after_trans1: ∀f1,f2,f0. f1 ⊚ f2 ≡ f0 → - ∀f3,f4. f0 ⊚ f3 ≡ f4 → +let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → + ∀f1,f2. f1 ⊚ f2 ≡ f0 → ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?. -#f1 #f2 #f0 * -f1 -f2 -f0 #f1 #f2 #f0 #b1 [1,2: #b2 ] #b0 -[ #Ht0 #H1 #H2 #H0 * #b3 #f3 * #b4 #f4 #Ht4 * #b #f #Ht - cases (after_inv_O1_aux2 … Ht4 H0) -Ht4 -H0 * - [ #Ht4 #H3 #H4 cases (after_inv_zero_aux2 … Ht H2 H3) -Ht -H2 -H3 - #Ht #H /3 width=6 by after_zero/ - | #a0 #a4 #Ht4 #H3 #H4 cases (after_inv_skip_aux2 … Ht H2 … H3) -Ht -H2 -H3 - #a #Ht3 #H /3 width=6 by after_skip/ +#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/ ] -| #a2 #a0 #Ht0 #H1 #H2 #H0 #f3 * #b4 #f4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0 - #a4 #Ht4 #H4 * #b #f #H cases (after_inv_S1_aux2 … H … H2) -H -H2 - #a #Ht3 #H /3 width=6 by after_skip/ -| #a1 #a0 #Ht0 #H1 #H0 #f3 * #b4 #f4 #Ht4 cases (after_inv_S1_aux2 … Ht4 … H0) -Ht4 -H0 - #a4 #Ht4 #H4 * #b #f #Ht /3 width=6 by after_drop/ ] 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 #b1 [1,2: #b0 ] #b4 -[ #Ht4 #H1 #H0 #H4 * #b2 #f2 * #b3 #f3 #Ht0 * #b #f #Ht - cases (after_inv_O3_aux2 … Ht0 H0) -b0 - #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2 - #Ht #H /3 width=6 by after_zero/ -| #a0 #a4 #Ht4 #H1 #H0 #H4 * #b2 #f2 * #b3 #f3 #Ht0 * #b #f #Ht - cases (after_inv_S3_aux2 … Ht0 … H0) -b0 * - [ #a3 #Ht0 #H2 #H3 cases (after_inv_zero_aux2 … Ht H1 H2) -b1 -b2 - #Ht #H /3 width=6 by after_skip/ - | #a2 #Ht0 #H2 cases (after_inv_skip_aux2 … Ht H1 … H2) -b1 -b2 - #a #Ht #H /3 width=6 by after_drop/ +#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/ ] -| #a1 #a4 #Ht4 #H1 #H4 * #b2 #f2 * #b3 #f3 #Ht0 * #b #f #Ht - cases (after_inv_S1_aux2 … Ht … H1) -b1 - #a #Ht #H /3 width=6 by after_drop/ +| #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,x. f1 ⊚ f2 ≡ x → ∀y. f1 ⊚ f2 ≡ y → x ≐ y ≝ ?. -* #a1 #f1 * #a2 #f2 * #c #x #Hx * #d #y #Hy -cases (after_inv_apply … Hx) -Hx #Hc #Hx -cases (after_inv_apply … Hy) -Hy #Hd #Hy +* #n1 #f1 * #n2 #f2 * #n #x #Hx * #m #y #Hy +cases (after_inv_apply … Hx) -Hx #Hn #Hx +cases (after_inv_apply … Hy) -Hy #Hm #Hy /3 width=4 by eq_seq/ qed-. let corec after_inj: ∀f1,x,f. f1 ⊚ x ≡ f → ∀y. f1 ⊚ y ≡ f → x ≐ y ≝ ?. -* #a1 #f1 * #c #x * #a #f #Hx * #d #y #Hy -cases (after_inv_apply … Hx) -Hx #Hc #Hx -cases (after_inv_apply … Hy) -Hy #Hd -cases (apply_inj_aux … Hc Hd) // -#Hy -a -d /3 width=4 by eq_seq/ +* #n1 #f1 * #n2 #x * #n #f #Hx * #m2 #y #Hy +cases (after_inv_apply … Hx) -Hx #Hn2 #Hx +cases (after_inv_apply … Hy) -Hy #Hm2 +cases (apply_inj_aux … Hn2 Hm2) -n -m2 /3 width=4 by eq_seq/ qed-. -(* Main inversion lemmas on after *******************************************) - theorem after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≐ f. /2 width=4 by after_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma index a40ba30ad..8fd1da8a7 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma @@ -14,25 +14,25 @@ include "ground_2/notation/functions/apply_2.ma". include "ground_2/notation/relations/rat_3.ma". -include "ground_2/relocation/nstream.ma". +include "ground_2/relocation/nstream_lift.ma". (* RELOCATION N-STREAM ******************************************************) let rec apply (i: nat) on i: rtmap → nat ≝ ?. -* #b #f cases i -i -[ @b +* #n #f cases i -i +[ @n | #i lapply (apply i f) -apply -i -f - #i @(⫯(b+i)) + #i @(⫯(n+i)) ] -qed. +defined. interpretation "functional application (nstream)" 'Apply f i = (apply i f). inductive at: rtmap → relation nat ≝ -| at_zero: ∀f. at (0 @ f) 0 0 -| at_skip: ∀f,i1,i2. at f i1 i2 → at (0 @ f) (⫯i1) (⫯i2) -| at_lift: ∀f,b,i1,i2. at (b @ f) i1 i2 → at (⫯b @ f) i1 (⫯i2) +| at_refl: ∀f. at (↑f) 0 0 +| at_push: ∀f,i1,i2. at f i1 i2 → at (↑f) (⫯i1) (⫯i2) +| at_next: ∀f,i1,i2. at f i1 i2 → at (⫯f) i1 (⫯i2) . interpretation "relational application (nstream)" @@ -40,122 +40,123 @@ interpretation "relational application (nstream)" (* Basic properties on apply ************************************************) -lemma apply_S1: ∀f,a,i. (⫯a@f)@❴i❵ = ⫯((a@f)@❴i❵). -#a #f * // +lemma apply_S1: ∀f,n,i. (⫯n@f)@❴i❵ = ⫯((n@f)@❴i❵). +#n #f * // qed. (* Basic inversion lemmas on at *********************************************) -fact at_inv_xOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. f = 0@g → - (i1 = 0 ∧ i2 = 0) ∨ - ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2. -#f #i1 #i2 * -f -i1 -i2 -[ /3 width=1 by or_introl, conj/ -| #f #i1 #i2 #Hi #g #H destruct /3 width=5 by ex3_2_intro, or_intror/ -| #f #b #i1 #i2 #_ #g #H destruct +fact at_inv_OOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. i1 = 0 → f = ↑g → i2 = 0. +#f #i1 #i2 * -f -i1 -i2 // +[ #f #i1 #i2 #_ #g #H destruct +| #f #i1 #i2 #_ #g #_ #H elim (discr_next_push … H) ] qed-. -lemma at_inv_xOx: ∀f,i1,i2. @⦃i1, 0@f⦄ ≡ i2 → - (i1 = 0 ∧ i2 = 0) ∨ - ∃∃j1,j2. @⦃j1, f⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2. -/2 width=3 by at_inv_xOx_aux/ qed-. +lemma at_inv_OOx: ∀f,i2. @⦃0, ↑f⦄ ≡ i2 → i2 = 0. +/2 width=6 by at_inv_OOx_aux/ qed-. -lemma at_inv_OOx: ∀f,i. @⦃0, 0 @ f⦄ ≡ i → i = 0. -#f #i #H elim (at_inv_xOx … H) -H * // -#j1 #j2 #_ #H destruct +fact at_inv_SOx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j1. i1 = ⫯j1 → f = ↑g → + ∃∃j2. @⦃j1, g⦄ ≡ j2 & i2 = ⫯j2. +#f #i1 #i2 * -f -i1 -i2 +[ #f #g #j1 #H destruct +| #f #i1 #i2 #Hi #g #j1 #H #Hf <(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/ +| #f #i1 #i2 #_ #g #j1 #_ #H elim (discr_next_push … H) +] qed-. -lemma at_inv_xOO: ∀f,i. @⦃i, 0@f⦄ ≡ 0 → i = 0. -#f #i #H elim (at_inv_xOx … H) -H * // -#j1 #j2 #_ #_ #H destruct +lemma at_inv_SOx: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ i2 → + ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2. +/2 width=5 by at_inv_SOx_aux/ qed-. + +fact at_inv_xSx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. f = ⫯g → + ∃∃j2. @⦃i1, g⦄ ≡ j2 & i2 = ⫯j2. +#f #i1 #i2 * -f -i1 -i2 +[ #f #g #H elim (discr_push_next … H) +| #f #i1 #i2 #_ #g #H elim (discr_push_next … H) +| #f #i1 #i2 #Hi #g #H <(injective_next … H) -g /2 width=3 by ex2_intro/ +] qed-. -lemma at_inv_SOx: ∀f,i1,i2. @⦃⫯i1, 0@f⦄ ≡ i2 → +lemma at_inv_xSx: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ i2 → ∃∃j2. @⦃i1, f⦄ ≡ j2 & i2 = ⫯j2. -#f #i1 #i2 #H elim (at_inv_xOx … H) -H * -[ #H destruct -| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/ -] +/2 width=3 by at_inv_xSx_aux/ qed-. + +(* Advanced inversion lemmas on at ******************************************) + +lemma at_inv_OOS: ∀f,i2. @⦃0, ↑f⦄ ≡ ⫯i2 → ⊥. +#f #i2 #H lapply (at_inv_OOx … H) -H +#H destruct qed-. -lemma at_inv_xOS: ∀f,i1,i2. @⦃i1, 0@f⦄ ≡ ⫯i2 → - ∃∃j1. @⦃j1, f⦄ ≡ i2 & i1 = ⫯j1. -#f #i1 #i2 #H elim (at_inv_xOx … H) -H * -[ #_ #H destruct -| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/ -] +lemma at_inv_SOS: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. +#f #i1 #i2 #H elim (at_inv_SOx … H) -H +#j2 #H2 #H destruct // qed-. -lemma at_inv_SOS: ∀f,i1,i2. @⦃⫯i1, 0@f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. -#f #i1 #i2 #H elim (at_inv_xOx … H) -H * -[ #H destruct -| #j1 #j2 #Hj #H1 #H2 destruct // -] +lemma at_inv_SOO: ∀f,i1. @⦃⫯i1, ↑f⦄ ≡ 0 → ⊥. +#f #i1 #H elim (at_inv_SOx … H) -H +#j2 #_ #H destruct qed-. -lemma at_inv_OOS: ∀f,i. @⦃0, 0@f⦄ ≡ ⫯i → ⊥. -#f #i #H elim (at_inv_xOx … H) -H * -[ #_ #H destruct -| #j1 #j2 #_ #H destruct -] +lemma at_inv_xSS: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. +#f #i1 #i2 #H elim (at_inv_xSx … H) -H +#j2 #H #H2 destruct // qed-. -lemma at_inv_SOO: ∀f,i. @⦃⫯i, 0@f⦄ ≡ 0 → ⊥. -#f #i #H elim (at_inv_xOx … H) -H * -[ #H destruct -| #j1 #j2 #_ #_ #H destruct -] +lemma at_inv_xSO: ∀f,i1. @⦃i1, ⫯f⦄ ≡ 0 → ⊥. +#f #i1 #H elim (at_inv_xSx … H) -H +#j2 #_ #H destruct qed-. -fact at_inv_xSx_aux: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,a. f = ⫯a @ g → - ∃∃j2. @⦃i1, a@g⦄ ≡ j2 & i2 = ⫯j2. -#f #i1 #i2 * -f -i1 -i2 -[ #f #g #a #H destruct -| #f #i1 #i2 #_ #g #a #H destruct -| #f #b #i1 #i2 #Hi #g #a #H destruct /2 width=3 by ex2_intro/ +lemma at_inv_xOx: ∀f,i1,i2. @⦃i1, ↑f⦄ ≡ i2 → + (i1 = 0 ∧ i2 = 0) ∨ + ∃∃j1,j2. @⦃j1, f⦄ ≡ j2 & i1 = ⫯j1 & i2 = ⫯j2. +#f * [2: #i1 ] #i2 #H +[ elim (at_inv_SOx … H) -H + #j2 #H2 #H destruct /3 width=5 by or_intror, ex3_2_intro/ +| >(at_inv_OOx … H) -i2 /3 width=1 by conj, or_introl/ ] qed-. -lemma at_inv_xSx: ∀f,b,i1,i2. @⦃i1, ⫯b@f⦄ ≡ i2 → - ∃∃j2. @⦃i1, b@f⦄ ≡ j2 & i2 = ⫯j2. -/2 width=3 by at_inv_xSx_aux/ qed-. - -lemma at_inv_xSS: ∀f,b,i1,i2. @⦃i1, ⫯b @ f⦄ ≡ ⫯i2 → @⦃i1, b@f⦄ ≡ i2. -#f #b #i1 #i2 #H elim (at_inv_xSx … H) -H -#j2 #Hj #H destruct // +lemma at_inv_xOO: ∀f,i. @⦃i, ↑f⦄ ≡ 0 → i = 0. +#f #i #H elim (at_inv_xOx … H) -H * // +#j1 #j2 #_ #_ #H destruct qed-. -lemma at_inv_xSO: ∀f,b,i. @⦃i, ⫯b@f⦄ ≡ 0 → ⊥. -#f #b #i #H elim (at_inv_xSx … H) -H -#j2 #_ #H destruct +lemma at_inv_xOS: ∀f,i1,i2. @⦃i1, ↑f⦄ ≡ ⫯i2 → + ∃∃j1. @⦃j1, f⦄ ≡ i2 & i1 = ⫯j1. +#f #i1 #i2 #H elim (at_inv_xOx … H) -H * +[ #_ #H destruct +| #j1 #j2 #Hj #H1 #H2 destruct /2 width=3 by ex2_intro/ +] qed-. (* alternative definition ***************************************************) -lemma at_O1: ∀b,f. @⦃0, b@f⦄ ≡ b. -#b elim b -b /2 width=1 by at_lift/ +lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≡ i2. +#i2 elim i2 -i2 /2 width=1 by at_refl, at_next/ qed. -lemma at_S1: ∀b,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, b@f⦄ ≡ ⫯(b+i2). -#b elim b -b /3 width=1 by at_skip, at_lift/ +lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, n@f⦄ ≡ ⫯(n+i2). +#n elim n -n /3 width=1 by at_push, at_next/ qed. -lemma at_inv_O1: ∀f,b,i2. @⦃0, b@f⦄ ≡ i2 → i2 = b. -#f #b elim b -b /2 width=2 by at_inv_OOx/ -#b #IH #i2 #H elim (at_inv_xSx … H) -H +lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≡ i2 → i2 = n. +#f #n elim n -n /2 width=2 by at_inv_OOx/ +#n #IH #i2 (at_inv_O1 … H) -i2 // | #i1 #i2 #H elim (at_inv_S1 … H) -H #j1 #Ht #H destruct @@ -174,41 +175,49 @@ lemma at_increasing_plus: ∀f,b,i1,i2. @⦃i1, b@f⦄ ≡ i2 → i1 + b ≤ i2. ] qed-. -lemma at_increasing_strict: ∀f,b,i1,i2. @⦃i1, ⫯b @ f⦄ ≡ i2 → - i1 < i2 ∧ @⦃i1, b@f⦄ ≡ ⫰i2. -#f #b #i1 #i2 #H elim (at_inv_xSx … H) -H +lemma at_increasing_strict: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ i2 → + i1 < i2 ∧ @⦃i1, f⦄ ≡ ⫰i2. +#f #i1 #i2 #H elim (at_inv_xSx … H) -H #j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/ qed-. -lemma at_fwd_id: ∀f,b,i. @⦃i, b@f⦄ ≡ i → b = 0. -#f #b * -[ #H <(at_inv_O1 … H) -f -b // +lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≡ i → n = 0. +#f #n * +[ #H <(at_inv_O1 … H) -f -n // | #i #H elim (at_inv_S1 … H) -H #j #H #H0 destruct lapply (at_increasing … H) -H #H lapply (eq_minus_O … H) -H // ] +qed-. + +(* Basic properties on at ***************************************************) + +lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i. +#f #i1 #i #n #m #H elim m -m /2 width=1 by at_next/ qed. -(* Main properties on at ****************************************************) +(* Advanced properties on at ************************************************) lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1. #i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ] -* #b #f #H lapply (at_fwd_id … H) +* #n #f #H lapply (at_fwd_id … H) #H0 destruct /4 width=1 by at_S1, at_inv_SOS/ qed-. +(* Main properties on at ****************************************************) + let corec at_ext: ∀f1,f2. (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≐ f2 ≝ ?. -* #b1 #f1 * #b2 #f2 #Hi lapply (Hi 0 b1 b2 ? ?) // +* #n1 #f1 * #n2 #f2 #Hi lapply (Hi 0 n1 n2 ? ?) // #H lapply (at_ext f1 f2 ?) /2 width=1 by eq_seq/ -at_ext -#j #j1 #j2 #H1 #H2 @(injective_plus_r … b2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *) +#j #j1 #j2 #H1 #H2 @(injective_plus_r … n2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *) qed-. theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀f1,f2. f1 ≐ f2 → ∀j1,j2. @⦃i1, f1⦄ ≡ j1 → @⦃i2, f2⦄ ≡ j2 → j1 < j2. #i1 #i2 #H @(lt_elim … H) -i1 -i2 -[ #i2 * #b1 #f1 * #b2 #f2 #H elim (eq_stream_inv_seq ????? H) -H +[ #i2 * #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H #H #Ht #j1 #j2 #H1 #H2 destruct >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 // -| #i1 #i2 #IH * #b1 #f1 * #b2 #f2 #H elim (eq_stream_inv_seq ????? H) -H +| #i1 #i2 #IH * #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H #H #Ht #j1 #j2 #H1 #H2 destruct elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2 #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=5 by lt_S_S, monotonic_lt_plus_r/ @@ -218,13 +227,13 @@ qed-. theorem at_inv_monotonic: ∀f1,i1,j1. @⦃i1, f1⦄ ≡ j1 → ∀f2,i2,j2. @⦃i2, f2⦄ ≡ j2 → f1 ≐ f2 → j2 < j1 → i2 < i1. #f1 #i1 #j1 #H elim H -f1 -i1 -j1 [ #f1 #f2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) // -| #f1 #i1 #j1 #_ #IH * #b2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht +| #f1 #i1 #j1 #_ #IH * #n2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht #H0 #Ht destruct elim (at_inv_xOx … H) -H * [ #H1 #H2 destruct // | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=5 by lt_S_S_to_lt, lt_S_S/ ] -| #f1 #b1 #i1 #j1 #_ #IH * #b2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht - #H0 #Ht destruct elim (at_inv_xSx … H) -H +| * #n1 #f1 #i1 #j1 #_ #IH * #n2 #f2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht + #H0 #Ht destruct id_unfold in ⊢ (???%→?); +lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ n = 0. +#f #n normalize >id_unfold in ⊢ (???%→?); #H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/ qed-. lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄. -* #a #f #H elim (isid_inv_seq … H) -H // +* #n #f #H elim (isid_inv_seq … H) -H // qed-. lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥. -* #a #f #H elim (isid_inv_seq … H) -H +* #n #f #H elim (isid_inv_seq … H) -H #_ #H destruct qed-. (* inversion lemmas on at ***************************************************) let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?. -* #a #f #Ht lapply (Ht 0) +* #n #f #Ht lapply (Ht 0) #H lapply (at_inv_O1 … H) -H #H0 >id_unfold @eq_seq -[ cases H0 -a // +[ cases H0 -n // | @id_inv_at -id_inv_at - #i lapply (Ht (⫯i)) -Ht cases H0 -a + #i lapply (Ht (⫯i)) -Ht cases H0 -n #H elim (at_inv_SOx … H) -H // ] qed-. lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i. #i elim i -i -[ * #a #f #H elim (isid_inv_seq … H) -H // -| #i #IH * #a #f #H elim (isid_inv_seq … H) -H +[ * #n #f #H elim (isid_inv_seq … H) -H // +| #i #IH * #n #f #H elim (isid_inv_seq … H) -H /3 width=1 by at_S1/ ] qed-. @@ -117,18 +116,15 @@ qed. (* Inversion lemmas on after ************************************************) let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?. -* #a1 #f1 * * [ | #a2 ] #f2 #H cases (isid_inv_seq … H) -H -#Ht1 #H1 -[ @(after_zero … H1) -H1 /2 width=1 by/ -| @(after_skip … H1) -H1 /2 width=5 by/ -] +* #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 ≝ ?. -* #a2 #f2 * * +* #n2 #f2 * * [ #f1 #H cases (isid_inv_seq … H) -H - #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/ -| #a1 #f1 #H @(after_drop … a1 a1) /2 width=5 by/ + /3 width=7 by after_refl/ +| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma index e98d8bee1..4e2f20bf6 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/functions/lift_1.ma". -include "ground_2/relocation/nstream_at.ma". +include "ground_2/relocation/nstream.ma". (* RELOCATION N-STREAM ******************************************************) @@ -22,23 +22,23 @@ definition push: rtmap → rtmap ≝ λf. 0@f. interpretation "push (nstream)" 'Lift f = (push f). definition next: rtmap → rtmap. -* #a #f @(⫯a@f) +* #n #f @(⫯n@f) qed. interpretation "next (nstream)" 'Successor f = (next f). -(* Basic properties on push *************************************************) +(* Basic properties *********************************************************) -lemma push_at_O: ∀f. @⦃0, ↑f⦄ ≡ 0. +lemma push_rew: ∀f. ↑f = 0@f. // qed. -lemma push_at_S: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃⫯i1, ↑f⦄ ≡ ⫯i2. -/2 width=1 by at_S1/ qed. +lemma next_rew: ∀f,n. ⫯(n@f) = (⫯n)@f. +// qed. -(* Basic inversion lemmas on push *******************************************) +lemma next_rew_sn: ∀f,n1,n2. n1 = ⫯n2 → n1@f = ⫯(n2@f). +// qed. -lemma push_inv_at_S: ∀f,i1,i2. @⦃⫯i1, ↑f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. -/2 width=1 by at_inv_SOS/ qed-. +(* Basic inversion lemmas ***************************************************) lemma injective_push: injective ? ? push. #f1 #f2 normalize #H destruct // @@ -52,18 +52,22 @@ lemma discr_next_push: ∀f1,f2. ⫯f1 = ↑f2 → ⊥. * #n1 #f1 #f2 normalize #H destruct qed-. -(* Basic properties on next *************************************************) +lemma injective_next: injective ? ? next. +* #n1 #f1 * #n2 #f2 normalize #H destruct // +qed-. -lemma next_at: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → @⦃i1, ⫯f⦄ ≡ ⫯i2. -* /2 width=1 by at_lift/ -qed. +lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → n = 0 ∧ g = f. +#f #g #n >push_rew #H destruct /2 width=1 by conj/ +qed-. -(* Basic inversion lemmas on next *******************************************) +lemma push_inv_seq_dx: ∀f,g,n. ↑f = n@g → n = 0 ∧ g = f. +#f #g #n >push_rew #H destruct /2 width=1 by conj/ +qed-. -lemma next_inv_at: ∀f,i1,i2. @⦃i1, ⫯f⦄ ≡ ⫯i2 → @⦃i1, f⦄ ≡ i2. -* /2 width=1 by at_inv_xSS/ +lemma next_inv_seq_sn: ∀f,g,n. n@g = ⫯f → ∃∃m. n = ⫯m & f = m@g. +* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/ qed-. -lemma injective_next: injective ? ? next. -* #a1 #f1 * #a2 #f2 normalize #H destruct // +lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. n = ⫯m & f = m@g. +* #m #f #g #n >next_rew #H destruct /2 width=3 by ex2_intro/ 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 50896c56c..39f75c7b6 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 @@ -12,7 +12,7 @@ table { class "green" [ { "multiple relocation" * } { [ { "" * } { - [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ] + [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ] [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]