From: Ferruccio Guidi Date: Mon, 15 Mar 2021 12:10:02 +0000 (+0100) Subject: propagating the arithmetics library, partial commit X-Git-Tag: make_still_working~152 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8fdf1af656038d0245eba64ff2531bbe94ce0e9e propagating the arithmetics library, partial commit + relocation updated and ported (de Bruijn indexes now start at 1) + recomm updated to generate substitution files + results on positive integers added to arith + some corrections --- diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml index c5d7f5857..e31efac1f 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml @@ -1,14 +1,11 @@ module ET = MrcTypes +module RL = RecommLib let read_substs substs ich = - let map subst = - let words = String.split_on_char ' ' subst in - List.filter ((<>) "") words - in while true do let line = input_line ich in - let subst = String.split_on_char ',' line in - substs := List.map map subst :: !substs + let subst = RL.split_on_char ',' line in + substs := List.map (RL.split_on_char ' ') subst :: !substs done let read_file file = diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml index ce971dd45..87caeb10b 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml @@ -13,9 +13,22 @@ let write = ref false let force = ref false +let subst = ref None + let chdir path = Sys.chdir path +let start_substs () = + subst := Some (open_out "subst.txt") + +let write_substs lint = function + | None -> () + | Some och -> EO.write_substs och lint + +let stop_substs = function + | None -> () + | Some och -> close_out och + let rec process path name = let file = Filename.concat path name in if Sys.is_directory file then begin @@ -26,6 +39,7 @@ let rec process path name = Printf.eprintf "processing: %S\n" file; let orig = EI.read_srcs file in let lint = EC.recomm_srcs orig in + write_substs lint !subst; if !force || (!write && lint <> orig) then EO.write_srcs file lint end else begin Printf.eprintf "skipping: %S\n" file @@ -43,6 +57,7 @@ let msg_o = " Log other comments (default: no)" let msg_r = " Replace the input files (default: no)" let msg_s = " Log section comments (default: no)" let msg_t = " Log title comments (default: no)" +let msg_u = " Write substitution file (default: no)" let msg_w = " Write the changed output files (default: no)" let main = @@ -59,5 +74,7 @@ let main = "-r", Arg.Set EO.replace, msg_r; "-s", Arg.Set EC.log_s, msg_s; "-t", Arg.Set EC.log_t, msg_t; + "-u", Arg.Unit start_substs, msg_u; "-w", Arg.Set write, msg_w; - ] (process "") "" + ] (process "") ""; + stop_substs !subst diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml index 655ff8095..53e68f84b 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml @@ -64,20 +64,20 @@ let log color s = let rec recomm srcs st = match srcs with - | [] -> + | [] -> st - | ET.Line _ as hd :: tl -> + | ET.Line _ as hd :: tl -> recomm tl @@ add hd @@ st - | ET.Text _ as hd :: tl -> + | ET.Text _ as hd :: tl -> recomm tl @@ add hd @@ st - | ET.Mark s as hd :: tl -> + | ET.Mark s as hd :: tl -> if !log_m then log red s; recomm tl @@ add hd @@ st - | ET.Key (s1, s2) as hd :: tl -> + | ET.Key (s1, s2) as hd :: tl -> if middle st then Printf.eprintf "middle: %S\n" s1; if !log_k then log prune (s1^s2); recomm tl @@ add hd @@ st - | ET.Title ss :: tl -> + | ET.Title ss :: tl -> if middle st then Printf.eprintf "middle: TITLE\n"; let r, ss1, ss2 = !c_line k_final ET.OO [] ss in let ss2 = @@ -87,7 +87,7 @@ let rec recomm srcs st = let s = String.concat " " ss in if !log_t then log blue s; recomm tl @@ add (ET.Title ss) @@ st - | ET.Slice ss :: tl -> + | ET.Slice ss :: tl -> if middle st then Printf.eprintf "middle: Section\n"; let r, ss1, ss2 = !s_line k_final ET.OO [] ss in let ss2 = @@ -97,7 +97,7 @@ let rec recomm srcs st = let s = String.capitalize_ascii (String.concat " " ss) in if !log_s then log sky s; recomm tl @@ add (ET.Slice ss) @@ st - | ET.Other (_, s, _) as hd :: tl -> + | ET.Other (_, _, s, _) as hd :: tl -> if !log_o && not (Array.mem s mute_o) then log black s; recomm tl @@ add hd @@ st diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommLib.ml new file mode 100644 index 000000000..7624d9a84 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLib.ml @@ -0,0 +1,2 @@ +let split_on_char c s = + List.filter ((<>) "") (String.split_on_char c s) diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommLib.mli new file mode 100644 index 000000000..ca2c912c4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLib.mli @@ -0,0 +1 @@ +val split_on_char: char -> string -> string list diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml index 187a2984b..c48ba9304 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml @@ -1,3 +1,4 @@ +module EL = RecommLib module ET = RecommTypes let width = ref 78 @@ -23,24 +24,24 @@ let complete s n = end let out_src och = function - | ET.Line s -> + | ET.Line s -> Printf.fprintf och "%s" s - | ET.Text s -> + | ET.Text s -> Printf.fprintf och "%s" s - | ET.Mark s -> + | ET.Mark s -> Printf.fprintf och "(* *%s*)" s - | ET.Key (s1, s2) -> + | ET.Key (s1, s2) -> let s3 = if s1 = "NOTE" then complete (s1^s2) 0 else "" in Printf.fprintf och "(* %s%s%s*)" s1 s2 s3 - | ET.Title ss -> + | ET.Title ss -> let s = String.concat " " ss in Printf.fprintf och "(* %s %s*)" s (complete s 1) - | ET.Slice ss -> + | ET.Slice ss -> let s = String.capitalize_ascii (String.concat " " ss) in Printf.fprintf och "(* %s %s*)" s (complete s 1) - | ET.Other (s1, s2, s3) -> + | ET.Other (_, s1, s2, s3) -> Printf.fprintf och "%s%s%s" s1 s2 s3 let write_srcs file srcs = @@ -55,3 +56,33 @@ let write_srcs file srcs = let och = open_out target in List.iter (out_src och) srcs; close_out och + +let write_subst och n s = + Printf.fprintf och "%s %s\n" s n + +let rec write_fst och = function + | [] -> () + | ET.Other (2, _, s, _) :: ET.Line _ :: ET.Text t :: tl -> + write_snd och tl s (EL.split_on_char ' ' t) + | ET.Other (2, _, s, _) :: tl -> + Printf.eprintf "skipping fst: %S\n" s; + write_fst och tl + | _ :: tl -> write_fst och tl + +and write_snd och tl s = function + | "definition" :: n :: _ + | "fact" :: n :: _ + | "lemma" :: n :: _ + | "inductive" :: n :: _ + | "theorem" :: n :: _ -> + let ss = EL.split_on_char ' ' s in + List.iter (write_subst och n) (List.tl ss); + write_fst och tl + | t :: _ -> + Printf.eprintf "skipping snd: %S %S\n" s t; + write_fst och tl + | [] -> + Printf.eprintf "skipping snd: %S\n" s; + write_fst och tl + +let write_substs = write_fst diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli index 088b7fd9d..05a0fe324 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli @@ -3,3 +3,5 @@ val width: int ref val replace: bool ref val write_srcs: string -> RecommTypes.srcs -> unit + +val write_substs: out_channel -> RecommTypes.srcs -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly index 79512c7c4..d8c655bf7 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommParser.mly @@ -79,16 +79,16 @@ sws: | SP sw sws { $2 :: $3 } src_l: - | NL { ET.Line $1 } - | OP sp PP inns CP { ET.Mark $4 } - | OP sp KW inns CP { ET.Key ($3, $4) } - | OP sp CW cws CP { ET.Title ($3 :: $4) } - | OP sp HW sws CP { ET.Slice (lc $3 :: $4) } - | OP sp CP { ET.Other ($1, $2, $3) } - | OP sp inns_r CP { ET.Other ($1, $2 ^ $3, $4) } - | OP SR inns CP { ET.Other ($1, $2 ^ $3, $4) } - | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) } - | OP SP SR inns CP { ET.Mark $4 } + | NL { ET.Line $1 } + | OP sp PP inns CP { ET.Mark $4 } + | OP sp KW inns CP { ET.Key ($3, $4) } + | OP sp CW cws CP { ET.Title ($3 :: $4) } + | OP sp HW sws CP { ET.Slice (lc $3 :: $4) } + | OP sp CP { ET.Other (0, $1, $2, $3) } + | OP sp inns_r CP { ET.Other (0, $1, $2 ^ $3, $4) } + | OP SR inns CP { ET.Other (1, $1, $2 ^ $3, $4) } + | OP SR SR inns CP { ET.Other (2, $1, $2 ^ $3 ^ $4, $5) } + | OP SP SR inns CP { ET.Mark $4 } src: | outs { ET.Text $1 } diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml index 7225e916e..7098edb5c 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommTypes.ml @@ -18,7 +18,7 @@ type src = (* section *) | Slice of words (* other comment *) - | Other of text * text * text + | Other of int * text * text * text type srcs = src list diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt b/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt index 331e5a939..9de8f4ed3 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_etc.txt @@ -41,21 +41,6 @@ qed-. (* Decidability of predicates ***********************************************) -lemma dec_lt (R:predicate nat): - (∀n. Decidable … (R n)) → - ∀n. Decidable … (∃∃m. m < n & R m). -#R #HR #n elim n -n [| #n * ] -[ @or_intror * /2 width=2 by lt_zero_false/ -| * /4 width=3 by lt_S, or_introl, ex2_intro/ -| #H0 elim (HR n) -HR - [ /3 width=3 by or_introl, ex2_intro/ - | #Hn @or_intror * #m #Hmn #Hm - elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ] - /4 width=3 by lt_S_S_to_lt, ex2_intro/ - ] -] -qed-. - lemma dec_min (R:predicate nat): (∀n. Decidable … (R n)) → ∀n. R n → ∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥). diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma index c2d89a6f7..5d99e4c55 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma @@ -18,7 +18,6 @@ include "ground/arith/nat_succ.ma". (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************) (*** le *) -(*** le_ind *) inductive nle (m:nat): predicate nat ≝ | nle_refl : nle m m | nle_succ_dx: ∀n. nle m n → nle m (↑n) @@ -88,7 +87,7 @@ lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥. lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥. #m @(nat_ind_succ … m) -m [| #m #IH ] #H -[ /3 width=2 by nle_inv_zero_dx, eq_inv_zero_nsucc/ +[ /2 width=2 by nle_inv_succ_zero/ | /3 width=1 by nle_inv_succ_bi/ ] qed-. @@ -110,7 +109,7 @@ lemma nle_ind_alt (Q: relation2 nat nat): (∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) → ∀m,n. m ≤ n → Q m n. #Q #IH1 #IH2 #m #n @(nat_ind_2_succ … m n) -m -n // -[ #m #H elim (nle_inv_succ_zero … H) +[ #m #_ #H elim (nle_inv_succ_zero … H) | /4 width=1 by nle_inv_succ_bi/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma index d54738f25..7a53e23f7 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma @@ -39,7 +39,11 @@ lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m. /2 width=1 by nle_plus_bi_sn/ qed. (*** le_plus_a *) -lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m. +lemma nle_plus_dx_sn (o) (m) (n): n ≤ m → n ≤ o + m. +/2 width=3 by nle_trans/ qed. + +(*** le_plus_b *) +lemma nle_plus_dx_dx (o) (m) (n): n ≤ m → n ≤ m + o. /2 width=3 by nle_trans/ qed. (* Main constructions with nplus ********************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma index 0abb785f7..4cfdfbacd 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma @@ -149,3 +149,22 @@ lemma nlt_ind_alt (Q: relation2 nat nat): | /4 width=1 by nlt_inv_succ_bi/ ] qed-. + +(* Advanced constructions (decidability) ************************************) + +(*** dec_lt *) +lemma dec_nlt (R:predicate nat): + (∀n. Decidable … (R n)) → + ∀n. Decidable … (∃∃m. m < n & R m). +#R #HR #n @(nat_ind_succ … n) -n [| #n * ] +[ @or_intror * /2 width=2 by nlt_inv_zero_dx/ +| * /4 width=3 by nlt_succ_dx_trans, ex2_intro, or_introl/ +| #H0 elim (HR n) -HR + [ /3 width=3 by or_introl, ex2_intro/ + | #Hn @or_intror * #m #Hmn #Hm + elim (nle_split_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ] + [ /4 width=3 by nlt_inv_succ_bi, ex2_intro/ + | lapply (eq_inv_nsucc_bi … H) -H /2 width=1 by/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma index 89af3af2b..0f0a21c82 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma @@ -31,6 +31,12 @@ lemma nlt_plus_bi_sn (m) (n1) (n2): n1 < n2 → m + n1 < m + n2. @nlt_i >nplus_succ_dx /2 width=1 by nle_plus_bi_sn/ qed. +lemma nlt_plus_dx_dx (o) (m) (n): m < n → m < n + o. +/2 width=1 by nle_plus_dx_dx/ qed. + +lemma nlt_plus_dx_sn (o) (m) (n) : m < n → m < o + n. +/2 width=1 by nle_plus_dx_sn/ qed. + lemma nlt_succ_plus_dx_refl_sn (m) (n): m < ↑(m + n). /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma index ecda40f03..e910fdaa0 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma @@ -25,7 +25,7 @@ lemma nminus_plus_sn_refl_sn (m) (n): m = m + n - n. #n #IH (plt_des_gen (𝟏) q) +[ /2 width=1 by plt_succ_bi/ +| /3 width=3 by ple_plt_trans, plt_ple_trans/ +] +qed-. + +lemma plt_inv_pred_bi (p) (q): + ↓p < ↓q → p < q. +/3 width=3 by plt_inv_pred_dx, ple_plt_trans/ +qed-. + +(* Constructions with ppred *************************************************) + +lemma plt_unit_sn (q): q = ↑↓q → 𝟏 < q. +// qed. + +lemma plt_pred_bi (p) (q): 𝟏 < p → p < q → ↓p < ↓q. +#p #q #Hp #Hpq +@ple_inv_succ_bi +<(plt_des_gen … Hp) -Hp +<(plt_des_gen … Hpq) // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma index 8fd6b5c47..1ff7afbb4 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma @@ -49,3 +49,25 @@ lemma pplus_assoc: associative … pplus. #p #q #r elim r -r // #r #IH next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=5 by after_next/ -] -qed-. - -theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1. -/2 width=1 by after_total_aux/ qed. - -(* Specific inversion lemmas on after ***************************************) - -lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ⫯f1 = g2 → - f2 ⊚ f1 ≘ f ∧ n2 = n. -#f2 #g2 #f #n2 elim n2 -n2 -[ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ] - #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/ -| #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] - #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1 - #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg - #H destruct /2 width=1 by conj/ -] -qed-. - -lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ↑f1 = g2 → - ∃∃m. f2 ⊚ f1 ≘ m⨮f & ↑(n2+m) = n. -#f2 #g2 #f #n2 elim n2 -n2 -[ #n #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ] - #g #Hf #H elim (next_inv_seq_dx … H) -H - #x #Hx #Hg destruct /2 width=3 by ex2_intro/ -| #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] - #g #Hg #H elim (next_inv_seq_dx … H) -H - #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ] - #m #Hf #Hm destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma after_inv_const: ∀f2,f1,f,n1,n. n⨮f2 ⊚ n1⨮f1 ≘ n⨮f → f2 ⊚ f1 ≘ f ∧ 0 = n1. -#f2 #f1 #f #n1 #n elim n -n -[ #H elim (after_inv_pxp … H) -H [ |*: // ] - #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ -| #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/ -] -qed-. - -lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f. -/2 width=4 by after_mono/ qed-. - -(* Specific forward lemmas on after *****************************************) - -lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f → f2@❨n1❩ = n. -#f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ] -/3 width=2 by at_inv_O1, sym_eq/ -qed-. - -lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f → - (⫰*[n1]f2) ⊚ f1 ≘ f. -#f #f1 #n1 elim n1 -n1 -[ #f2 #n2 #n #H elim (after_inv_xpx … H) -H // -| #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ] - #m #Hm #H destruct /2 width=3 by/ -] -qed-. - -lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f → - (n2⨮f2)@❨n1❩ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f. -/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. - -(* Properties on apply ******************************************************) - -lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩. -/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_basic.ma deleted file mode 100644 index 703bee03d..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_basic.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/relocation/rtmap_basic.ma". -include "ground/relocation/nstream_after.ma". - -(* RELOCATION N-STREAM ******************************************************) - -(* Specific properties on basic relocation **********************************) - -lemma apply_basic_lt: ∀m,n,i. i < m → 𝐁❨m,n❩@❨i❩ = i. -/3 width=1 by at_inv_total, at_basic_lt/ qed-. - -lemma apply_basic_ge: ∀m,n,i. m ≤ i → 𝐁❨m,n❩@❨i❩ = n+i. -/3 width=1 by at_inv_total, at_basic_ge/ qed-. - -(* Specific main properties on basic relocation *****************************) - -theorem basic_swap: ∀d1,d2. d2 ≤ d1 → - ∀h1,h2. 𝐁❨d2,h2❩∘𝐁❨d1,h1❩ ≡ 𝐁❨h2+d1,h1❩∘𝐁❨d2,h2❩. -#d1 #d2 #Hd21 #h1 #h2 -@nstream_inv_eq -@nstream_eq_inv_ext #i -(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2) >apply_basic_lt - /2 width=1 by le_plus_a/ -| elim (lt_or_ge i d1) -Hd21 #Hd1 - [ >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2) >apply_basic_lt - /2 width=1 by monotonic_lt_plus_r/ - | >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2) - >apply_basic_ge [2: /2 width=1 by le_plus_a/ ] - >apply_basic_ge /2 width=1 by monotonic_le_plus_r/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_coafter.ma deleted file mode 100644 index 368647aee..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_coafter.ma +++ /dev/null @@ -1,103 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/notation/functions/cocompose_2.ma". -include "ground/relocation/rtmap_coafter.ma". - -(* RELOCATION N-STREAM ******************************************************) - -rec definition fun0 (n1:nat) on n1: rtmap → nat. -* * [ | #n2 #f2 @0 ] -#f2 cases n1 -n1 [ @0 ] -#n1 @(↑(fun0 n1 f2)) -defined. - -rec definition fun2 (n1:nat) on n1: rtmap → rtmap. -* * [ | #n2 #f2 @(n2⨮f2) ] -#f2 cases n1 -n1 [ @f2 ] -#n1 @(fun2 n1 f2) -defined. - -rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap. -* * [ | #n2 #f2 @(n1⨮f1) ] -#f2 cases n1 -n1 [ @f1 ] -#n1 @(fun1 n1 f1 f2) -defined. - -corec definition cocompose: rtmap → rtmap → rtmap. -#f2 * #n1 #f1 @(seq … (fun0 n1 f2)) @(cocompose (fun2 n1 f2) (fun1 n1 f1 f2)) -defined. - -interpretation "functional co-composition (nstream)" - 'CoCompose f1 f2 = (cocompose f1 f2). - -(* Basic properties on funs *************************************************) - -(* Note: we need theese since matita blocks recursive δ when ι is blocked *) -lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (↑f2). -* #n2 #f2 * // -qed. - -lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (↑f2). -* #n2 #f2 * // -qed. - -lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1⨮f1. -* #n2 #f2 #f1 * // -qed. - -(* Basic properies on cocompose *********************************************) - -lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)⨮(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1⨮f1). -#f2 #f1 #n1 <(stream_rew … (f2~∘(n1⨮f1))) normalize // -qed. - -(* Basic inversion lemmas on compose ****************************************) - -lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f → - 0 = x ∧ f2 ~∘ f1 = f. -#f2 #f1 #f #x -next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/ -] -qed-. - -theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1. -/2 width=1 by coafter_total_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_eq.ma deleted file mode 100644 index 9678dcc5b..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_eq.ma +++ /dev/null @@ -1,55 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.tcs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/relocation/rtmap_eq.ma". - -(* RELOCATION N-STREAM ******************************************************) - -(* Specific properties ******************************************************) - -fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1⨮f1 ≡ n2⨮f2 → n1 = n2 ∧ f1 ≡ f2. -#f1 #f2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2 -[ #n2 #H elim (eq_inv_px … H) -H [2,3: // ] - #g1 #H1 #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ -| #n1 #H elim (eq_inv_np … H) -H // -| #n1 #n2 #IH #H lapply (eq_inv_nn … H ????) -H [1,2,3,4: // ] - #H elim (IH H) -IH -H /2 width=1 by conj/ -] -qed-. - -lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,n1,n2. n1⨮f1 = g1 → n2⨮f2 = g2 → - n1 = n2 ∧ f1 ≡ f2. -/2 width=1 by eq_inv_seq_aux/ qed-. - -corec lemma nstream_eq: ∀f1,f2. f1 ≡ f2 → f1 ≗ f2. -* #n1 #f1 * #n2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf * -#g1 #g2 #Hg #H1 #H2 -[ cases (push_inv_seq_dx … H1) -H1 * -n1 #H1 - cases (push_inv_seq_dx … H2) -H2 * -n2 #H2 - @eq_seq /2 width=1 by/ -| cases (next_inv_seq_dx … H1) -H1 #m1 #H1 * -n1 - cases (next_inv_seq_dx … H2) -H2 #m2 #H2 * -n2 - cases (eq_inv_seq … Hg … H1 H2) -g1 -g2 #Hm #Hf - @eq_seq /2 width=1 by/ -] -qed-. - -corec lemma nstream_inv_eq: ∀f1,f2. f1 ≗ f2 → f1 ≡ f2. -* #n1 #f1 * #n2 #f2 #H cases (eq_stream_inv_seq ??? H) -H [2,3,4,5,6,7: // ] -#Hf * -n2 cases n1 -n1 /3 width=5 by eq_push/ -#n @eq_next /3 width=5 by eq_seq/ -qed. - -lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n⨮f1 ≡ n⨮f2. -/4 width=1 by nstream_inv_eq, nstream_eq, eq_seq/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_id.ma deleted file mode 100644 index f3a1cce51..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_id.ma +++ /dev/null @@ -1,33 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/notation/functions/identity_0.ma". -include "ground/relocation/rtmap_eq.ma". - -(* RELOCATION N-STREAM ******************************************************) - -corec definition id: rtmap ≝ ⫯id. - -interpretation "identity (nstream)" - 'Identity = (id). - -(* Basic properties *********************************************************) - -lemma id_rew: ⫯𝐈𝐝 = 𝐈𝐝. -<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize // -qed. - -lemma id_eq_rew: ⫯𝐈𝐝 ≡ 𝐈𝐝. -cases id_rew in ⊢ (??%); // -qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_isid.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_isid.ma deleted file mode 100644 index 48ab9aaa2..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_isid.ma +++ /dev/null @@ -1,25 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/notation/functions/identity_0.ma". -include "ground/relocation/rtmap_isid.ma". - -(* RELOCATION N-STREAM ******************************************************) - -(* Specific inversion lemmas ************************************************) - -lemma isid_inv_seq: ∀f,n. 𝐈❪n⨮f❫ → 𝐈❪f❫ ∧ 0 = n. -#f #n #H elim (isid_inv_gen … H) -H -#g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_istot.ma deleted file mode 100644 index e1eaf0f27..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_istot.ma +++ /dev/null @@ -1,120 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.tcs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/notation/functions/apply_2.ma". -include "ground/relocation/nstream_eq.ma". -include "ground/relocation/rtmap_istot.ma". - -(* RELOCATION N-STREAM ******************************************************) - -rec definition apply (i: nat) on i: rtmap → nat ≝ ?. -* #n #f cases i -i -[ @n -| #i lapply (apply i f) -apply -i -f - #i @(↑(n+i)) -] -defined. - -interpretation "functional application (nstream)" - 'Apply f i = (apply i f). - -(* Specific properties on at ************************************************) - -lemma at_O1: ∀i2,f. @❪0, i2⨮f❫ ≘ i2. -#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/ -qed. - -lemma at_S1: ∀n,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, n⨮f❫ ≘ ↑(n+i2). -#n elim n -n /3 width=7 by at_push, at_next/ -qed. - -lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩. -#i1 elim i1 -i1 -[ * // | #i #IH * /3 width=1 by at_S1/ ] -qed. - -lemma at_istot: ∀f. 𝐓❪f❫. -/2 width=2 by ex_intro/ qed. - -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 // -#m apply_O1 >apply_O1 #H destruct - lapply (Hf (↑i)) >apply_S1 >apply_S1 #H - /3 width=2 by injective_plus_r, injective_S/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream_sor.ma deleted file mode 100644 index 2e7758110..000000000 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream_sor.ma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground/relocation/rtmap_sor.ma". - -(* RELOCATION N-STREAM ******************************************************) - -axiom union: rtmap → rtmap → rtmap. - -interpretation "union (nstream)" - 'union f1 f2 = (union f1 f2). - -(* Specific properties on sor ***********************************************) - -axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≘ f1 ∪ f2. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream.ma new file mode 100644 index 000000000..7092798fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/notation/functions/upspoon_1.ma". +include "ground/lib/stream.ma". +include "ground/arith/pnat.ma". + +(* RELOCATION P-STREAM ******************************************************) + +definition rtmap: Type[0] ≝ stream pnat. + +definition push: rtmap → rtmap ≝ λf. 𝟏⨮f. + +interpretation "push (pstream)" 'UpSpoon f = (push f). + +definition next: rtmap → rtmap. +* #p #f @(↑p⨮f) +defined. + +interpretation "next (pstream)" 'UpArrow f = (next f). + +(* Basic properties *********************************************************) + +lemma push_rew: ∀f. 𝟏⨮f = ⫯f. +// qed. + +lemma next_rew: ∀f,p. (↑p)⨮f = ↑(p⨮f). +// qed. + +(* Basic inversion lemmas ***************************************************) + +lemma injective_push: injective ? ? push. +#f1 #f2 nsucc_inj nsucc_inj next_rew #H cases (compose_inv_S1 … H) -H * -p >next_rew + /3 width=5 by after_next/ +] +qed-. + +theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1. +/2 width=1 by after_total_aux/ qed. + +(* Specific inversion lemmas on after ***************************************) + +lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 → + f2 ⊚ f1 ≘ f ∧ p2 = p. +#f2 #g2 #f #p2 elim p2 -p2 +[ #p #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [|*: // ] + #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/ +| #p2 #IH #p #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [|*: // ] + #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1 + #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg + #H destruct /2 width=1 by conj/ +] +qed-. + +lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 → + ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p. +#f2 #g2 #f #p2 elim p2 -p2 +[ #p #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [|*: // ] + #g #Hf #H elim (next_inv_seq_dx … H) -H + #x #Hx #Hg destruct /2 width=3 by ex2_intro/ +| #p2 #IH #p #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [|*: // ] + #g #Hg #H elim (next_inv_seq_dx … H) -H + #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ] + #m #Hf #Hm destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma after_inv_const: ∀f2,f1,f,p1,p. + p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1. +#f2 #f1 #f #p1 #p elim p -p +[ #H elim (after_inv_pxp … H) -H [|*: // ] + #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ +| #p #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/ +] +qed-. + +lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f. +/2 width=4 by after_mono/ qed-. + +(* Specific forward lemmas on after *****************************************) + +lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p. +#f2 #f1 #f #p1 #p #H lapply (after_fwd_at ? p1 (𝟏) … H) -H [4:|*: // ] +/3 width=2 by at_inv_O1, sym_eq/ +qed-. + +lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → + (⫰*[↓p1]f2) ⊚ f1 ≘ f. +#f #f1 #p1 elim p1 -p1 +[ #f2 #p2 #p #H elim (after_inv_xpx … H) -H // +| #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ] + #x #Hx #H destruct /2 width=3 by/ +] +qed-. + +lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → + (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f. +/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. + +(* Properties on apply ******************************************************) + +lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩. +/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_basic.ma new file mode 100644 index 000000000..072b509f4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_basic.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/arith/nat_lt_plus.ma". +include "ground/relocation/rtmap_basic_at.ma". +include "ground/relocation/pstream_after.ma". + +(* RELOCATION N-STREAM ******************************************************) + +(* Specific properties on basic relocation **********************************) + +lemma apply_basic_lt: ∀m,n,i. ninj i ≤ m → 𝐁❨m,n❩@❨i❩ = i. +/3 width=1 by at_inv_total, at_basic_lt/ qed-. + +lemma apply_basic_ge: ∀m,n,i. m < ninj i → 𝐁❨m,n❩@❨i❩ = i+n. +/3 width=1 by at_inv_total, at_basic_ge/ qed-. + +(* Specific main properties on basic relocation *****************************) + +theorem basic_swap: ∀d1,d2. d2 ≤ d1 → + ∀h1,h2. 𝐁❨d2,h2❩∘𝐁❨d1,h1❩ ≡ 𝐁❨d1+h2,h1❩∘𝐁❨d2,h2❩. +#d1 #d2 #Hd21 #h1 #h2 +@nstream_inv_eq +@nstream_eq_inv_ext #i +(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2) >apply_basic_ge + [ >apply_basic_ge // >nrplus_inj_sn /2 width=1 by nlt_plus_bi_sn/ + | >nrplus_inj_sn /2 width=2 by nlt_plus_dx_dx/ + ] + | >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2) + >apply_basic_lt // >nrplus_inj_sn /2 width=1 by nle_plus_bi_dx/ + ] +| lapply (nle_trans … Hd2 … Hd21) -Hd21 #Hd1 + >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2) + >apply_basic_lt /2 width=1 by nle_plus_dx_dx/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_coafter.ma new file mode 100644 index 000000000..4dd17dd58 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_coafter.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/notation/functions/cocompose_2.ma". +include "ground/relocation/rtmap_coafter.ma". + +(* RELOCATION N-STREAM ******************************************************) + +rec definition fun0 (p1:pnat) on p1: rtmap → pnat. +* * [ | #p2 #f2 @(𝟏) ] +#f2 cases p1 -p1 [ @(𝟏) ] +#p1 @(↑(fun0 p1 f2)) +defined. + +rec definition fun2 (p1:pnat) on p1: rtmap → rtmap. +* * [ | #p2 #f2 @(p2⨮f2) ] +#f2 cases p1 -p1 [ @f2 ] +#p1 @(fun2 p1 f2) +defined. + +rec definition fun1 (p1:pnat) (f1:rtmap) on p1: rtmap → rtmap. +* * [ | #p2 #f2 @(p1⨮f1) ] +#f2 cases p1 -p1 [ @f1 ] +#p1 @(fun1 p1 f1 f2) +defined. + +corec definition cocompose: rtmap → rtmap → rtmap. +#f2 * #p1 #f1 +@(stream_cons … (fun0 p1 f2)) @(cocompose (fun2 p1 f2) (fun1 p1 f1 f2)) +defined. + +interpretation "functional co-composition (nstream)" + 'CoCompose f1 f2 = (cocompose f1 f2). + +(* Basic properties on funs *************************************************) + +(* Note: we need theese since matita blocks recursive δ when ι is blocked *) +lemma fun0_xn: ∀f2,p1. 𝟏 = fun0 p1 (↑f2). +* #p2 #f2 * // +qed. + +lemma fun2_xn: ∀f2,p1. f2 = fun2 p1 (↑f2). +* #p2 #f2 * // +qed. + +lemma fun1_xxn: ∀f2,f1,p1. fun1 p1 f1 (↑f2) = p1⨮f1. +* #p2 #f2 #f1 * // +qed. + +(* Basic properies on cocompose *********************************************) + +lemma cocompose_rew: ∀f2,f1,p1. (fun0 p1 f2)⨮(fun2 p1 f2)~∘(fun1 p1 f1 f2) = f2 ~∘ (p1⨮f1). +#f2 #f1 #p1 <(stream_rew … (f2~∘(p1⨮f1))) normalize // +qed. + +(* Basic inversion lemmas on compose ****************************************) + +lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f → + ∧∧ 𝟏 = x & f2 ~∘ f1 = f. +#f2 #f1 #f #x +next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/ +] +qed-. + +theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1. +/2 width=1 by coafter_total_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_eq.ma new file mode 100644 index 000000000..12663ae77 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_eq.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/lib/stream_eq.ma". +include "ground/relocation/rtmap_eq.ma". + +(* RELOCATION N-STREAM ******************************************************) + +(* Specific properties ******************************************************) + +fact eq_inv_seq_aux: ∀f1,f2,p1,p2. p1⨮f1 ≡ p2⨮f2 → p1 = p2 ∧ f1 ≡ f2. +#f1 #f2 #p1 #p2 @(pnat_ind_2 … p1 p2) -p1 -p2 +[ #p2 #H elim (eq_inv_px … H) -H [2,3: // ] + #g1 #H1 #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ +| #p1 #_ #H elim (eq_inv_np … H) -H // +| #p1 #p2 #IH #H lapply (eq_inv_nn … H ????) -H [5:|*: // ] + #H elim (IH H) -IH -H /2 width=1 by conj/ +] +qed-. + +lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,p1,p2. p1⨮f1 = g1 → p2⨮f2 = g2 → + p1 = p2 ∧ f1 ≡ f2. +/2 width=1 by eq_inv_seq_aux/ qed-. + +corec lemma nstream_eq: ∀f1,f2. f1 ≡ f2 → f1 ≗ f2. +* #p1 #f1 * #p2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf * +#g1 #g2 #Hg #H1 #H2 +[ cases (push_inv_seq_dx … H1) -H1 * -p1 #H1 + cases (push_inv_seq_dx … H2) -H2 * -p2 #H2 + @stream_eq_cons /2 width=1 by/ +| cases (next_inv_seq_dx … H1) -H1 #m1 #H1 * -p1 + cases (next_inv_seq_dx … H2) -H2 #m2 #H2 * -p2 + cases (eq_inv_seq … Hg … H1 H2) -g1 -g2 #Hm #Hf + @stream_eq_cons /2 width=1 by/ +] +qed-. + +corec lemma nstream_inv_eq: ∀f1,f2. f1 ≗ f2 → f1 ≡ f2. +* #p1 #f1 * #p2 #f2 #H cases (stream_eq_inv_cons ??? H) -H [|*: // ] +#Hf * -p2 cases p1 -p1 /3 width=5 by eq_push/ +#n @eq_next /3 width=5 by stream_eq_cons/ +qed. + +lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n⨮f1 ≡ n⨮f2. +/4 width=1 by nstream_inv_eq, nstream_eq, stream_eq_cons/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_id.ma new file mode 100644 index 000000000..f3a1cce51 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_id.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/notation/functions/identity_0.ma". +include "ground/relocation/rtmap_eq.ma". + +(* RELOCATION N-STREAM ******************************************************) + +corec definition id: rtmap ≝ ⫯id. + +interpretation "identity (nstream)" + 'Identity = (id). + +(* Basic properties *********************************************************) + +lemma id_rew: ⫯𝐈𝐝 = 𝐈𝐝. +<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize // +qed. + +lemma id_eq_rew: ⫯𝐈𝐝 ≡ 𝐈𝐝. +cases id_rew in ⊢ (??%); // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_isid.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_isid.ma new file mode 100644 index 000000000..fa647fd14 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_isid.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/relocation/rtmap_isid.ma". + +(* RELOCATION N-STREAM ******************************************************) + +(* Specific inversion lemmas ************************************************) + +lemma isid_inv_seq: ∀f,p. 𝐈❪p⨮f❫ → 𝐈❪f❫ ∧ 𝟏 = p. +#f #p #H elim (isid_inv_gen … H) -H +#g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_istot.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_istot.ma new file mode 100644 index 000000000..f8b66a364 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_istot.ma @@ -0,0 +1,122 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/notation/functions/apply_2.ma". +include "ground/arith/pnat_le_plus.ma". +include "ground/relocation/pstream_eq.ma". +include "ground/relocation/rtmap_istot.ma". + +(* RELOCATION N-STREAM ******************************************************) + +rec definition apply (i: pnat) on i: rtmap → pnat. +* #p #f cases i -i +[ @p +| #i lapply (apply i f) -apply -i -f + #i @(i+p) +] +defined. + +interpretation "functional application (nstream)" + 'Apply f i = (apply i f). + +(* Specific properties on at ************************************************) + +lemma at_O1: ∀i2,f. @❪𝟏, i2⨮f❫ ≘ i2. +#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/ +qed. + +lemma at_S1: ∀p,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, p⨮f❫ ≘ i2+p. +#p elim p -p /3 width=7 by at_push, at_next/ +qed. + +lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩. +#i1 elim i1 -i1 +[ * // | #i #IH * /3 width=1 by at_S1/ ] +qed. + +lemma at_istot: ∀f. 𝐓❪f❫. +/2 width=2 by ex_intro/ qed. + +lemma at_plus2: ∀f,i1,i,p,q. @❪i1, p⨮f❫ ≘ i → @❪i1, (p+q)⨮f❫ ≘ i+q. +#f #i1 #i #p #q #H elim q -q +/2 width=5 by at_next/ +qed. + +(* Specific inversion lemmas on at ******************************************) + +lemma at_inv_O1: ∀f,p,i2. @❪𝟏, p⨮f❫ ≘ i2 → p = i2. +#f #p elim p -p /2 width=6 by at_inv_ppx/ +#p #IH #i2 #H elim (at_inv_xnx … H) -H [|*: // ] +#j2 #Hj * -i2 /3 width=1 by eq_f/ +qed-. + +lemma at_inv_S1: ∀f,p,j1,i2. @❪↑j1, p⨮f❫ ≘ i2 → + ∃∃j2. @❪j1, f❫ ≘ j2 & j2+p = i2. +#f #p elim p -p /2 width=5 by at_inv_npx/ +#p #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [|*: // ] +#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj +#i2 #Hi * -j2 /2 width=3 by ex2_intro/ +qed-. + +lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2. +/2 width=6 by at_mono/ qed-. + +(* Spercific forward lemmas on at *******************************************) + +lemma at_increasing_plus: ∀f,p,i1,i2. @❪i1, p⨮f❫ ≘ i2 → i1 + p ≤ ↑i2. +#f #p * +[ #i2 #H <(at_inv_O1 … H) -i2 // +| #i1 #i2 #H elim (at_inv_S1 … H) -H + #j1 #Ht * -i2 apply_S1 >apply_S1 /3 width=1 by eq_f2/ +qed. + +lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩). +* #p #f * // +qed. + +(* Main inversion lemmas ****************************************************) + +theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2. +/2 width=4 by at_inj/ qed-. + +corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2. +* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons +[ @(Hf (𝟏)) +| @nstream_eq_inv_ext -nstream_eq_inv_ext #i + lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct + lapply (Hf (↑i)) >apply_S1 >apply_S1 #H + /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_sor.ma new file mode 100644 index 000000000..2e7758110 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_sor.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/relocation/rtmap_sor.ma". + +(* RELOCATION N-STREAM ******************************************************) + +axiom union: rtmap → rtmap → rtmap. + +interpretation "union (nstream)" + 'union f1 f2 = (union f1 f2). + +(* Specific properties on sor ***********************************************) + +axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≘ f1 ∪ f2. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_tl.ma new file mode 100644 index 000000000..318b7da88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_tl.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/lib/stream_hdtl.ma". +include "ground/relocation/pstream.ma". + +(* RELOCATION P-STREAM ******************************************************) + +(* Poperties with stream_tl *************************************************) + +lemma tl_push: ∀f. f = ⫰⫯f. +// qed. + +lemma tl_next: ∀f. ⫰f = ⫰↑f. +* // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pstream_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_tls.ma new file mode 100644 index 000000000..e7232fa8b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pstream_tls.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/lib/stream_tls.ma". +include "ground/arith/nat_pred_succ.ma". +include "ground/relocation/pstream_tl.ma". + +(* RELOCATION P-STREAM ******************************************************) + +(* Poperties with stream_tls ************************************************) + +lemma tls_next: ∀f. ∀p:pnat. ⫰*[p]f = ⫰*[p]↑f. +#f #p >(npsucc_pred p) nsucc_inj + elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ] + [ #g2 #j1 #Hg2 #H1 #H2 destruct >nsucc_inj in Hf; #Hf + elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct + nsucc_inj #Hf + elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct + elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ] + [ #g2 #j1 #Hg2 #H1 #H2 destruct (at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/ ] qed-. -lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 0 = i2 → 0 = i1. +lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1. #f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * // #j1 #j2 #_ #_ * -i2 #H destruct qed-. @@ -142,8 +147,8 @@ lemma at_inv_xpn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 ] qed-. -lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 0 = i2 → - ∃∃g. 0 = i1 & ⫯g = f. +lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i2 → + ∃∃g. 𝟏 = i1 & ⫯g = f. #f elim (pn_split f) * #g #H #i1 #i2 #Hf #H2 [ /3 width=6 by at_inv_xpp, ex2_intro/ @@ -168,21 +173,21 @@ lemma at_increasing: ∀i2,i1,f. @❪i1,f❫ ≘ i2 → i1 ≤ i2. [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // | #i2 #IH * // #i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ] - /3 width=2 by le_S_S, le_S/ + /3 width=2 by ple_succ_bi, ple_succ_dx/ ] qed-. lemma at_increasing_strict: ∀g,i1,i2. @❪i1,g❫ ≘ i2 → ∀f. ↑f = g → i1 < i2 ∧ @❪i1,f❫ ≘ ↓i2. #g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H -/4 width=2 by conj, at_increasing, le_S_S/ +/4 width=2 by conj, at_increasing, ple_succ_bi/ qed-. lemma at_fwd_id_ex: ∀f,i. @❪i,f❫ ≘ i → ∃g. ⫯g = f. #f elim (pn_split f) * /2 width=2 by ex_intro/ #g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H #j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg -#H elim (lt_le_false … H) -H // +#H elim (plt_ge_false … H) -H // qed-. (* Basic properties *********************************************************) @@ -205,20 +210,20 @@ lemma at_le_ex: ∀j2,i2,f. @❪i2,f❫ ≘ j2 → ∀i1. i1 ≤ i2 → [ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] #g [ #x2 ] #Hg [ #H2 ] #H0 [ * /3 width=3 by at_refl, ex2_intro/ - #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12 + #i1 #Hi12 destruct lapply (ple_inv_succ_bi … Hi12) -Hi12 #Hi12 elim (IH … Hg … Hi12) -x2 -IH - /3 width=7 by at_push, ex2_intro, le_S_S/ + /3 width=7 by at_push, ex2_intro, ple_succ_bi/ | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2 - /3 width=5 by at_next, ex2_intro, le_S_S/ + /3 width=5 by at_next, ex2_intro, ple_succ_bi/ ] | elim (at_inv_xxp … Hf) -Hf // - #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12) + #g * -i2 #H2 #i1 #Hi12 <(ple_inv_unit_dx … Hi12) /3 width=3 by at_refl, ex2_intro/ ] qed-. 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 ] +#i1 #i2 #H @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ] #f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/ qed-. @@ -228,14 +233,14 @@ theorem at_monotonic: ∀j2,i2,f. @❪i2,f❫ ≘ j2 → ∀j1,i1. @❪i1,f❫ i1 < i2 → j1 < j2. #j2 elim j2 -j2 [ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f // - #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi // + #g #H21 #_ #j1 #i1 #_ #Hi elim (plt_ge_false … Hi) -Hi // | #j2 #IH #i2 #f #H2f * // - #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi) - #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ] + #j1 #i1 #H1f #Hi elim (plt_inv_gen … Hi) + #_ #Hi2 elim (at_inv_nxn … H2f (↓i2)) -H2f [1,3: * |*: // ] #g #H2g #H [ elim (at_inv_xpn … H1f … H) -f - /4 width=8 by lt_S_S_to_lt, lt_S_S/ - | /4 width=8 by at_inv_xnn, lt_S_S/ + /4 width=8 by plt_inv_succ_bi, plt_succ_bi/ + | /4 width=8 by at_inv_xnn, plt_succ_bi/ ] ] qed-. @@ -244,17 +249,17 @@ theorem at_inv_monotonic: ∀j1,i1,f. @❪i1,f❫ ≘ j1 → ∀j2,i2. @❪i2,f j1 < j2 → i1 < i2. #j1 elim j1 -j1 [ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f // - #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj - #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f // + #g * -i1 #H #j2 #i2 #H2f #Hj lapply (plt_des_gen … Hj) -Hj + #H22 elim (at_inv_xpn … H2f … (↓j2) H) -f // | #j1 #IH * [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ] - #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj + #g #H1g #H #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj /3 width=7 by at_inv_xnn/ - | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj - #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ] + | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj + #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ] #g #Hg #H - [ elim (at_inv_xpn … H2f … H H22) -f -H22 - /3 width=7 by lt_S_S/ + [ elim (at_inv_xpn … H2f … (↓j2) H) -f + /3 width=7 by plt_succ_bi/ | /3 width=7 by at_inv_xnn/ ] ] @@ -262,13 +267,13 @@ theorem at_inv_monotonic: ∀j1,i1,f. @❪i1,f❫ ≘ j1 → ∀j2,i2. @❪i2,f qed-. theorem at_mono: ∀f,i,i1. @❪i,f❫ ≘ i1 → ∀i2. @❪i,f❫ ≘ i2 → i2 = i1. -#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // -#Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/ +#f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) // +#Hi elim (plt_ge_false i i) /3 width=6 by at_inv_monotonic, eq_sym/ qed-. theorem at_inj: ∀f,i1,i. @❪i1,f❫ ≘ i → ∀i2. @❪i2,f❫ ≘ i → i1 = i2. -#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // -#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/ +#f #i1 #i #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) // +#Hi elim (plt_ge_false i i) /2 width=6 by at_monotonic/ qed-. theorem at_div_comm: ∀f2,g2,f1,g1. @@ -312,17 +317,19 @@ theorem at_div_pn: ∀f2,g2,f1,g1. (* Properties on tls ********************************************************) -lemma at_pxx_tls: ∀n,f. @❪0,f❫ ≘ n → @❪0,⫱*[n]f❫ ≘ 0. -#n elim n -n // +(* Note: this requires ↑ on first n *) +lemma at_pxx_tls: ∀n,f. @❪𝟏,f❫ ≘ ↑n → @❪𝟏,⫱*[n]f❫ ≘ 𝟏. +#n @(nat_ind_succ … n) -n // #n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct pushs_S // qed. -lemma at_basic_ge: ∀m,n,i. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ n+i. -#m elim m -m // -#m #IH #n #j #H -elim (le_inv_S1 … H) -H #i #Hmi #H destruct -/3 width=7 by refl, at_push/ +lemma at_basic_zero_succ (n): ↑𝐁❨𝟎,n❩ = 𝐁❨𝟎,↑n❩. +#n >nexts_S // qed. - -(* Inversion lemmas with application ****************************************) - -lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @❪i, 𝐁❨m,n❩❫ ≘ j → i = j. -/3 width=4 by at_basic_lt, at_mono/ qed-. - -lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ j → n+i = j. -/3 width=4 by at_basic_ge, at_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_after.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_after.ma index 3bcde3092..792fa995d 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_after.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_basic_after.ma @@ -12,28 +12,26 @@ (* *) (**************************************************************************) -include "ground/relocation/rtmap_after.ma". +include "ground/arith/nat_le_pred.ma". +include "ground/relocation/rtmap_after_uni.ma". include "ground/relocation/rtmap_basic.ma". (* RELOCATION MAP ***********************************************************) (* Properties with composition **********************************************) -lemma after_basic_rc (m2,m1,n2,n1): - m1 ≤ m2 → m2 ≤ m1+n1 → 𝐁❨m2,n2❩ ⊚ 𝐁❨m1,n1❩ ≘ 𝐁❨m1,n2+n1❩. -#m2 elim m2 -m2 -[ #m1 #n2 #n1 #Hm21 #_ - <(le_n_O_to_eq … Hm21) -m1 // -| #m2 #IH * - [ #n2 #n1 #_ < plus_O_n #H - elim (le_inv_S1 … H) -H #x #Hx #H destruct - Hn1 -Hn1 (npsucc_pred i) #Hmi +/2 width=1 by rm_nat_basic_lt/ +qed. + +lemma at_basic_ge (m) (n) (i): + m < ninj i → @❪i, 𝐁❨m,n❩❫ ≘ i+n. +#m #n #i >(npsucc_pred i) #Hmi H -H +/3 width=7 by rm_nat_push/ +qed. + +(* Inversion lemmas with application ****************************************) + +lemma rm_nat_basic_inv_lt (m) (n) (l) (k): + l < m → @↑❪l, 𝐁❨m,n❩❫ ≘ k → l = k. +/3 width=4 by rm_nat_basic_lt, rm_nat_mono/ qed-. + +lemma rm_nat_basic_inv_ge (m) (n) (l) (k): + m ≤ l → @↑❪l, 𝐁❨m,n❩❫ ≘ k → l+n = k. +/3 width=4 by rm_nat_basic_ge, rm_nat_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_coafter.ma index e74866dac..aede6b3a3 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_coafter.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_coafter.ma @@ -14,6 +14,7 @@ include "ground/notation/relations/rcoafter_3.ma". include "ground/relocation/rtmap_sor.ma". +include "ground/relocation/rtmap_nat.ma". include "ground/relocation/rtmap_after.ma". (* RELOCATION MAP ***********************************************************) @@ -238,21 +239,21 @@ lemma coafter_mono_eq: ∀f1,f2,f. f1 ~⊚ f2 ≘ f → ∀g1,g2,g. g1 ~⊚ g2 (* Forward lemmas with pushs ************************************************) -lemma coafter_fwd_pushs: ∀j,i,g2,f1,g. g2 ~⊚ ⫯*[i]f1 ≘ g → @❪i, g2❫ ≘ j → - ∃f. ⫯*[j] f = g. -#j elim j -j -[ #i #g2 #f1 #g #Hg #H - elim (at_inv_xxp … H) -H [|*: // ] #f2 #H1 #H2 destruct - /2 width=2 by ex_intro/ -| #j #IH * [| #i ] #g2 #f1 #g #Hg #H - [ elim (at_inv_pxn … H) -H [|*: // ] #f2 #Hij #H destruct +lemma coafter_fwd_pushs: ∀k,l,g2,f1,g. g2 ~⊚ ⫯*[l]f1 ≘ g → @↑❪l, g2❫ ≘ k → + ∃∃f. ⫱*[k]g2 ~⊚ f1 ≘ f & ⫯*[k] f = g. +#k @(nat_ind_succ … k) -k +[ #l #g2 #f1 #g #Hg #H + elim (rm_nat_inv_xxp … H) -H [|*: // ] #f2 #H1 #H2 destruct + /2 width=3 by ex2_intro/ +| #k #IH * [| #l ] #g2 #f1 #g #Hg #H + [ elim (rm_nat_inv_pxn … H) -H [|*: // ] #f2 #Hlk #H destruct elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct - elim (IH … Hf Hij) -f1 -f2 -IH /2 width=2 by ex_intro/ - | elim (at_inv_nxn … H) -H [1,4: * |*: // ] #f2 #Hij #H destruct + elim (IH … Hf Hlk) -IH -Hf -Hlk /2 width=3 by ex2_intro/ + | elim (rm_nat_inv_nxn … H) -H [1,4: * |*: // ] #f2 #Hlk #H destruct [ elim (coafter_inv_ppx … Hg) -Hg [|*: // ] #f #Hf #H destruct - elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/ + elim (IH … Hf Hlk) -IH -Hf -Hlk /2 width=3 by ex2_intro/ | elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct - elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/ + elim (IH … Hf Hlk) -IH -Hf -Hlk /2 width=3 by ex2_intro/ ] ] ] @@ -278,14 +279,14 @@ qed-. (* Properties with iterated tail ********************************************) -lemma coafter_tls: ∀j,i,f1,f2,f. @❪i, f1❫ ≘ j → - f1 ~⊚ f2 ≘ f → ⫱*[j]f1 ~⊚ ⫱*[i]f2 ≘ ⫱*[j]f. -#j elim j -j [ #i | #j #IH * [| #i ] ] #f1 #f2 #f #Hf1 #Hf -[ elim (at_inv_xxp … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct // -| elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 +lemma coafter_tls: ∀l2,l1,f1,f2,f. @↑❪l1, f1❫ ≘ l2 → + f1 ~⊚ f2 ≘ f → ⫱*[l2]f1 ~⊚ ⫱*[l1]f2 ≘ ⫱*[l2]f. +#l2 @(nat_ind_succ … l2) -l2 [ #l1 | #l2 #IH * [| #l1 ] ] #f1 #f2 #f #Hf1 #Hf +[ elim (rm_nat_inv_xxp … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct // +| elim (rm_nat_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 elim (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct lapply (IH … Hg1 Hg) -IH -Hg1 -Hg // -| elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ] #g1 #Hg1 #H1 +| elim (rm_nat_inv_xxn … Hf1) -Hf1 [1,3: * |*: // ] #g1 [ #k1 ] #Hg1 [ #H ] #H1 [ elim (coafter_inv_pxx … Hf … H1) -Hf * #g2 #g #Hg #H2 #H0 destruct lapply (IH … Hg1 Hg) -IH -Hg1 -Hg #H // | elim (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct @@ -294,24 +295,25 @@ lemma coafter_tls: ∀j,i,f1,f2,f. @❪i, f1❫ ≘ j → ] qed. -lemma coafter_tls_O: ∀n,f1,f2,f. @❪0, f1❫ ≘ n → - f1 ~⊚ f2 ≘ f → ⫱*[n]f1 ~⊚ f2 ≘ ⫱*[n]f. +lemma coafter_tls_O: ∀k,f1,f2,f. @↑❪𝟎, f1❫ ≘ k → + f1 ~⊚ f2 ≘ f → ⫱*[k]f1 ~⊚ f2 ≘ ⫱*[k]f. /2 width=1 by coafter_tls/ qed. +(* Note: this does not require ↑ first and second j *) lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≘ g → - ∀n. @❪0, g2❫ ≘ n → ⫱*[↑n]g2 ~⊚ ⫱g1 ≘ ⫱*[↑n]g. -#g2 #g1 #g #Hg #n #Hg2 + ∀j. @❪𝟏, g2❫ ≘ j → ⫱*[j]g2 ~⊚ ⫱g1 ≘ ⫱*[j]g. +#g2 #g1 #g #Hg #j #Hg2 +lapply (rm_nat_pred_bi … Hg2) -Hg2 #Hg2 lapply (coafter_tls … Hg2 … Hg) -Hg #Hg lapply (at_pxx_tls … Hg2) -Hg2 #H elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2 -elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct -(npsucc_pred j) IH // ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_id.ma index 6446254d0..2ab5b383e 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_id.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_id.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/relocation/nstream_id.ma". +include "ground/relocation/pstream_id.ma". include "ground/relocation/rtmap_isid.ma". (* RELOCATION MAP ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma index 1b6ce598e..fa421497a 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isdiv.ma @@ -79,13 +79,13 @@ qed-. (* Properties with iterated next ********************************************) lemma isdiv_nexts: ∀n,f. 𝛀❪f❫ → 𝛀❪↑*[n]f❫. -#n elim n -n /3 width=3 by isdiv_next/ +#n @(nat_ind_succ … n) -n /3 width=3 by isdiv_next/ qed. (* Inversion lemmas with iterated next **************************************) lemma isdiv_inv_nexts: ∀n,g. 𝛀❪↑*[n]g❫ → 𝛀❪g❫. -#n elim n -n /3 width=3 by isdiv_inv_next/ +#n @(nat_ind_succ … n) -n /3 width=3 by isdiv_inv_next/ qed. (* Properties with tail *****************************************************) @@ -100,5 +100,5 @@ qed. (* Properties with iterated tail ********************************************) lemma isdiv_tls: ∀n,g. 𝛀❪g❫ → 𝛀❪⫱*[n]g❫. -#n elim n -n /3 width=1 by isdiv_tl/ +#n @(nat_ind_succ … n) -n /3 width=1 by isdiv_tl/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma index 5439f36ee..7da7f85ad 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isfin.ma @@ -67,13 +67,13 @@ qed. (* Properties with iterated push ********************************************) lemma isfin_pushs: ∀n,f. 𝐅❪f❫ → 𝐅❪⫯*[n]f❫. -#n elim n -n /3 width=3 by isfin_push/ +#n @(nat_ind_succ … n) -n /3 width=3 by isfin_push/ qed. (* Inversion lemmas with iterated push **************************************) lemma isfin_inv_pushs: ∀n,g. 𝐅❪⫯*[n]g❫ → 𝐅❪g❫. -#n elim n -n /3 width=3 by isfin_inv_push/ +#n @(nat_ind_succ … n) -n /3 width=3 by isfin_inv_push/ qed. (* Properties with tail *****************************************************) @@ -92,5 +92,5 @@ qed-. (* Inversion lemmas with iterated tail **************************************) lemma isfin_inv_tls: ∀n,f. 𝐅❪⫱*[n]f❫ → 𝐅❪f❫. -#n elim n -n /3 width=1 by isfin_inv_tl/ +#n @(nat_ind_succ … n) -n /3 width=1 by isfin_inv_tl/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isid.ma index e43b0bc08..f52700b3e 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isid.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_isid.ma @@ -78,13 +78,13 @@ qed-. (* Properties with iterated push ********************************************) lemma isid_pushs: ∀n,f. 𝐈❪f❫ → 𝐈❪⫯*[n]f❫. -#n elim n -n /3 width=3 by isid_push/ +#n @(nat_ind_succ … n) -n /3 width=3 by isid_push/ qed. (* Inversion lemmas with iterated push **************************************) lemma isid_inv_pushs: ∀n,g. 𝐈❪⫯*[n]g❫ → 𝐈❪g❫. -#n elim n -n /3 width=3 by isid_inv_push/ +#n @(nat_ind_succ … n) -n /3 width=3 by isid_inv_push/ qed. (* Properties with tail *****************************************************) @@ -99,5 +99,5 @@ qed. (* Properties with iterated tail ********************************************) lemma isid_tls: ∀n,g. 𝐈❪g❫ → 𝐈❪⫱*[n]g❫. -#n elim n -n /3 width=1 by isid_tl/ +#n @(nat_ind_succ … n) -n /3 width=1 by isid_tl/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_istot.ma index 472a66945..f93936acf 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_istot.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/relations/istotal_1.ma". +include "ground/notation/relations/ist_1.ma". include "ground/relocation/rtmap_at.ma". (* RELOCATION MAP ***********************************************************) @@ -20,7 +20,7 @@ include "ground/relocation/rtmap_at.ma". definition istot: predicate rtmap ≝ λf. ∀i. ∃j. @❪i,f❫ ≘ j. interpretation "test for totality (rtmap)" - 'IsTotal f = (istot f). + 'IsT f = (istot f). (* Basic inversion lemmas ***************************************************) @@ -44,7 +44,9 @@ qed. (* Properties on tls ********************************************************) lemma istot_tls: ∀n,f. 𝐓❪f❫ → 𝐓❪⫱*[n]f❫. -#n elim n -n /3 width=1 by istot_tl/ +#n @(nat_ind_succ … n) -n // +#n #IH #f #Hf (npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?); +// +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma rm_nat_inv_ppx (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2. +#f #l1 #l2 #H #g #H1 #H2 destruct +lapply (at_inv_ppx … H ???) -H +/2 width=2 by eq_inv_npsucc_bi/ +qed-. + +lemma rm_nat_inv_npx (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → + ∃∃k2. @↑❪k1,g❫ ≘ k2 & ↑k2 = l2. +#f #l1 #l2 #H #g #k1 #H1 #H2 destruct +elim (at_inv_npx … H) -H [|*: // ] #k2 #Hg +>(npsucc_pred (↑l2)) #H +@(ex2_intro … (↓k2)) // +(npsucc_pred (k2)) in ⊢ (%→?→?); #Hg #H +@(ex2_intro … (↓k2)) // +(eq_inv_nsucc_bi … H) -k2 // +qed-. + +lemma rm_nat_inv_xnp (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥. +#f #l1 #l2 #Hf #g #H elim (rm_nat_inv_xnx … Hf … H) -f +#x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/ +qed-. + +lemma rm_nat_inv_xnn (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → @↑❪l1,g❫ ≘ k2. +#f #l1 #l2 #Hf #g #k2 #H elim (rm_nat_inv_xnx … Hf … H) -f +#x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 // +qed-. + +lemma rm_nat_inv_pxp (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f. +#f elim (pn_split … f) * /2 width=2 by ex_intro/ +#g #H #l1 #l2 #Hf #H1 #H2 cases (rm_nat_inv_xnp … Hf … H H2) +qed-. + +lemma rm_nat_inv_pxn (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 → + ∃∃g. @↑❪l1,g❫ ≘ k2 & ↑g = f. +#f elim (pn_split … f) * +#g #H #l1 #l2 #Hf #k2 #H1 #H2 +[ elim (rm_nat_inv_ppn … Hf … H1 H H2) +| /3 width=5 by rm_nat_inv_xnn, ex2_intro/ +] +qed-. + +lemma rm_nat_inv_nxp (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥. +#f elim (pn_split f) * +#g #H #l1 #l2 #Hf #k1 #H1 #H2 +[ elim (rm_nat_inv_npp … Hf … H1 H H2) +| elim (rm_nat_inv_xnp … Hf … H H2) +] +qed-. + +lemma rm_nat_inv_nxn (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 → + ∨∨ ∃∃g. @↑❪k1,g❫ ≘ k2 & ⫯g = f + | ∃∃g. @↑❪l1,g❫ ≘ k2 & ↑g = f. +#f elim (pn_split f) * +/4 width=7 by rm_nat_inv_xnn, rm_nat_inv_npn, ex2_intro, or_intror, or_introl/ +qed-. + +(* Note: the following inversion lemmas must be checked *) +lemma rm_nat_inv_xpx (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g. ⫯g = f → + ∨∨ ∧∧ 𝟎 = l1 & 𝟎 = l2 + | ∃∃k1,k2. @↑❪k1,g❫ ≘ k2 & ↑k1 = l1 & ↑k2 = l2. +#f * [2: #l1 ] #l2 #Hf #g #H +[ elim (rm_nat_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/ +| >(rm_nat_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/ +] +qed-. + +lemma rm_nat_inv_xpp (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1. +#f #l1 #l2 #Hf #g #H elim (rm_nat_inv_xpx … Hf … H) -f * // +#k1 #k2 #_ #_ * -l2 #H elim (eq_inv_zero_nsucc … H) +qed-. + +lemma rm_nat_inv_xpn (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 → + ∃∃k1. @↑❪k1,g❫ ≘ k2 & ↑k1 = l1. +#f #l1 #l2 #Hf #g #k2 #H elim (rm_nat_inv_xpx … Hf … H) -f * +[ #_ * -l2 #H elim (eq_inv_nsucc_zero … H) +| #x1 #x2 #Hg #H1 * -l2 #H + lapply (eq_inv_nsucc_bi … H) -H #H destruct + /2 width=3 by ex2_intro/ +] +qed-. + +lemma rm_nat_inv_xxp (f) (l1) (l2): + @↑❪l1,f❫ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f. +#f elim (pn_split f) * +#g #H #l1 #l2 #Hf #H2 +[ /3 width=6 by rm_nat_inv_xpp, ex2_intro/ +| elim (rm_nat_inv_xnp … Hf … H H2) +] +qed-. + +lemma rm_nat_inv_xxn (f) (l1) (l2): @↑❪l1,f❫ ≘ l2 → ∀k2. ↑k2 = l2 → + ∨∨ ∃∃g,k1. @↑❪k1,g❫ ≘ k2 & ↑k1 = l1 & ⫯g = f + | ∃∃g. @↑❪l1,g❫ ≘ k2 & ↑g = f. +#f elim (pn_split f) * +#g #H #l1 #l2 #Hf #k2 #H2 +[ elim (rm_nat_inv_xpn … Hf … H H2) -l2 /3 width=5 by or_introl, ex3_2_intro/ +| lapply (rm_nat_inv_xnn … Hf … H H2) -l2 /3 width=3 by or_intror, ex2_intro/ +] +qed-. + +(* Main destructions ********************************************************) + +theorem rm_nat_monotonic (k2) (l2) (f): + @↑❪l2,f❫ ≘ k2 → ∀k1,l1. @↑❪l1,f❫ ≘ k1 → l1 < l2 → k1 < k2. +#k2 @(nat_ind_succ … k2) -k2 +[ #l2 #f #H2f elim (rm_nat_inv_xxp … H2f) -H2f // + #g #H21 #_ #k1 #l1 #_ #Hi destruct + elim (nlt_inv_zero_dx … Hi) +| #k2 #IH #l2 #f #H2f #k1 @(nat_ind_succ … k1) -k1 // + #k1 #_ #l1 #H1f #Hl elim (nlt_inv_gen … Hl) + #_ #Hl2 elim (rm_nat_inv_nxn … H2f (↓l2)) -H2f [1,3: * |*: // ] + #g #H2g #H + [ elim (rm_nat_inv_xpn … H1f … H) -f + /4 width=8 by nlt_inv_succ_bi, nlt_succ_bi/ + | /4 width=8 by rm_nat_inv_xnn, nlt_succ_bi/ + ] +] +qed-. + +theorem rm_nat_inv_monotonic (k1) (l1) (f): + @↑❪l1,f❫ ≘ k1 → ∀k2,l2. @↑❪l2,f❫ ≘ k2 → k1 < k2 → l1 < l2. +#k1 @(nat_ind_succ … k1) -k1 +[ #l1 #f #H1f elim (rm_nat_inv_xxp … H1f) -H1f // + #g * -l1 #H #k2 #l2 #H2f #Hk + lapply (nlt_des_gen … Hk) -Hk #H22 + elim (rm_nat_inv_xpn … H2f … (↓k2) H) -f // +| #k1 #IH #l1 @(nat_ind_succ … l1) -l1 + [ #f #H1f elim (rm_nat_inv_pxn … H1f) -H1f [ |*: // ] + #g #H1g #H #k2 #l2 #H2f #Hj elim (nlt_inv_succ_sn … Hj) -Hj + /3 width=7 by rm_nat_inv_xnn/ + | #l1 #_ #f #H1f #k2 #l2 #H2f #Hj elim (nlt_inv_succ_sn … Hj) -Hj + #Hj #H22 elim (rm_nat_inv_nxn … H1f) -H1f [1,4: * |*: // ] + #g #Hg #H + [ elim (rm_nat_inv_xpn … H2f … (↓k2) H) -f + /3 width=7 by nlt_succ_bi/ + | /3 width=7 by rm_nat_inv_xnn/ + ] + ] +] +qed-. + +theorem rm_nat_mono (f) (l) (l1) (l2): + @↑❪l,f❫ ≘ l1 → @↑❪l,f❫ ≘ l2 → l2 = l1. +#f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) // +#Hi elim (nlt_ge_false l l) /3 width=6 by rm_nat_inv_monotonic, eq_sym/ +qed-. + +theorem rm_nat_inj (f) (l1) (l2) (l): + @↑❪l1,f❫ ≘ l → @↑❪l2,f❫ ≘ l → l1 = l2. +#f #l1 #l2 #l #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) // +#Hi elim (nlt_ge_false l l) /2 width=6 by rm_nat_monotonic/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nat_uni.ma new file mode 100644 index 000000000..3faf3c95c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nat_uni.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/arith/nat_plus.ma". +include "ground/relocation/rtmap_uni.ma". +include "ground/relocation/rtmap_nat.ma". + +(* NON-NEGATIVE APPLICATION FOR RELOCATION MAPS *****************************) + +(* Properties with uniform relocations **************************************) + +lemma rm_nat_uni (n) (l): @↑❪l,𝐔❨n❩❫ ≘ l+n. +#n @(nat_ind_succ … n) -n /2 width=5 by rm_nat_next/ +qed. + +(* Inversion lemmas with uniform relocations ********************************) + +lemma rm_nat_inv_uni (n) (l) (k): @↑❪l,𝐔❨n❩❫ ≘ k → k = l+n. +/2 width=4 by rm_nat_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nexts.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nexts.ma index 08851ebe6..128c26d64 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nexts.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_nexts.ma @@ -13,20 +13,42 @@ (**************************************************************************) include "ground/notation/functions/uparrowstar_2.ma". +include "ground/arith/nat_succ_iter.ma". include "ground/relocation/rtmap_eq.ma". (* RELOCATION MAP ***********************************************************) -rec definition nexts (f:rtmap) (n:nat) on n: rtmap ≝ match n with -[ O ⇒ f | S m ⇒ ↑(nexts f m) ]. +definition nexts (f:rtmap) (n:nat) ≝ next^n f. interpretation "nexts (rtmap)" 'UpArrowStar n f = (nexts f n). +(* Basic properties *********************************************************) + +lemma nexts_O: ∀f. f = ↑*[𝟎] f. +// qed. + +lemma nexts_S: ∀f,n. ↑↑*[n] f = ↑*[↑n] f. +#f #n @(niter_succ … next) +qed. + +lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ↑*[n] f1 ≡ ↑*[n] f2). +#n @(nat_ind_succ … n) -n /3 width=5 by eq_next/ +qed. + +(* Advanced properties ******************************************************) + +lemma nexts_swap: ∀f,n. ↑↑*[n] f = ↑*[n] ↑f. +#f #n @(niter_appl … next) +qed. + +lemma nexts_xn: ∀n,f. ↑*[n] ↑f = ↑*[↑n] f. +// qed. + (* Basic_inversion lemmas *****************************************************) lemma eq_inv_nexts_sn: ∀n,f1,g2. ↑*[n] f1 ≡ g2 → ∃∃f2. f1 ≡ f2 & ↑*[n] f2 = g2. -#n elim n -n /2 width=3 by ex2_intro/ +#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/ #n #IH #f1 #g2 #H elim (eq_inv_nx … H) -H [|*: // ] #f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct /2 width=3 by ex2_intro/ @@ -34,26 +56,8 @@ qed-. lemma eq_inv_nexts_dx: ∀n,f2,g1. g1 ≡ ↑*[n] f2 → ∃∃f1. f1 ≡ f2 & ↑*[n] f1 = g1. -#n elim n -n /2 width=3 by ex2_intro/ +#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/ #n #IH #f2 #g1 #H elim (eq_inv_xn … H) -H [|*: // ] #f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct /2 width=3 by ex2_intro/ qed-. - -(* Basic properties *********************************************************) - -lemma nexts_O: ∀f. f = ↑*[0] f. -// qed. - -lemma nexts_S: ∀f,n. ↑↑*[n] f = ↑*[↑n] f. -// qed. - -lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ↑*[n] f1 ≡ ↑*[n] f2). -#n elim n -n /3 width=5 by eq_next/ -qed. - -(* Advanced properties ******************************************************) - -lemma nexts_xn: ∀n,f. ↑*[n] ↑f = ↑*[↑n] f. -#n elim n -n // -qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_pushs.ma index 420143933..5c43f1872 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_pushs.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_pushs.ma @@ -13,20 +13,42 @@ (**************************************************************************) include "ground/notation/functions/upspoonstar_2.ma". +include "ground/arith/nat_succ_iter.ma". include "ground/relocation/rtmap_eq.ma". (* RELOCATION MAP ***********************************************************) -rec definition pushs (f:rtmap) (n:nat) on n: rtmap ≝ match n with -[ O ⇒ f | S m ⇒ ⫯(pushs f m) ]. +definition pushs (f:rtmap) (n:nat) ≝ push^n f. interpretation "pushs (rtmap)" 'UpSpoonStar n f = (pushs f n). +(* Basic properties *********************************************************) + +lemma pushs_O: ∀f. f = ⫯*[𝟎] f. +// qed. + +lemma pushs_S: ∀f,n. ⫯⫯*[n] f = ⫯*[↑n] f. +#f #n @(niter_succ … push) +qed. + +lemma pushs_eq_repl: ∀n. eq_repl (λf1,f2. ⫯*[n] f1 ≡ ⫯*[n] f2). +#n @(nat_ind_succ … n) -n /3 width=5 by eq_push/ +qed. + +(* Advanced properties ******************************************************) + +lemma push_swap (n) (f): ⫯⫯*[n] f = ⫯*[n] ⫯f. +#n #f @(niter_appl … push) +qed. + +lemma pushs_xn: ∀n,f. ⫯*[n] ⫯f = ⫯*[↑n] f. +// qed. + (* Basic_inversion lemmas *****************************************************) lemma eq_inv_pushs_sn: ∀n,f1,g2. ⫯*[n] f1 ≡ g2 → ∃∃f2. f1 ≡ f2 & ⫯*[n] f2 = g2. -#n elim n -n /2 width=3 by ex2_intro/ +#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/ #n #IH #f1 #g2 #H elim (eq_inv_px … H) -H [|*: // ] #f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct /2 width=3 by ex2_intro/ @@ -34,26 +56,8 @@ qed-. lemma eq_inv_pushs_dx: ∀n,f2,g1. g1 ≡ ⫯*[n] f2 → ∃∃f1. f1 ≡ f2 & ⫯*[n] f1 = g1. -#n elim n -n /2 width=3 by ex2_intro/ +#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/ #n #IH #f2 #g1 #H elim (eq_inv_xp … H) -H [|*: // ] #f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct /2 width=3 by ex2_intro/ qed-. - -(* Basic properties *********************************************************) - -lemma pushs_O: ∀f. f = ⫯*[0] f. -// qed. - -lemma pushs_S: ∀f,n. ⫯⫯*[n] f = ⫯*[↑n] f. -// qed. - -lemma pushs_eq_repl: ∀n. eq_repl (λf1,f2. ⫯*[n] f1 ≡ ⫯*[n] f2). -#n elim n -n /3 width=5 by eq_push/ -qed. - -(* Advanced properties ******************************************************) - -lemma pushs_xn: ∀n,f. ⫯*[n] ⫯f = ⫯*[↑n] f. -#n elim n -n // -qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma index edd962354..002e6eac7 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sle.ma @@ -111,10 +111,11 @@ corec theorem sle_trans: Transitive … sle. /3 width=5 by sle_push, sle_next, sle_weak/ qed-. -(* Properties with iteraded push ********************************************) +(* Properties with iterated push ********************************************) -lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ⫯*[i] f1 ⊆ ⫯*[i] f2. -#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/ +lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀n. ⫯*[n] f1 ⊆ ⫯*[n] f2. +#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n +/2 width=5 by sle_push/ qed. (* Properties with tail *****************************************************) @@ -148,8 +149,9 @@ qed-. (* Properties with iteraded tail ********************************************) -lemma sle_tls: ∀f1,f2. f1 ⊆ f2 → ∀i. ⫱*[i] f1 ⊆ ⫱*[i] f2. -#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_tl/ +lemma sle_tls: ∀f1,f2. f1 ⊆ f2 → ∀n. ⫱*[n] f1 ⊆ ⫱*[n] f2. +#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n +/2 width=5 by sle_tl/ qed. (* Properties with isid *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma index 0b3f0ddaa..bcc705521 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma @@ -12,8 +12,12 @@ (* *) (**************************************************************************) +include "ground/xoa/or_3.ma". +include "ground/xoa/ex_3_1.ma". include "ground/xoa/ex_4_2.ma". include "ground/notation/relations/runion_3.ma". +include "ground/arith/nat_plus.ma". +include "ground/arith/nat_le_max.ma". include "ground/relocation/rtmap_isfin.ma". include "ground/relocation/rtmap_sle.ma". @@ -305,7 +309,8 @@ qed-. lemma sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≘ f → ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≘ ⫱*[n]f. -#f1 #f2 #f #Hf #n elim n -n /2 width=1 by sor_tl/ +#f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n +/2 width=1 by sor_tl/ qed. (* Properies with test for identity *****************************************) @@ -370,11 +375,11 @@ lemma sor_fcla_ex: ∀f1,n1. 𝐂❪f1❫ ≘ n1 → ∀f2,n2. 𝐂❪f2❫ ≘ ∃∃f,n. f1 ⋓ f2 ≘ f & 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2. #f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by sor_isid_sn, ex4_2_intro/ #f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by fcla_push, fcla_next, ex4_2_intro, sor_isid_dx/ -#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n