From 802e118337ebd0f8b732d4939973aae6415b5bec Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Feb 2016 17:45:09 +0000 Subject: [PATCH] - ground_2: support for relocation updated - basic_2: theory of relocation updated - MaTeX: (co)inductive types are now processed --- matita/components/binaries/matex/Makefile | 5 +- .../components/binaries/matex/anticipate.ml | 1 - matita/components/binaries/matex/engine.ml | 12 +- .../components/binaries/matex/test/test.tex | 39 ++- .../lambdadelta/basic_2/relocation/lifts.ma | 308 ++++++++++-------- .../basic_2/relocation/lifts_lifts.ma | 96 +++--- .../basic_2/relocation/lifts_lifts_vector.ma | 36 +- .../basic_2/relocation/lifts_simple.ma | 12 +- .../basic_2/relocation/lifts_vector.ma | 114 ++++--- .../basic_2/relocation/lifts_weight.ma | 4 +- .../lambdadelta/ground_2/lib/streams.ma | 7 +- .../lambdadelta/ground_2/lib/streams_hdtl.ma | 6 + .../ground_2/relocation/nstream_after.ma | 33 +- .../ground_2/relocation/nstream_at.ma | 19 +- .../ground_2/relocation/nstream_id.ma | 20 +- .../ground_2/relocation/nstream_lift.ma | 40 +++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 20 +- 17 files changed, 455 insertions(+), 317 deletions(-) diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index 4e1e3ca66..42cf1c181 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -8,10 +8,11 @@ include ../Makefile.common REGISTRY = $(RT_BASE_DIR)/matita.conf.xml OBJS = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con\ - cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con + cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con\ + cic:/matita/lambdadelta/basic_1/pr0/defs/pr0.ind test: - @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%.con=%) + @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%=%) $(H)./matex.native -O test -t -p $(REGISTRY) $(OBJS) .PHONY: test diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml index 1081dffcc..47fc2cae1 100644 --- a/matita/components/binaries/matex/anticipate.ml +++ b/matita/components/binaries/matex/anticipate.ml @@ -121,7 +121,6 @@ try with | T.TypeCheckerFailure s | T.AssertFailure s -> malformed (Lazy.force s) - | Invalid_argument "List.nth" -> malformed "4" (* to be removed *) let proc_fun c = let r, s, i, u, t = c in diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 0cfb11087..6053456ca 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -42,9 +42,6 @@ let internal s = let malformed s = X.error ("engine: malformed term: " ^ s) -let not_supported () = - X.error "engine: object not supported" - (* generic term processing *) let proc_sort = function @@ -213,13 +210,20 @@ let proc_pair s ss u xt = let proc_fun ss (r, s, i, u, t) = proc_pair s (s :: ss) u (Some t) +let proc_constructor ss (r, s, u) = + proc_pair s (s :: ss) u None + +let proc_type ss (r, s, u, cs) = + proc_pair s (s :: ss) u None; + L.iter (proc_constructor ss) cs + let proc_obj u = let ss = K.segments_of_uri u in let _, _, _, _, obj = E.get_checked_obj G.status u in match obj with | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs - | C.Inductive (_, _, _, _) -> not_supported () + | C.Inductive (_, _, ts, _) -> L.iter (proc_type ss) ts (* interface functions ******************************************************) diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index 80f765652..057a1f54b 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -6,11 +6,43 @@ \begin{document} -\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type.tex} +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type} \bigskip -\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body.tex} +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_comp.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_delta.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_refl.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_tau.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_upsilon.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_zeta.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body} \bigskip @@ -20,6 +52,9 @@ \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} +\bigskip + +\ObjRef{pr0} \ObjRef{pr0_ind} \ObjRef{pr0_confluence} diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma index 6a66289bd..45cd021eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/relocation/trace_isid.ma". +include "ground_2/relocation/nstream_id.ma". include "basic_2/notation/relations/rliftstar_3.ma". include "basic_2/grammar/term.ma". @@ -22,16 +22,16 @@ include "basic_2/grammar/term.ma". lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat lifts_nil lifts_cons *) -inductive lifts: trace → relation term ≝ -| lifts_sort: ∀k,t. lifts t (⋆k) (⋆k) -| lifts_lref: ∀i1,i2,t. @⦃i1, t⦄ ≡ i2 → lifts t (#i1) (#i2) -| lifts_gref: ∀p,t. lifts t (§p) (§p) -| lifts_bind: ∀a,I,V1,V2,T1,T2,t. - lifts t V1 V2 → lifts (Ⓣ@t) T1 T2 → - lifts t (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) -| lifts_flat: ∀I,V1,V2,T1,T2,t. - lifts t V1 V2 → lifts t T1 T2 → - lifts t (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) +inductive lifts: rtmap → relation term ≝ +| lifts_sort: ∀s,f. lifts f (⋆s) (⋆s) +| lifts_lref: ∀i1,i2,f. @⦃i1, f⦄ ≡ i2 → lifts f (#i1) (#i2) +| lifts_gref: ∀l,f. lifts f (§l) (§l) +| lifts_bind: ∀p,I,V1,V2,T1,T2,f. + lifts f V1 V2 → lifts (↑f) T1 T2 → + lifts f (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) +| lifts_flat: ∀I,V1,V2,T1,T2,f. + lifts f V1 V2 → lifts f T1 T2 → + lifts f (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) . interpretation "generic relocation (term)" @@ -39,180 +39,180 @@ interpretation "generic relocation (term)" (* Basic inversion lemmas ***************************************************) -fact lifts_inv_sort1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀k. X = ⋆k → Y = ⋆k. -#X #Y #t * -X -Y -t // -[ #i1 #i2 #t #_ #x #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct -| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct +fact lifts_inv_sort1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀s. X = ⋆s → Y = ⋆s. +#X #Y #f * -X -Y -f // +[ #i1 #i2 #f #_ #x #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct +| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct ] qed-. (* Basic_1: was: lift1_sort *) (* Basic_2A1: includes: lift_inv_sort1 *) -lemma lifts_inv_sort1: ∀Y,k,t. ⬆*[t] ⋆k ≡ Y → Y = ⋆k. +lemma lifts_inv_sort1: ∀Y,s,f. ⬆*[f] ⋆s ≡ Y → Y = ⋆s. /2 width=4 by lifts_inv_sort1_aux/ qed-. -fact lifts_inv_lref1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀i1. X = #i1 → - ∃∃i2. @⦃i1, t⦄ ≡ i2 & Y = #i2. -#X #Y #t * -X -Y -t -[ #k #t #x #H destruct -| #i1 #i2 #t #Hi12 #x #H destruct /2 width=3 by ex2_intro/ -| #p #t #x #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct -| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct +fact lifts_inv_lref1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀i1. X = #i1 → + ∃∃i2. @⦃i1, f⦄ ≡ i2 & Y = #i2. +#X #Y #f * -X -Y -f +[ #s #f #x #H destruct +| #i1 #i2 #f #Hi12 #x #H destruct /2 width=3 by ex2_intro/ +| #l #f #x #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct +| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct ] qed-. (* Basic_1: was: lift1_lref *) (* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *) -lemma lifts_inv_lref1: ∀Y,i1,t. ⬆*[t] #i1 ≡ Y → - ∃∃i2. @⦃i1, t⦄ ≡ i2 & Y = #i2. +lemma lifts_inv_lref1: ∀Y,i1,f. ⬆*[f] #i1 ≡ Y → + ∃∃i2. @⦃i1, f⦄ ≡ i2 & Y = #i2. /2 width=3 by lifts_inv_lref1_aux/ qed-. -fact lifts_inv_gref1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀p. X = §p → Y = §p. -#X #Y #t * -X -Y -t // -[ #i1 #i2 #t #_ #x #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct -| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct +fact lifts_inv_gref1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀l. X = §l → Y = §l. +#X #Y #f * -X -Y -f // +[ #i1 #i2 #f #_ #x #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct +| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct ] qed-. (* Basic_2A1: includes: lift_inv_gref1 *) -lemma lifts_inv_gref1: ∀Y,p,t. ⬆*[t] §p ≡ Y → Y = §p. +lemma lifts_inv_gref1: ∀Y,l,f. ⬆*[f] §l ≡ Y → Y = §l. /2 width=4 by lifts_inv_gref1_aux/ qed-. -fact lifts_inv_bind1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → - ∀a,I,V1,T1. X = ⓑ{a,I}V1.T1 → - ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 & - Y = ⓑ{a,I}V2.T2. -#X #Y #t * -X -Y -t -[ #k #t #b #J #W1 #U1 #H destruct -| #i1 #i2 #t #_ #b #J #W1 #U1 #H destruct -| #p #t #b #J #W1 #U1 #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #b #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/ -| #I #V1 #V2 #T1 #T2 #t #_ #_ #b #J #W1 #U1 #H destruct +fact lifts_inv_bind1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → + ∀p,I,V1,T1. X = ⓑ{p,I}V1.T1 → + ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 & + Y = ⓑ{p,I}V2.T2. +#X #Y #f * -X -Y -f +[ #s #f #q #J #W1 #U1 #H destruct +| #i1 #i2 #f #_ #q #J #W1 #U1 #H destruct +| #l #f #b #J #W1 #U1 #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #q #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/ +| #I #V1 #V2 #T1 #T2 #f #_ #_ #q #J #W1 #U1 #H destruct ] qed-. (* Basic_1: was: lift1_bind *) (* Basic_2A1: includes: lift_inv_bind1 *) -lemma lifts_inv_bind1: ∀a,I,V1,T1,Y,t. ⬆*[t] ⓑ{a,I}V1.T1 ≡ Y → - ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 & - Y = ⓑ{a,I}V2.T2. +lemma lifts_inv_bind1: ∀p,I,V1,T1,Y,f. ⬆*[f] ⓑ{p,I}V1.T1 ≡ Y → + ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 & + Y = ⓑ{p,I}V2.T2. /2 width=3 by lifts_inv_bind1_aux/ qed-. -fact lifts_inv_flat1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → +fact lifts_inv_flat1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀I,V1,T1. X = ⓕ{I}V1.T1 → - ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 & + ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 & Y = ⓕ{I}V2.T2. -#X #Y #t * -X -Y -t -[ #k #t #J #W1 #U1 #H destruct -| #i1 #i2 #t #_ #J #W1 #U1 #H destruct -| #p #t #J #W1 #U1 #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #J #W1 #U1 #H destruct -| #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/ +#X #Y #f * -X -Y -f +[ #s #f #J #W1 #U1 #H destruct +| #i1 #i2 #f #_ #J #W1 #U1 #H destruct +| #l #f #J #W1 #U1 #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #J #W1 #U1 #H destruct +| #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_1: was: lift1_flat *) (* Basic_2A1: includes: lift_inv_flat1 *) -lemma lifts_inv_flat1: ∀I,V1,T1,Y,t. ⬆*[t] ⓕ{I}V1.T1 ≡ Y → - ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 & +lemma lifts_inv_flat1: ∀I,V1,T1,Y,f. ⬆*[f] ⓕ{I}V1.T1 ≡ Y → + ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 & Y = ⓕ{I}V2.T2. /2 width=3 by lifts_inv_flat1_aux/ qed-. -fact lifts_inv_sort2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀k. Y = ⋆k → X = ⋆k. -#X #Y #t * -X -Y -t // -[ #i1 #i2 #t #_ #x #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct -| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct +fact lifts_inv_sort2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀s. Y = ⋆s → X = ⋆s. +#X #Y #f * -X -Y -f // +[ #i1 #i2 #f #_ #x #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct +| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct ] qed-. (* Basic_1: includes: lift_gen_sort *) (* Basic_2A1: includes: lift_inv_sort2 *) -lemma lifts_inv_sort2: ∀X,k,t. ⬆*[t] X ≡ ⋆k → X = ⋆k. +lemma lifts_inv_sort2: ∀X,s,f. ⬆*[f] X ≡ ⋆s → X = ⋆s. /2 width=4 by lifts_inv_sort2_aux/ qed-. -fact lifts_inv_lref2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀i2. Y = #i2 → - ∃∃i1. @⦃i1, t⦄ ≡ i2 & X = #i1. -#X #Y #t * -X -Y -t -[ #k #t #x #H destruct -| #i1 #i2 #t #Hi12 #x #H destruct /2 width=3 by ex2_intro/ -| #p #t #x #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct -| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct +fact lifts_inv_lref2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀i2. Y = #i2 → + ∃∃i1. @⦃i1, f⦄ ≡ i2 & X = #i1. +#X #Y #f * -X -Y -f +[ #s #f #x #H destruct +| #i1 #i2 #f #Hi12 #x #H destruct /2 width=3 by ex2_intro/ +| #l #f #x #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct +| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct ] qed-. (* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *) (* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *) -lemma lifts_inv_lref2: ∀X,i2,t. ⬆*[t] X ≡ #i2 → - ∃∃i1. @⦃i1, t⦄ ≡ i2 & X = #i1. +lemma lifts_inv_lref2: ∀X,i2,f. ⬆*[f] X ≡ #i2 → + ∃∃i1. @⦃i1, f⦄ ≡ i2 & X = #i1. /2 width=3 by lifts_inv_lref2_aux/ qed-. -fact lifts_inv_gref2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → ∀p. Y = §p → X = §p. -#X #Y #t * -X -Y -t // -[ #i1 #i2 #t #_ #x #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct -| #I #V1 #V2 #T1 #T2 #t #_ #_ #x #H destruct +fact lifts_inv_gref2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀l. Y = §l → X = §l. +#X #Y #f * -X -Y -f // +[ #i1 #i2 #f #_ #x #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct +| #I #V1 #V2 #T1 #T2 #f #_ #_ #x #H destruct ] qed-. (* Basic_2A1: includes: lift_inv_gref1 *) -lemma lifts_inv_gref2: ∀X,p,t. ⬆*[t] X ≡ §p → X = §p. +lemma lifts_inv_gref2: ∀X,l,f. ⬆*[f] X ≡ §l → X = §l. /2 width=4 by lifts_inv_gref2_aux/ qed-. -fact lifts_inv_bind2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → - ∀a,I,V2,T2. Y = ⓑ{a,I}V2.T2 → - ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 & - X = ⓑ{a,I}V1.T1. -#X #Y #t * -X -Y -t -[ #k #t #b #J #W2 #U2 #H destruct -| #i1 #i2 #t #_ #b #J #W2 #U2 #H destruct -| #p #t #b #J #W2 #U2 #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #b #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/ -| #I #V1 #V2 #T1 #T2 #t #_ #_ #b #J #W2 #U2 #H destruct +fact lifts_inv_bind2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → + ∀p,I,V2,T2. Y = ⓑ{p,I}V2.T2 → + ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 & + X = ⓑ{p,I}V1.T1. +#X #Y #f * -X -Y -f +[ #s #f #q #J #W2 #U2 #H destruct +| #i1 #i2 #f #_ #q #J #W2 #U2 #H destruct +| #l #f #q #J #W2 #U2 #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #q #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/ +| #I #V1 #V2 #T1 #T2 #f #_ #_ #q #J #W2 #U2 #H destruct ] qed-. (* Basic_1: includes: lift_gen_bind *) (* Basic_2A1: includes: lift_inv_bind2 *) -lemma lifts_inv_bind2: ∀a,I,V2,T2,X,t. ⬆*[t] X ≡ ⓑ{a,I}V2.T2 → - ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[Ⓣ@t] T1 ≡ T2 & - X = ⓑ{a,I}V1.T1. +lemma lifts_inv_bind2: ∀p,I,V2,T2,X,f. ⬆*[f] X ≡ ⓑ{p,I}V2.T2 → + ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[↑f] T1 ≡ T2 & + X = ⓑ{p,I}V1.T1. /2 width=3 by lifts_inv_bind2_aux/ qed-. -fact lifts_inv_flat2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → +fact lifts_inv_flat2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → ∀I,V2,T2. Y = ⓕ{I}V2.T2 → - ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 & + ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 & X = ⓕ{I}V1.T1. -#X #Y #t * -X -Y -t -[ #k #t #J #W2 #U2 #H destruct -| #i1 #i2 #t #_ #J #W2 #U2 #H destruct -| #p #t #J #W2 #U2 #H destruct -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #J #W2 #U2 #H destruct -| #I #V1 #V2 #T1 #T2 #t #HV12 #HT12 #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/ +#X #Y #f * -X -Y -f +[ #s #f #J #W2 #U2 #H destruct +| #i1 #i2 #f #_ #J #W2 #U2 #H destruct +| #l #f #J #W2 #U2 #H destruct +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #J #W2 #U2 #H destruct +| #I #V1 #V2 #T1 #T2 #f #HV12 #HT12 #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_1: includes: lift_gen_flat *) (* Basic_2A1: includes: lift_inv_flat2 *) -lemma lifts_inv_flat2: ∀I,V2,T2,X,t. ⬆*[t] X ≡ ⓕ{I}V2.T2 → - ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & ⬆*[t] T1 ≡ T2 & +lemma lifts_inv_flat2: ∀I,V2,T2,X,f. ⬆*[f] X ≡ ⓕ{I}V2.T2 → + ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & ⬆*[f] T1 ≡ T2 & X = ⓕ{I}V1.T1. /2 width=3 by lifts_inv_flat2_aux/ qed-. (* Basic_2A1: includes: lift_inv_pair_xy_x *) -lemma lifts_inv_pair_xy_x: ∀I,V,T,t. ⬆*[t] ②{I}V.T ≡ V → ⊥. +lemma lifts_inv_pair_xy_x: ∀I,V,T,f. ⬆*[f] ②{I}V.T ≡ V → ⊥. #J #V elim V -V -[ * #i #U #t #H +[ * #i #U #f #H [ lapply (lifts_inv_sort2 … H) -H #H destruct | elim (lifts_inv_lref2 … H) -H #x #_ #H destruct | lapply (lifts_inv_gref2 … H) -H #H destruct ] -| * [ #a ] #I #V2 #T2 #IHV2 #_ #U #t #H +| * [ #p ] #I #V2 #T2 #IHV2 #_ #U #f #H [ elim (lifts_inv_bind2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/ | elim (lifts_inv_flat2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/ ] @@ -221,15 +221,15 @@ qed-. (* Basic_1: includes: thead_x_lift_y_y *) (* Basic_2A1: includes: lift_inv_pair_xy_y *) -lemma lifts_inv_pair_xy_y: ∀I,T,V,t. ⬆*[t] ②{I}V.T ≡ T → ⊥. +lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⬆*[f] ②{I}V.T ≡ T → ⊥. #J #T elim T -T -[ * #i #W #t #H +[ * #i #W #f #H [ lapply (lifts_inv_sort2 … H) -H #H destruct | elim (lifts_inv_lref2 … H) -H #x #_ #H destruct | lapply (lifts_inv_gref2 … H) -H #H destruct ] -| * [ #a ] #I #V2 #T2 #_ #IHT2 #W #t #H +| * [ #p ] #I #V2 #T2 #_ #IHT2 #W #f #H [ elim (lifts_inv_bind2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/ | elim (lifts_inv_flat2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/ ] @@ -239,23 +239,24 @@ qed-. (* Basic forward lemmas *****************************************************) (* Basic_2A1: includes: lift_inv_O2 *) -lemma lifts_fwd_isid: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐈⦃t⦄ → T1 = T2. -#T1 #T2 #t #H elim H -T1 -T2 -t /4 width=3 by isid_inv_at, eq_f2, eq_f/ +lemma lifts_fwd_isid: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐈⦃f⦄ → T1 = T2. +#T1 #T2 #f #H elim H -T1 -T2 -f +/4 width=3 by isid_inv_at_mono, isid_push, eq_f2, eq_f/ qed-. (* Basic_2A1: includes: lift_fwd_pair1 *) -lemma lifts_fwd_pair1: ∀I,V1,T1,Y,t. ⬆*[t] ②{I}V1.T1 ≡ Y → - ∃∃V2,T2. ⬆*[t] V1 ≡ V2 & Y = ②{I}V2.T2. -* [ #a ] #I #V1 #T1 #Y #t #H +lemma lifts_fwd_pair1: ∀I,V1,T1,Y,f. ⬆*[f] ②{I}V1.T1 ≡ Y → + ∃∃V2,T2. ⬆*[f] V1 ≡ V2 & Y = ②{I}V2.T2. +* [ #p ] #I #V1 #T1 #Y #f #H [ elim (lifts_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/ | elim (lifts_inv_flat1 … H) -H /2 width=4 by ex2_2_intro/ ] qed-. (* Basic_2A1: includes: lift_fwd_pair2 *) -lemma lifts_fwd_pair2: ∀I,V2,T2,X,t. ⬆*[t] X ≡ ②{I}V2.T2 → - ∃∃V1,T1. ⬆*[t] V1 ≡ V2 & X = ②{I}V1.T1. -* [ #a ] #I #V2 #T2 #X #t #H +lemma lifts_fwd_pair2: ∀I,V2,T2,X,f. ⬆*[f] X ≡ ②{I}V2.T2 → + ∃∃V1,T1. ⬆*[f] V1 ≡ V2 & X = ②{I}V1.T1. +* [ #p ] #I #V2 #T2 #X #f #H [ elim (lifts_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/ | elim (lifts_inv_flat2 … H) -H /2 width=4 by ex2_2_intro/ ] @@ -263,38 +264,65 @@ qed-. (* Basic properties *********************************************************) +lemma lifts_eq_repl_back: ∀T1,T2. eq_stream_repl_back … (λf. ⬆*[f] T1 ≡ T2). +#T1 #T2 #f1 #H elim H -T1 -T2 -f1 +/4 width=3 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, push_eq_repl/ +qed-. + +lemma lifts_eq_repl_fwd: ∀T1,T2. eq_stream_repl_fwd … (λf. ⬆*[f] T1 ≡ T2). +#T1 #T2 @eq_stream_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *) +qed-. + +(* Basic_1: includes: lift_r *) +(* Basic_2A1: includes: lift_refl *) +lemma lifts_refl: ∀T,f. 𝐈⦃f⦄ → ⬆*[f] T ≡ T. +#T elim T -T * +/4 width=1 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/ +qed. + +(* Basic_2A1: includes: lift_total *) +lemma lifts_total: ∀T1,f. ∃T2. ⬆*[f] T1 ≡ T2. +#T1 elim T1 -T1 * +/3 width=2 by lifts_lref, lifts_sort, lifts_gref, ex_intro/ +[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f +elim (IHV1 f) -IHV1 #V2 #HV12 +[ elim (IHT1 (↑f)) -IHT1 /3 width=2 by lifts_bind, ex_intro/ +| elim (IHT1 f) -IHT1 /3 width=2 by lifts_flat, ex_intro/ +] +qed-. + (* Basic_1: includes: lift_free (right to left) *) (* Basic_2A1: includes: lift_split *) -lemma lifts_split_trans: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → - ∀t1,t2. t2 ⊚ t1 ≡ t → - ∃∃T. ⬆*[t1] T1 ≡ T & ⬆*[t2] T ≡ T2. -#T1 #T2 #t #H elim H -T1 -T2 -t +lemma lifts_split_trans: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → + ∀f1,f2. f2 ⊚ f1 ≡ f → + ∃∃T. ⬆*[f1] T1 ≡ T & ⬆*[f2] T ≡ T2. +#T1 #T2 #f #H elim H -T1 -T2 -f [ /3 width=3 by lifts_sort, ex2_intro/ -| #i1 #i2 #t #Hi #t1 #t2 #Ht elim (after_at_fwd … Ht … Hi) -Ht -Hi +| #i1 #i2 #f #Hi #f1 #f2 #Ht elim (after_at_fwd … Hi … Ht) -Hi -Ht /3 width=3 by lifts_lref, ex2_intro/ | /3 width=3 by lifts_gref, ex2_intro/ -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV #IHT #t1 #t2 #Ht - elim (IHV … Ht) elim (IHT (Ⓣ@t1) (Ⓣ@t2)) -IHV -IHT - /3 width=5 by lifts_bind, after_true, ex2_intro/ -| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV #IHT #t1 #t2 #Ht +| #p #I #V1 #V2 #T1 #T2 #f #_ #_ #IHV #IHT #f1 #f2 #Ht + elim (IHV … Ht) elim (IHT (↑f1) (↑f2)) -IHV -IHT + /3 width=5 by lifts_bind, after_O2, ex2_intro/ +| #I #V1 #V2 #T1 #T2 #f #_ #_ #IHV #IHT #f1 #f2 #Ht elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht /3 width=5 by lifts_flat, ex2_intro/ ] qed-. (* Note: apparently, this was missing in Basic_2A1 *) -lemma lifts_split_div: ∀T1,T2,t1. ⬆*[t1] T1 ≡ T2 → - ∀t2,t. t2 ⊚ t1 ≡ t → - ∃∃T. ⬆*[t2] T2 ≡ T & ⬆*[t] T1 ≡ T. -#T1 #T2 #t1 #H elim H -T1 -T2 -t1 +lemma lifts_split_div: ∀T1,T2,f1. ⬆*[f1] T1 ≡ T2 → + ∀f2,f. f2 ⊚ f1 ≡ f → + ∃∃T. ⬆*[f2] T2 ≡ T & ⬆*[f] T1 ≡ T. +#T1 #T2 #f1 #H elim H -T1 -T2 -f1 [ /3 width=3 by lifts_sort, ex2_intro/ -| #i1 #i2 #t1 #Hi #t2 #t #Ht elim (after_at1_fwd … Ht … Hi) -Ht -Hi +| #i1 #i2 #f1 #Hi #f2 #f #Ht elim (after_at1_fwd … Hi … Ht) -Hi -Ht /3 width=3 by lifts_lref, ex2_intro/ | /3 width=3 by lifts_gref, ex2_intro/ -| #a #I #V1 #V2 #T1 #T2 #t1 #_ #_ #IHV #IHT #t2 #t #Ht - elim (IHV … Ht) elim (IHT (Ⓣ@t2) (Ⓣ@t)) -IHV -IHT - /3 width=5 by lifts_bind, after_true, ex2_intro/ -| #I #V1 #V2 #T1 #T2 #t1 #_ #_ #IHV #IHT #t2 #t #Ht +| #p #I #V1 #V2 #T1 #T2 #f1 #_ #_ #IHV #IHT #f2 #f #Ht + elim (IHV … Ht) elim (IHT (↑f2) (↑f)) -IHV -IHT + /3 width=5 by lifts_bind, after_O2, ex2_intro/ +| #I #V1 #V2 #T1 #T2 #f1 #_ #_ #IHV #IHT #f2 #f #Ht elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht /3 width=5 by lifts_flat, ex2_intro/ ] @@ -302,18 +330,18 @@ qed-. (* Basic_1: includes: dnf_dec2 dnf_dec *) (* Basic_2A1: includes: is_lift_dec *) -lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2). +lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⬆*[f] T1 ≡ T2). #T1 elim T1 -T1 [ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ] - #i2 #t elim (is_at_dec t i2) + #i2 #f elim (is_at_dec f i2) [ * /4 width=3 by lifts_lref, ex_intro, or_introl/ | #H @or_intror * #X #HX elim (lifts_inv_lref2 … HX) -HX /3 width=2 by ex_intro/ ] -| * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #t - [ elim (IHV2 t) -IHV2 - [ * #V1 #HV12 elim (IHT2 (Ⓣ@t)) -IHT2 +| * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f + [ elim (IHV2 f) -IHV2 + [ * #V1 #HV12 elim (IHT2 (↑f)) -IHT2 [ * #T1 #HT12 @or_introl /3 width=2 by lifts_bind, ex_intro/ | -V1 #HT2 @or_intror * #X #H elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/ @@ -321,8 +349,8 @@ lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2). | -IHT2 #HV2 @or_intror * #X #H elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/ ] - | elim (IHV2 t) -IHV2 - [ * #V1 #HV12 elim (IHT2 t) -IHT2 + | elim (IHV2 f) -IHV2 + [ * #V1 #HV12 elim (IHT2 f) -IHT2 [ * #T1 #HT12 /4 width=2 by lifts_flat, ex_intro, or_introl/ | -V1 #HT2 @or_intror * #X #H elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma index 3ac75012c..2372488aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma @@ -18,84 +18,70 @@ include "basic_2/relocation/lifts.ma". (* Main properties **********************************************************) -(* Basic_2A1: includes: lift_inj *) -theorem lifts_inj: ∀t,T1,U. ⬆*[t] T1 ≡ U → ∀T2. ⬆*[t] T2 ≡ U → T1 = T2. -#t #T1 #U #H elim H -t -T1 -U -[ /2 width=2 by lifts_inv_sort2/ -| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref2 … HX) -HX - /4 width=4 by at_inj, eq_f/ -| /2 width=2 by lifts_inv_gref2/ -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind2 … HX) -HX - #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/ -| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat2 … HX) -HX - #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/ -] -qed-. - (* Basic_1: includes: lift_gen_lift *) (* Basic_2A1: includes: lift_div_le lift_div_be *) -theorem lifts_div: ∀T,T2,t2. ⬆*[t2] T2 ≡ T → ∀T1,t. ⬆*[t] T1 ≡ T → - ∀t1. t2 ⊚ t1 ≡ t → ⬆*[t1] T1 ≡ T2. -#T #T2 #t2 #H elim H -T -T2 -t2 -[ #k #t2 #T1 #t #H >(lifts_inv_sort2 … H) -T1 // -| #i2 #i #t2 #Hi2 #T1 #t #H #t1 #Ht21 elim (lifts_inv_lref2 … H) -H +theorem lifts_div: ∀T,T2,f2. ⬆*[f2] T2 ≡ T → ∀T1,f. ⬆*[f] T1 ≡ T → + ∀f1. f2 ⊚ f1 ≡ f → ⬆*[f1] T1 ≡ T2. +#T #T2 #f2 #H elim H -T -T2 -f2 +[ #s #f2 #T1 #f #H >(lifts_inv_sort2 … H) -T1 // +| #i2 #i #f2 #Hi2 #T1 #f #H #f1 #Ht21 elim (lifts_inv_lref2 … H) -H #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, after_fwd_at1/ -| #p #t2 #T1 #t #H >(lifts_inv_gref2 … H) -T1 // -| #a #I #W2 #W #U2 #U #t2 #_ #_ #IHW #IHU #T1 #t #H +| #l #f2 #T1 #f #H >(lifts_inv_gref2 … H) -T1 // +| #p #I #W2 #W #U2 #U #f2 #_ #_ #IHW #IHU #T1 #f #H elim (lifts_inv_bind2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct - /4 width=3 by lifts_bind, after_true/ -| #I #W2 #W #U2 #U #t2 #_ #_ #IHW #IHU #T1 #t #H + /4 width=3 by lifts_bind, after_O2/ +| #I #W2 #W #U2 #U #f2 #_ #_ #IHW #IHU #T1 #f #H elim (lifts_inv_flat2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct /3 width=3 by lifts_flat/ ] qed-. -(* Basic_2A1: includes: lift_mono *) -theorem lifts_mono: ∀t,T,U1. ⬆*[t] T ≡ U1 → ∀U2. ⬆*[t] T ≡ U2 → U1 = U2. -#t #T #U1 #H elim H -t -T -U1 -[ /2 width=2 by lifts_inv_sort1/ -| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref1 … HX) -HX - /4 width=4 by at_mono, eq_f/ -| /2 width=2 by lifts_inv_gref1/ -| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind1 … HX) -HX - #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/ -| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat1 … HX) -HX - #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/ -] -qed-. - (* Basic_1: was: lift1_lift1 (left to right) *) (* Basic_1: includes: lift_free (left to right) lift_d lift1_xhg (right to left) lift1_free (right to left) *) (* Basic_2A1: includes: lift_trans_be lift_trans_le lift_trans_ge lifts_lift_trans_le lifts_lift_trans *) -theorem lifts_trans: ∀T1,T,t1. ⬆*[t1] T1 ≡ T → ∀T2,t2. ⬆*[t2] T ≡ T2 → - ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1 ≡ T2. -#T1 #T #t1 #H elim H -T1 -T -t1 -[ #k #t1 #T2 #t2 #H >(lifts_inv_sort1 … H) -T2 // -| #i1 #i #t1 #Hi1 #T2 #t2 #H #t #Ht21 elim (lifts_inv_lref1 … H) -H +theorem lifts_trans: ∀T1,T,f1. ⬆*[f1] T1 ≡ T → ∀T2,f2. ⬆*[f2] T ≡ T2 → + ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1 ≡ T2. +#T1 #T #f1 #H elim H -T1 -T -f1 +[ #s #f1 #T2 #f2 #H >(lifts_inv_sort1 … H) -T2 // +| #i1 #i #f1 #Hi1 #T2 #f2 #H #f #Ht21 elim (lifts_inv_lref1 … H) -H #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at/ -| #p #t1 #T2 #t2 #H >(lifts_inv_gref1 … H) -T2 // -| #a #I #W1 #W #U1 #U #t1 #_ #_ #IHW #IHU #T2 #t2 #H +| #l #f1 #T2 #f2 #H >(lifts_inv_gref1 … H) -T2 // +| #p #I #W1 #W #U1 #U #f1 #_ #_ #IHW #IHU #T2 #f2 #H elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct - /4 width=3 by lifts_bind, after_true/ -| #I #W1 #W #U1 #U #t1 #_ #_ #IHW #IHU #T2 #t2 #H + /4 width=3 by lifts_bind, after_O2/ +| #I #W1 #W #U1 #U #f1 #_ #_ #IHW #IHU #T2 #f2 #H elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct /3 width=3 by lifts_flat/ ] qed-. (* Basic_2A1: includes: lift_conf_O1 lift_conf_be *) -theorem lifts_conf: ∀T,T1,t1. ⬆*[t1] T ≡ T1 → ∀T2,t. ⬆*[t] T ≡ T2 → - ∀t2. t2 ⊚ t1 ≡ t → ⬆*[t2] T1 ≡ T2. -#T #T1 #t1 #H elim H -T -T1 -t1 -[ #k #t1 #T2 #t #H >(lifts_inv_sort1 … H) -T2 // -| #i #i1 #t1 #Hi1 #T2 #t #H #t2 #Ht21 elim (lifts_inv_lref1 … H) -H +theorem lifts_conf: ∀T,T1,f1. ⬆*[f1] T ≡ T1 → ∀T2,f. ⬆*[f] T ≡ T2 → + ∀f2. f2 ⊚ f1 ≡ f → ⬆*[f2] T1 ≡ T2. +#T #T1 #f1 #H elim H -T -T1 -f1 +[ #s #f1 #T2 #f #H >(lifts_inv_sort1 … H) -T2 // +| #i #i1 #f1 #Hi1 #T2 #f #H #f2 #Ht21 elim (lifts_inv_lref1 … H) -H #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at2/ -| #p #t1 #T2 #t #H >(lifts_inv_gref1 … H) -T2 // -| #a #I #W #W1 #U #U1 #t1 #_ #_ #IHW #IHU #T2 #t #H +| #l #f1 #T2 #f #H >(lifts_inv_gref1 … H) -T2 // +| #p #I #W #W1 #U #U1 #f1 #_ #_ #IHW #IHU #T2 #f #H elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct - /4 width=3 by lifts_bind, after_true/ -| #I #W #W1 #U #U1 #t1 #_ #_ #IHW #IHU #T2 #t #H + /4 width=3 by lifts_bind, after_O2/ +| #I #W #W1 #U #U1 #f1 #_ #_ #IHW #IHU #T2 #f #H elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct /3 width=3 by lifts_flat/ ] qed-. + +(* Advanced proprerties *****************************************************) + +(* Basic_2A1: includes: lift_inj *) +lemma lifts_inj: ∀T1,U,f. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2. +#T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝 f ?) +/3 width=6 by lifts_div, lifts_fwd_isid/ +qed-. + +(* Basic_2A1: includes: lift_mono *) +lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2. +#T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝 f ?) +/3 width=6 by lifts_conf, lifts_fwd_isid/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma index c1a088ee5..f741b3e5a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma @@ -20,34 +20,34 @@ include "basic_2/relocation/lifts_vector.ma". (* Main properties **********************************************************) (* Basic_1: includes: lifts_inj *) -theorem liftsv_inj: ∀T1s,Us,t. ⬆*[t] T1s ≡ Us → - ∀T2s. ⬆*[t] T2s ≡ Us → T1s = T2s. -#T1s #Us #t #H elim H -T1s -Us -[ #T2s #H >(liftsv_inv_nil2 … H) -H // -| #T1s #Us #T1 #U #HT1U #_ #IHT1Us #X #H destruct - elim (liftsv_inv_cons2 … H) -H #T2 #T2s #HT2U #HT2Us #H destruct +theorem liftsv_inj: ∀T1c,Us,f. ⬆*[f] T1c ≡ Us → + ∀T2c. ⬆*[f] T2c ≡ Us → T1c = T2c. +#T1c #Us #f #H elim H -T1c -Us +[ #T2c #H >(liftsv_inv_nil2 … H) -H // +| #T1c #Us #T1 #U #HT1U #_ #IHT1Us #X #H destruct + elim (liftsv_inv_cons2 … H) -H #T2 #T2c #HT2U #HT2Us #H destruct >(lifts_inj … HT1U … HT2U) -U /3 width=1 by eq_f/ ] qed-. (* Basic_2A1: includes: liftv_mono *) -theorem liftsv_mono: ∀Ts,U1s,t. ⬆*[t] Ts ≡ U1s → - ∀U2s. ⬆*[t] Ts ≡ U2s → U1s = U2s. -#Ts #U1s #t #H elim H -Ts -U1s -[ #U2s #H >(liftsv_inv_nil1 … H) -H // -| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct - elim (liftsv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct +theorem liftsv_mono: ∀Ts,U1c,f. ⬆*[f] Ts ≡ U1c → + ∀U2c. ⬆*[f] Ts ≡ U2c → U1c = U2c. +#Ts #U1c #f #H elim H -Ts -U1c +[ #U2c #H >(liftsv_inv_nil1 … H) -H // +| #Ts #U1c #T #U1 #HTU1 #_ #IHTU1c #X #H destruct + elim (liftsv_inv_cons1 … H) -H #U2 #U2c #HTU2 #HTU2c #H destruct >(lifts_mono … HTU1 … HTU2) -T /3 width=1 by eq_f/ ] qed-. (* Basic_1: includes: lifts1_xhg (right to left) *) (* Basic_2A1: includes: liftsv_liftv_trans_le *) -theorem liftsv_trans: ∀T1s,Ts,t1. ⬆*[t1] T1s ≡ Ts → ∀T2s,t2. ⬆*[t2] Ts ≡ T2s → - ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1s ≡ T2s. -#T1s #Ts #t1 #H elim H -T1s -Ts -[ #T2s #t2 #H >(liftsv_inv_nil1 … H) -T2s /2 width=3 by liftsv_nil/ -| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #t2 #H elim (liftsv_inv_cons1 … H) -H - #T2 #T2s #HT2 #HT2s #H destruct /3 width=6 by lifts_trans, liftsv_cons/ +theorem liftsv_trans: ∀T1c,Ts,f1. ⬆*[f1] T1c ≡ Ts → ∀T2c,f2. ⬆*[f2] Ts ≡ T2c → + ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1c ≡ T2c. +#T1c #Ts #f1 #H elim H -T1c -Ts +[ #T2c #f2 #H >(liftsv_inv_nil1 … H) -T2c /2 width=3 by liftsv_nil/ +| #T1c #Ts #T1 #T #HT1 #_ #IHT1c #X #f2 #H elim (liftsv_inv_cons1 … H) -H + #T2 #T2c #HT2 #HT2c #H destruct /3 width=6 by lifts_trans, liftsv_cons/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma index ae73703f7..df090ce57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma @@ -20,13 +20,13 @@ include "basic_2/relocation/lifts.ma". (* Forward lemmas on simple terms *******************************************) (* Basic_2A1: includes: lift_simple_dx *) -lemma lifts_simple_dx: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#T1 #T2 #t #H elim H -T1 -T2 -t // -#a #I #V1 #V2 #T1 #T2 #t #_ #_ #_ #_ #H elim (simple_inv_bind … H) +lemma lifts_simple_dx: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +#T1 #T2 #f #H elim H -T1 -T2 -f // +#p #I #V1 #V2 #T1 #T2 #f #_ #_ #_ #_ #H elim (simple_inv_bind … H) qed-. (* Basic_2A1: includes: lift_simple_sn *) -lemma lifts_simple_sn: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -#T1 #T2 #t #H elim H -T1 -T2 -t // -#a #I #V1 #V2 #T1 #T2 #t #_ #_ #_ #_ #H elim (simple_inv_bind … H) +lemma lifts_simple_sn: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +#T1 #T2 #f #H elim H -T1 -T2 -f // +#p #I #V1 #V2 #T1 #T2 #f #_ #_ #_ #_ #H elim (simple_inv_bind … H) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma index 159e9d869..9c6128335 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma @@ -18,97 +18,105 @@ include "basic_2/relocation/lifts.ma". (* GENERIC RELOCATION FOR TERM VECTORS *************************************) (* Basic_2A1: includes: liftv_nil liftv_cons *) -inductive liftsv (t:trace) : relation (list term) ≝ -| liftsv_nil : liftsv t (◊) (◊) -| liftsv_cons: ∀T1s,T2s,T1,T2. - ⬆*[t] T1 ≡ T2 → liftsv t T1s T2s → - liftsv t (T1 @ T1s) (T2 @ T2s) +inductive liftsv (f): relation (list term) ≝ +| liftsv_nil : liftsv f (◊) (◊) +| liftsv_cons: ∀T1c,T2c,T1,T2. + ⬆*[f] T1 ≡ T2 → liftsv f T1c T2c → + liftsv f (T1 @ T1c) (T2 @ T2c) . interpretation "generic relocation (vector)" - 'RLiftStar t T1s T2s = (liftsv t T1s T2s). + 'RLiftStar f T1c T2c = (liftsv f T1c T2c). (* Basic inversion lemmas ***************************************************) -fact liftsv_inv_nil1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → X = ◊ → Y = ◊. -#X #Y #t * -X -Y // -#T1s #T2s #T1 #T2 #_ #_ #H destruct +fact liftsv_inv_nil1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → X = ◊ → Y = ◊. +#X #Y #f * -X -Y // +#T1c #T2c #T1 #T2 #_ #_ #H destruct qed-. (* Basic_2A1: includes: liftv_inv_nil1 *) -lemma liftsv_inv_nil1: ∀Y,t. ⬆*[t] ◊ ≡ Y → Y = ◊. +lemma liftsv_inv_nil1: ∀Y,f. ⬆*[f] ◊ ≡ Y → Y = ◊. /2 width=5 by liftsv_inv_nil1_aux/ qed-. -fact liftsv_inv_cons1_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → - ∀T1,T1s. X = T1 @ T1s → - ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s & - Y = T2 @ T2s. -#X #Y #t * -X -Y -[ #U1 #U1s #H destruct -| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/ +fact liftsv_inv_cons1_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → + ∀T1,T1c. X = T1 @ T1c → + ∃∃T2,T2c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c & + Y = T2 @ T2c. +#X #Y #f * -X -Y +[ #U1 #U1c #H destruct +| #T1c #T2c #T1 #T2 #HT12 #HT12c #U1 #U1c #H destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_2A1: includes: liftv_inv_cons1 *) -lemma liftsv_inv_cons1: ∀T1,T1s,Y,t. ⬆*[t] T1 @ T1s ≡ Y → - ∃∃T2,T2s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s & - Y = T2 @ T2s. +lemma liftsv_inv_cons1: ∀T1,T1c,Y,f. ⬆*[f] T1 @ T1c ≡ Y → + ∃∃T2,T2c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c & + Y = T2 @ T2c. /2 width=3 by liftsv_inv_cons1_aux/ qed-. -fact liftsv_inv_nil2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → Y = ◊ → X = ◊. -#X #Y #t * -X -Y // -#T1s #T2s #T1 #T2 #_ #_ #H destruct +fact liftsv_inv_nil2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → Y = ◊ → X = ◊. +#X #Y #f * -X -Y // +#T1c #T2c #T1 #T2 #_ #_ #H destruct qed-. -lemma liftsv_inv_nil2: ∀X,t. ⬆*[t] X ≡ ◊ → X = ◊. +lemma liftsv_inv_nil2: ∀X,f. ⬆*[f] X ≡ ◊ → X = ◊. /2 width=5 by liftsv_inv_nil2_aux/ qed-. -fact liftsv_inv_cons2_aux: ∀X,Y,t. ⬆*[t] X ≡ Y → - ∀T2,T2s. Y = T2 @ T2s → - ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s & - X = T1 @ T1s. -#X #Y #t * -X -Y -[ #U2 #U2s #H destruct -| #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/ +fact liftsv_inv_cons2_aux: ∀X,Y,f. ⬆*[f] X ≡ Y → + ∀T2,T2c. Y = T2 @ T2c → + ∃∃T1,T1c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c & + X = T1 @ T1c. +#X #Y #f * -X -Y +[ #U2 #U2c #H destruct +| #T1c #T2c #T1 #T2 #HT12 #HT12c #U2 #U2c #H destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma liftsv_inv_cons2: ∀X,T2,T2s,t. ⬆*[t] X ≡ T2 @ T2s → - ∃∃T1,T1s. ⬆*[t] T1 ≡ T2 & ⬆*[t] T1s ≡ T2s & - X = T1 @ T1s. +lemma liftsv_inv_cons2: ∀X,T2,T2c,f. ⬆*[f] X ≡ T2 @ T2c → + ∃∃T1,T1c. ⬆*[f] T1 ≡ T2 & ⬆*[f] T1c ≡ T2c & + X = T1 @ T1c. /2 width=3 by liftsv_inv_cons2_aux/ qed-. (* Basic_1: was: lifts1_flat (left to right) *) -lemma lifts_inv_applv1: ∀V1s,U1,T2,t. ⬆*[t] Ⓐ V1s.U1 ≡ T2 → - ∃∃V2s,U2. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 & - T2 = Ⓐ V2s.U2. -#V1s elim V1s -V1s +lemma lifts_inv_applv1: ∀V1c,U1,T2,f. ⬆*[f] Ⓐ V1c.U1 ≡ T2 → + ∃∃V2c,U2. ⬆*[f] V1c ≡ V2c & ⬆*[f] U1 ≡ U2 & + T2 = Ⓐ V2c.U2. +#V1c elim V1c -V1c [ /3 width=5 by ex3_2_intro, liftsv_nil/ -| #V1 #V1s #IHV1s #T1 #X #t #H elim (lifts_inv_flat1 … H) -H - #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY - #V2s #T2 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/ +| #V1 #V1c #IHV1c #T1 #X #f #H elim (lifts_inv_flat1 … H) -H + #V2 #Y #HV12 #HY #H destruct elim (IHV1c … HY) -IHV1c -HY + #V2c #T2 #HV12c #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/ ] qed-. -lemma lifts_inv_applv2: ∀V2s,U2,T1,t. ⬆*[t] T1 ≡ Ⓐ V2s.U2 → - ∃∃V1s,U1. ⬆*[t] V1s ≡ V2s & ⬆*[t] U1 ≡ U2 & - T1 = Ⓐ V1s.U1. -#V2s elim V2s -V2s +lemma lifts_inv_applv2: ∀V2c,U2,T1,f. ⬆*[f] T1 ≡ Ⓐ V2c.U2 → + ∃∃V1c,U1. ⬆*[f] V1c ≡ V2c & ⬆*[f] U1 ≡ U2 & + T1 = Ⓐ V1c.U1. +#V2c elim V2c -V2c [ /3 width=5 by ex3_2_intro, liftsv_nil/ -| #V2 #V2s #IHV2s #T2 #X #t #H elim (lifts_inv_flat2 … H) -H - #V1 #Y #HV12 #HY #H destruct elim (IHV2s … HY) -IHV2s -HY - #V1s #T1 #HV12s #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/ +| #V2 #V2c #IHV2c #T2 #X #f #H elim (lifts_inv_flat2 … H) -H + #V1 #Y #HV12 #HY #H destruct elim (IHV2c … HY) -IHV2c -HY + #V1c #T1 #HV12c #HT12 #H destruct /3 width=5 by ex3_2_intro, liftsv_cons/ ] qed-. (* Basic properties *********************************************************) +(* Basic_2A1: includes: liftv_total *) +lemma liftsv_total: ∀f. ∀T1c:list term. ∃T2c. ⬆*[f] T1c ≡ T2c. +#f #T1c elim T1c -T1c +[ /2 width=2 by liftsv_nil, ex_intro/ +| #T1 #T1c * #T2c #HT12c + elim (lifts_total T1 f) /3 width=2 by liftsv_cons, ex_intro/ +] +qed-. + (* Basic_1: was: lifts1_flat (right to left) *) -lemma lifts_applv: ∀V1s,V2s,t. ⬆*[t] V1s ≡ V2s → - ∀T1,T2. ⬆*[t] T1 ≡ T2 → - ⬆*[t] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. -#V1s #V2s #t #H elim H -V1s -V2s /3 width=1 by lifts_flat/ +lemma lifts_applv: ∀V1c,V2c,f. ⬆*[f] V1c ≡ V2c → + ∀T1,T2. ⬆*[f] T1 ≡ T2 → + ⬆*[f] Ⓐ V1c. T1 ≡ Ⓐ V2c. T2. +#V1c #V2c #f #H elim H -V1c -V2c /3 width=1 by lifts_flat/ qed. -(* Basic_2A1: removed theorems 1: liftv_total *) (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma index ace77ad27..3c65cd7b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma @@ -20,6 +20,6 @@ include "basic_2/relocation/lifts.ma". (* Forward lemmas on weight for terms ***************************************) (* Basic_2A1: includes: lift_fwd_tw *) -lemma lifts_fwd_tw: ∀T1,T2,t. ⬆*[t] T1 ≡ T2 → ♯{T1} = ♯{T2}. -#T1 #T2 #t #H elim H -T1 -T2 -t normalize // +lemma lifts_fwd_tw: ∀T1,T2,f. ⬆*[f] T1 ≡ T2 → ♯{T1} = ♯{T2}. +#T1 #T2 #f #H elim H -T1 -T2 -f normalize // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma index 4bb3883ce..38540eecd 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma @@ -31,11 +31,14 @@ coinductive eq_stream (A): relation (stream A) ≝ interpretation "extensional equivalence (nstream)" 'ExtEq A t1 t2 = (eq_stream A t1 t2). +definition eq_stream_repl (A) (R:relation …) ≝ + ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 t2. + definition eq_stream_repl_back (A) (R:predicate …) ≝ - ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 → R t2. + ∀t1. R t1 → ∀t2. t1 ≐⦋A⦌ t2 → R t2. definition eq_stream_repl_fwd (A) (R:predicate …) ≝ - ∀t1,t2. t2 ≐⦋A⦌ t1 → R t1 → R t2. + ∀t1. R t1 → ∀t2. t2 ≐⦋A⦌ t1 → R t2. (* Basic inversion lemmas ***************************************************) 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 90af6fd87..e23b7bb2d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma @@ -32,3 +32,9 @@ qed. lemma eq_stream_split (A) (t): (hd … t) @ (tl … t) ≐⦋A⦌ t. #A * // 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) -H +/2 width=1 by/ +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 79e028a99..b11f32e15 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -419,19 +419,26 @@ qed-. (* Main inversion lemmas on after *******************************************) -let corec after_mono: ∀f1,f2,x. f1 ⊚ f2 ≡ x → ∀y. f1 ⊚ f2 ≡ y → x ≐ y ≝ ?. -* #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 ≝ ?. -* #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/ +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=4 by after_mono/ qed-. +/2 width=8 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 8fd1da8a7..9cb77e391 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_at.ma @@ -40,6 +40,12 @@ interpretation "relational application (nstream)" (* Basic properties on apply ************************************************) +lemma apply_eq_repl (i): eq_stream_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵). +#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H +elim (eq_stream_inv_seq ????? H) -H normalize // +#Hn #Hf /4 width=1 by eq_f2, eq_f/ +qed. + lemma apply_S1: ∀f,n,i. (⫯n@f)@❴i❵ = ⫯((n@f)@❴i❵). #n #f * // qed. @@ -251,13 +257,13 @@ qed-. lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → i2 = f@❴i1❵. /2 width=6 by at_mono/ qed-. -lemma at_repl_back: ∀i1,i2. eq_stream_repl_back ? (λf. @⦃i1, f⦄ ≡ i2). -#i1 #i2 #f1 #f2 #Ht #H1 lapply (at_total i1 f2) -#H2 <(at_mono … Ht … H1 … H2) -f1 -i2 // +lemma at_eq_repl_back: ∀i1,i2. eq_stream_repl_back ? (λf. @⦃i1, f⦄ ≡ i2). +#i1 #i2 #f1 #H1 #f2 #Hf lapply (at_total i1 f2) +#H2 <(at_mono … Hf … H1 … H2) -f1 -i2 // qed-. -lemma at_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λf. @⦃i1, f⦄ ≡ i2). -#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_repl_back/ +lemma at_eq_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λf. @⦃i1, f⦄ ≡ i2). +#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_eq_repl_back/ qed-. (* Advanced properties on at ************************************************) @@ -287,5 +293,6 @@ qed-. (* Advanced properties on apply *********************************************) -fact apply_inj_aux: ∀f1,f2. f1 ≐ f2 → ∀i,i1,i2. i = f1@❴i1❵ → i = f2@❴i2❵ → i1 = i2. +fact apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. j1 = f1@❴i1❵ → j2 = f2@❴i2❵ → + j1 = j2 → f1 ≐ f2 → i1 = i2. /2 width=6 by at_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma index a24fd8a3b..b80af7485 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma @@ -36,6 +36,12 @@ qed. (* Basic properties on isid *************************************************) +lemma isid_eq_repl_back: eq_stream_repl_back … isid. +/2 width=3 by eq_stream_canc_sn/ qed-. + +lemma isid_eq_repl_fwd: eq_stream_repl_fwd … isid. +/3 width=3 by isid_eq_repl_back, eq_stream_repl_sym/ qed-. + lemma isid_id: 𝐈⦃𝐈𝐝⦄. // qed. @@ -59,6 +65,14 @@ lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥. #_ #H destruct qed-. +lemma isid_inv_gen: ∀f. 𝐈⦃f⦄ → ∃∃g. 𝐈⦃g⦄ & f = ↑g. +* #n #f #H elim (isid_inv_seq … H) -H +#Hf #H destruct /2 width=3 by ex2_intro/ +qed-. + +lemma isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≐ f2. +/2 width=3 by eq_stream_canc_dx/ qed-. + (* inversion lemmas on at ***************************************************) let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?. @@ -110,7 +124,7 @@ lemma after_isid_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f1 ≐ f → 𝐈⦃f2⦄. #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_repl_back, at_mono, at_id_le/ +/3 width=7 by at_eq_repl_back, at_mono, at_id_le/ qed. (* Inversion lemmas on after ************************************************) @@ -129,11 +143,11 @@ let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?. qed-. lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f. -/3 width=4 by isid_after_sn, after_mono/ +/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=4 by isid_after_dx, after_mono/ +/3 width=8 by isid_after_dx, after_mono/ qed-. (* lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄. 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 4e2f20bf6..dc462b3da 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_lift.ma @@ -29,6 +29,14 @@ interpretation "next (nstream)" 'Successor f = (next f). (* Basic properties *********************************************************) +lemma push_eq_repl: eq_stream_repl … (λf1,f2. ↑f1 ≐ ↑f2). +/2 width=1 by eq_seq/ qed. + +lemma next_eq_repl: eq_stream_repl … (λf1,f2. ⫯f1 ≐ ⫯f2). +* #n1 #f1 * #n2 #f2 #H elim (eq_stream_inv_seq ????? H) -H +/2 width=1 by eq_seq/ +qed. + lemma push_rew: ∀f. ↑f = 0@f. // qed. @@ -71,3 +79,35 @@ qed-. 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-. + +lemma push_inv_dx: ∀x,f. x ≐ ↑f → ∃∃g. x = ↑g & g ≐ f. +* #m #x #f #H elim (eq_stream_inv_seq ????? H) -H +/2 width=3 by ex2_intro/ +qed-. + +lemma push_inv_sn: ∀f,x. ↑f ≐ x → ∃∃g. x = ↑g & f ≐ g. +#f #x #H lapply (eq_stream_sym … H) -H +#H elim (push_inv_dx … H) -H +/3 width=3 by eq_stream_sym, ex2_intro/ +qed-. + +lemma push_inv_bi: ∀f,g. ↑f ≐ ↑g → f ≐ g. +#f #g #H elim (push_inv_dx … H) -H +#x #H #Hg lapply (injective_push … H) -H // +qed-. + +lemma next_inv_dx: ∀x,f. x ≐ ⫯f → ∃∃g. x = ⫯g & g ≐ f. +* #m #x * #n #f #H elim (eq_stream_inv_seq ????? H) -H +/3 width=5 by eq_seq, ex2_intro/ +qed-. + +lemma next_inv_sn: ∀f,x. ⫯f ≐ x → ∃∃g. x = ⫯g & f ≐ g. +#f #x #H lapply (eq_stream_sym … H) -H +#H elim (next_inv_dx … H) -H +/3 width=3 by eq_stream_sym, ex2_intro/ +qed-. + +lemma next_inv_bi: ∀f,g. ⫯f ≐ ⫯g → f ≐ g. +#f #g #H elim (next_inv_dx … H) -H +#x #H #Hg lapply (injective_next … H) -H // +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 39f75c7b6..bba1fcca1 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 @@ -10,23 +10,23 @@ table { } ] class "green" - [ { "multiple relocation" * } { + [ { "natural numbers with infinity" * } { [ { "" * } { - [ "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 ( ? ▭ ? ≡ ? )" * ] + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" + "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" + "ynat_plus ( ? + ? )" * + ] } ] } ] class "grass" - [ { "natural numbers with infinity" * } { + [ { "multiple relocation" * } { [ { "" * } { - [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" - "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" - "ynat_plus ( ? + ? )" * - ] + [ "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 ( ? ▭ ? ≡ ? )" * ] } ] } -- 2.39.2