From: Ferruccio Guidi Date: Fri, 26 Feb 2021 13:21:42 +0000 (+0100) Subject: propagating the arithmetics library, partial commit X-Git-Tag: make_still_working~159 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;p=helm.git propagating the arithmetics library, partial commit + counters (was: steps) ported and restyled + core notation: "pair" decentralized + some corrections and renaming --- diff --git a/.gitignore b/.gitignore index 9f322dc4c..69568a56b 100644 --- a/.gitignore +++ b/.gitignore @@ -80,6 +80,8 @@ helm/www/lambdadelta/xslt/xhtbl.xsl matita/matita/lib/lambda/.depend matita/matita/contribs/lambdadelta/.depend +matita/matita/contribs/lambdadelta/bin/recomm/srcs +matita/matita/contribs/lambdadelta/bin/recomm/log.txt matita/matita/contribs/lambdadelta/bin/nodes matita/matita/contribs/lambdadelta/bin/token matita/matita/contribs/lambdadelta/*/probe.txt diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index ad020929b..3bdc93e97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -19,9 +19,9 @@ include "ground/xoa/ex_5_2.ma". include "ground/xoa/ex_6_9.ma". include "ground/xoa/ex_7_10.ma". include "ground/xoa/or_5.ma". -include "ground/steps/rtc_shift.ma". -include "ground/steps/rtc_plus.ma". -include "ground/steps/rtc_max.ma". +include "ground/counters/rtc_shift.ma". +include "ground/counters/rtc_plus.ma". +include "ground/counters/rtc_max.ma". include "basic_2/notation/relations/predty_7.ma". include "static_2/syntax/lenv.ma". include "static_2/syntax/genv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index ac451b66c..d14504422 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -16,9 +16,9 @@ include "ground/xoa/ex_4_1.ma". include "ground/xoa/ex_4_3.ma". include "ground/xoa/ex_5_6.ma". include "ground/xoa/ex_6_7.ma". -include "ground/steps/rtc_max_shift.ma". -include "ground/steps/rtc_isrt_plus.ma". -include "ground/steps/rtc_isrt_max_shift.ma". +include "ground/counters/rtc_max_shift.ma". +include "ground/counters/rtc_isrt_plus.ma". +include "ground/counters/rtc_isrt_max_shift.ma". include "static_2/syntax/sh.ma". include "basic_2/notation/relations/pred_6.ma". include "basic_2/rt_transition/cpg.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma index 4f41f762d..de305d481 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma @@ -13,9 +13,9 @@ (**************************************************************************) include "ground/xoa/ex_4_3.ma". -include "ground/steps/rtc_ist_shift.ma". -include "ground/steps/rtc_ist_plus.ma". -include "ground/steps/rtc_ist_max.ma". +include "ground/counters/rtc_ist_shift.ma". +include "ground/counters/rtc_ist_plus.ma". +include "ground/counters/rtc_ist_max.ma". include "static_2/syntax/sh.ma". include "basic_2/notation/relations/pty_6.ma". include "basic_2/rt_transition/cpg.ma". diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile index fdee8f321..cb3deebf6 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/Makefile +++ b/matita/matita/contribs/lambdadelta/bin/recomm/Makefile @@ -8,7 +8,7 @@ clean:: @$(RM) recommGc*.ml* test: - @./recomm.native $(O) -C ../../ground/steps . | sort | uniq > log.txt + @./recomm.native -r $(O) -C srcs . | sort | uniq > log.txt MRCS = $(wildcard *.mrc) diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc index bd88c9d60..363f07fcf 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundCounters.mrc @@ -1,5 +1,4 @@ PcsAnd b "" true false -rtc_max, max -rtc_shift, shift -rtc_ism, test for constrained rt-transition counter -rtc_ist, test for t-transition counter +rtc_shift +rtc_max +rtc_plus diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc index f78834d6a..3352f4295 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundCounters.mrc @@ -1,3 +1,4 @@ PccFor d "" true false -T-BOUND RT-TRANSITION COUNTERS, RT-TRANSITION COUNTER -T-TRANSITION COUNTERS, T-TRANSITION COUNTER +RT-TRANSITION COUNTERS +T-BOUND RT-TRANSITION COUNTERS +T-TRANSITION COUNTERS diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc new file mode 100644 index 000000000..72b071350 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundCounters.mrc @@ -0,0 +1,4 @@ +PccFor r "" true false +ADDITION +MAXIMUM, MAXIMUN +SHIFT diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml index a2336ad9c..bac315438 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml @@ -10,6 +10,8 @@ module G = RecommGc let write = ref false +let force = ref false + let chdir path = Sys.chdir path @@ -23,7 +25,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 - if !write && lint <> orig then EO.write_srcs file lint + if !force || (!write && lint <> orig) then EO.write_srcs file lint end else begin Printf.eprintf "skipping: %S\n" file end @@ -32,13 +34,15 @@ let msg_C = " Set this working directory (default: .)" let msg_L = " Log lexer tokens (default: no)" let msg_c = " Set these output columns (default: 78)" let msg_d = " Log with dark colors (default: no)" +let msg_f = " Write all output files (default: no)" let msg_k = " Log key comments (default: no)" let msg_m = " Log mark comments (default: no)" let msg_n = " Log with no colors (default: yes)" 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_w = " Write the output files (default: no)" +let msg_w = " Write the changed output files (default: no)" let main = Arg.parse [ @@ -46,10 +50,12 @@ let main = "-L", Arg.Set EL.debug, msg_m; "-c", Arg.Int ((:=) EO.width), msg_c; "-d", Arg.Clear EC.bw, msg_d; + "-f", Arg.Set force, msg_f; "-k", Arg.Set EC.log_k, msg_k; "-m", Arg.Set EC.log_m, msg_m; "-n", Arg.Set EC.bw, msg_n; "-o", Arg.Set EC.log_o, msg_o; + "-r", Arg.Set EO.replace, msg_r; "-s", Arg.Set EC.log_s, msg_s; "-t", Arg.Set EC.log_t, msg_t; "-w", Arg.Set write, msg_w; diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml index 93d1d0316..e5629ccc8 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml @@ -76,7 +76,7 @@ let rec recomm srcs st = 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 as hd :: tl -> + | ET.Title ss :: tl -> if middle st then Printf.eprintf "middle: TITLE\n"; let b, ss1, ss2 = !c_line k_final false [] ss in let ss2 = @@ -85,8 +85,8 @@ let rec recomm srcs st = let ss = List.rev_append ss1 ss2 in let s = String.concat " " ss in if !log_t then log blue s; - recomm tl @@ add hd @@ st - | ET.Slice ss as hd :: tl -> + recomm tl @@ add (ET.Title ss) @@ st + | ET.Slice ss :: tl -> if middle st then Printf.eprintf "middle: Section\n"; let b, ss1, ss2 = !s_line k_final false [] ss in let ss2 = @@ -95,7 +95,7 @@ let rec recomm srcs st = let ss = List.rev_append ss1 ss2 in let s = String.capitalize_ascii (String.concat " " ss) in if !log_s then log sky s; - recomm tl @@ add hd @@ st + recomm tl @@ add (ET.Slice ss) @@ st | 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/recommGc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml index 6ffe876a7..12a3ec664 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml @@ -1,5 +1,6 @@ module G1 = RecommGcbGroundCounters module G2 = RecommGcdGroundCounters -module G3 = RecommGcsAttr -module G4 = RecommGcsMain -module G5 = RecommGcsWith +module G3 = RecommGcrGroundCounters +module G4 = RecommGcsAttr +module G5 = RecommGcsMain +module G6 = RecommGcsWith diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml index da14eabe1..53a98c92e 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundCounters.ml @@ -1,14 +1,9 @@ let step k ok outs ins = if ok then k ok outs ins else match ins with - | "rtc_ist" :: tl -> k true ("rtc_ist" :: outs) tl - | "test" :: "for" :: "t-transition" :: "counter" :: tl -> k true ("rtc_ist" :: outs) tl - | "rtc_ism" :: tl -> k true ("rtc_ism" :: outs) tl - | "test" :: "for" :: "constrained" :: "rt-transition" :: "counter" :: tl -> k true ("rtc_ism" :: outs) tl - | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl - | "shift" :: tl -> k true ("rtc_shift" :: outs) tl + | "rtc_plus" :: tl -> k true ("rtc_plus" :: outs) tl | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl - | "max" :: tl -> k true ("rtc_max" :: outs) tl + | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl | _ -> k ok outs ins let main = diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml index 5f86d75fe..796c21168 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundCounters.ml @@ -2,9 +2,8 @@ let step k ok outs ins = if ok then k ok outs ins else match ins with | "T-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl - | "T-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl - | "RT-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl + | "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: outs) tl | _ -> k ok outs ins let main = diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml new file mode 100644 index 000000000..d85161fa4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.ml @@ -0,0 +1,11 @@ +let step k ok outs ins = + if ok then k ok outs ins else + match ins with + | "SHIFT" :: tl -> k true ("SHIFT" :: outs) tl + | "MAXIMUM" :: tl -> k true ("MAXIMUM" :: outs) tl + | "MAXIMUN" :: tl -> k true ("MAXIMUM" :: outs) tl + | "ADDITION" :: tl -> k true ("ADDITION" :: outs) tl + | _ -> k ok outs ins + +let main = + RecommPccFor.register_r step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundCounters.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll index 0f66fc44b..21cca9c6c 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll @@ -10,6 +10,7 @@ let heads = [| "Advanved"; "Basic"; + "Constructions"; "Forward"; "Destructions"; "Eliminations"; diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml index 5189c7f77..fe8bebe94 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml @@ -2,6 +2,8 @@ module ET = RecommTypes let width = ref 78 +let replace = ref false + let complete s = let l = !width - String.length s - 6 in if l < 0 then begin @@ -19,7 +21,7 @@ let out_src och = function | ET.Mark s -> Printf.fprintf och "(* %s**)" s | ET.Key (s1, s2) -> - Printf.fprintf och "(* %s1%s2*)" s1 s2 + Printf.fprintf och "(* %s%s*)" s1 s2 | ET.Title ss -> let s = String.concat " " ss in Printf.fprintf och "(* %s %s*)" s (complete s) @@ -30,6 +32,14 @@ let out_src och = function Printf.fprintf och "%s%s%s" s1 s2 s3 let write_srcs file srcs = - let och = open_out (file ^ ".new") in + let target = + if !replace then begin + Sys.rename file (file ^ ".old"); + file + end else begin + file ^ ".new" + end + in + let och = open_out target in List.iter (out_src och) srcs; close_out och diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli index e1e856296..088b7fd9d 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.mli @@ -1,3 +1,5 @@ val width: int ref +val replace: bool ref + val write_srcs: string -> RecommTypes.srcs -> unit diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml index 5d08261c8..cdad8df55 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml @@ -8,7 +8,7 @@ let r_line = ref ES.id let k_for k ok outs ins = if ok then begin match ins with - | "for" :: tl -> !d_line k false ("for" :: outs) tl + | "FOR" :: tl -> !d_line k false ("FOR" :: outs) tl | _ -> k true outs ins end else begin k true outs ins diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma index c3ca75497..44c3539b9 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma @@ -60,11 +60,18 @@ lemma nmax_assoc: associative … nmax. #n1 #n2 #IH #n3 @(nat_ind_succ … n3) -n3 // qed. +lemma nmax_max_comm_23 (o:nat) (m) (n): (o ∨ m ∨ n) = (o ∨ n ∨ m). +#o #m #n >nmax_assoc >nmax_assoc nplus_assoc >nplus_assoc (nmax_zero_dx n) /2 width=1 by rtc_ism_max/ +qed. + +lemma rtc_ism_max_idem_sn (n) (c1) (c2): 𝐌❪n,c1❫ → 𝐌❪n,c2❫ → 𝐌❪n,c1∨c2❫. +#n #c1 #c2 #H1 #H2 >(nmax_idem n) /2 width=1 by rtc_ism_max/ +qed. + +(* Inversions with rtc_max **************************************************) + +lemma rtc_ism_inv_max (n) (c1) (c2): 𝐌❪n,c1 ∨ c2❫ → + ∃∃n1,n2. 𝐌❪n1,c1❫ & 𝐌❪n2,c2❫ & (n1 ∨ n2) = n. +#n #c1 #c2 * #ri #rs #H +elim (rtc_max_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4 +elim (eq_inv_nmax_zero … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/ +qed-. + +lemma rtc_isr_inv_max (c1) (c2): 𝐌❪𝟎,c1 ∨ c2❫ → ∧∧ 𝐌❪𝟎,c1❫ & 𝐌❪𝟎,c2❫. +#c1 #c2 #H +elim (rtc_ism_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H +elim (eq_inv_nmax_zero … H) -H #H1 #H2 destruct +/2 width=1 by conj/ +qed-. + +lemma rtc_ism_inv_max_zero_dx (n) (c1) (c2): 𝐌❪n,c1 ∨ c2❫ → 𝐌❪𝟎,c2❫ → 𝐌❪n,c1❫. +#n #c1 #c2 #H #H2 +elim (rtc_ism_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +lapply (rtc_ism_inj … Hn2 H2) -c2 #H destruct // +qed-. + +lemma rtc_ism_inv_max_eq_t (n) (c1) (c2): 𝐌❪n,c1 ∨ c2❫ → rtc_eq_t c1 c2 → + ∧∧ 𝐌❪n,c1❫ & 𝐌❪n,c2❫. +#n #c1 #c2 #H #Hc12 +elim (rtc_ism_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct +lapply (rtc_ism_eq_t_trans … Hc1 … Hc12) -Hc12 #H +<(rtc_ism_inj … H … Hc2) -Hc2 +(nplus_zero_sn n) /2 width=1 by rtc_ism_plus/ +qed. + +lemma rtc_ism_plus_zero_dx (n) (c1) (c2): 𝐌❪n,c1❫ → 𝐌❪𝟎,c2❫ → 𝐌❪n,c1+c2❫. +/2 width=1 by rtc_ism_plus/ qed. + +lemma rtc_ism_succ (n) (c): 𝐌❪n,c❫ → 𝐌❪↑n,c+𝟘𝟙❫. +#n #c #H >nplus_one_dx +/2 width=1 by rtc_ism_plus/ +qed. + +(* Inversions with rtc_plus *************************************************) + +lemma rtc_ism_inv_plus (n) (c1) (c2): 𝐌❪n,c1 + c2❫ → + ∃∃n1,n2. 𝐌❪n1,c1❫ & 𝐌❪n2,c2❫ & n1 + n2 = n. +#n #c1 #c2 * #ri #rs #H +elim (rtc_plus_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4 +elim (eq_inv_nplus_zero … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/ +qed-. + +lemma rtc_ism_inv_plus_zero_dx (n) (c1) (c2): 𝐌❪n,c1 + c2❫ → 𝐌❪𝟎,c2❫ → 𝐌❪n,c1❫. +#n #c1 #c2 #H #H2 +elim (rtc_ism_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +lapply (rtc_ism_inj … Hn2 H2) -c2 #H destruct // +qed-. + +lemma rtc_ism_inv_plus_unit_dx (n) (c1) (c2): 𝐌❪n,c1 + c2❫ → 𝐌❪𝟏,c2❫ → + ∃∃m. 𝐌❪m,c1❫ & n = ↑m. +#n #c1 #c2 #H #H2 +elim (rtc_ism_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +lapply (rtc_ism_inj … Hn2 H2) -c2 #H destruct +/2 width=3 by ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_shift.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_shift.ma new file mode 100644 index 000000000..3ecc6d017 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_shift.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/counters/rtc_shift.ma". +include "ground/counters/rtc_ism.ma". + +(* T-BOUND RT-TRANSITION COUNTERS *******************************************) + +(* Constructions with rtc_shift *********************************************) + +lemma rtc_isr_shift (c): 𝐌❪𝟎,c❫ → 𝐌❪𝟎,↕*c❫. +#c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/ +qed. + +(* Inversions with rtc_shift ************************************************) + +lemma rtc_ism_inv_shift (n) (c): 𝐌❪n,↕*c❫ → ∧∧ 𝐌❪𝟎,c❫ & 𝟎 = n. +#n #c * #ri #rs #H +elim (rtc_shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3 +elim (eq_inv_nmax_zero … H1) -H1 /3 width=3 by ex1_2_intro, conj/ +qed-. + +lemma rtc_isr_inv_shift (c): 𝐌❪𝟎,↕*c❫ → 𝐌❪𝟎,c❫. +#c #H elim (rtc_ism_inv_shift … H) -H // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma new file mode 100644 index 000000000..38c430ae8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relations/ist_2.ma". +include "ground/counters/rtc.ma". + +(* T-TRANSITION COUNTERS ****************************************************) + +definition rtc_ist: relation2 nat rtc ≝ + λts,c. 〈𝟎,𝟎,𝟎,ts〉 = c. + +interpretation + "t-transition counters (rtc)" + 'IsT ts c = (rtc_ist ts c). + +(* Basic constructions ******************************************************) + +lemma rtc_ist_zz: 𝐓❪𝟎,𝟘𝟘❫. +// qed. + +lemma rtc_ist_zu: 𝐓❪𝟏,𝟘𝟙❫. +// qed. + +(* Basic inversions *********************************************************) + +lemma rtc_ist_inv_zz (n): 𝐓❪n,𝟘𝟘❫ → 𝟎 = n. +#n #H destruct // +qed-. + +lemma rtc_ist_inv_zu (n): 𝐓❪n,𝟘𝟙❫ → ninj (𝟏) = n. +#n #H destruct // +qed-. + +lemma rtc_ist_inv_uz (n): 𝐓❪n,𝟙𝟘❫ → ⊥. +#h #H destruct +qed-. + +(* Main inversions **********************************************************) + +theorem rtc_ist_inj (n1) (n2) (c): 𝐓❪n1,c❫ → 𝐓❪n2,c❫ → n1 = n2. +#n1 #n2 #c #H1 #H2 destruct // +qed-. + +theorem rtc_ist_mono (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪n,c2❫ → c1 = c2. +#n #c1 #c2 #H1 #H2 destruct // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_max.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_max.ma new file mode 100644 index 000000000..3ad43260d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_max.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/xoa/ex_3_2.ma". +include "ground/counters/rtc_max.ma". +include "ground/counters/rtc_ist.ma". + +(* T-BOUND RT-TRANSITION COUNTERS *******************************************) + +(* Constructions with rtc_max ***********************************************) + +lemma rtc_ist_max (n1) (n2) (c1) (c2): 𝐓❪n1,c1❫ → 𝐓❪n2,c2❫ → 𝐓❪n1∨n2,c1∨c2❫. +#n1 #n2 #c1 #c2 #H1 #H2 destruct // +qed. + +lemma rtc_ist_max_zero_sn (n) (c1) (c2): 𝐓❪𝟎,c1❫ → 𝐓❪n,c2❫ → 𝐓❪n,c1∨c2❫. +/2 width=1 by rtc_ist_max/ qed. + +lemma rtc_ist_max_zero_dx (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪𝟎,c2❫ → 𝐓❪n,c1∨c2❫. +// qed. + +lemma rtc_ist_max_idem_sn (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪n,c2❫ → 𝐓❪n,c1∨c2❫. +#n #c1 #c2 #H1 #H2 >(nmax_idem n) /2 width=1 by rtc_ist_max/ +qed. + +(* Inversions with rtc_max **************************************************) + +lemma rtc_ist_inv_max (n) (c1) (c2): 𝐓❪n,c1 ∨ c2❫ → + ∃∃n1,n2. 𝐓❪n1,c1❫ & 𝐓❪n2,c2❫ & (n1 ∨ n2) = n. +#n #c1 #c2 #H +elim (rtc_max_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct +elim (eq_inv_nmax_zero … H1) -H1 #H11 #H12 destruct +elim (eq_inv_nmax_zero … H2) -H2 #H21 #H22 destruct +elim (eq_inv_nmax_zero … H3) -H3 #H31 #H32 destruct +/2 width=5 by ex3_2_intro/ +qed-. + +lemma rtc_ist_inv_zero_max (c1) (c2): 𝐓❪𝟎,c1 ∨ c2❫ → ∧∧ 𝐓❪𝟎,c1❫ & 𝐓❪𝟎,c2❫. +#c1 #c2 #H +elim (rtc_ist_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H +elim (eq_inv_nmax_zero … H) -H #H1 #H2 destruct +/2 width=1 by conj/ +qed-. + +lemma rtc_ist_inv_max_zero_dx (n) (c1) (c2): 𝐓❪n,c1 ∨ c2❫ → 𝐓❪𝟎,c2❫ → 𝐓❪n,c1❫. +#n #c1 #c2 #H #H2 +elim (rtc_ist_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma new file mode 100644 index 000000000..08bb3b772 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/xoa/ex_3_2.ma". +include "ground/counters/rtc_plus.ma". +include "ground/counters/rtc_ist.ma". + +(* T-BOUND RT-TRANSITION COUNTERS *******************************************) + +(* Constructions with rtc_plus **********************************************) + +lemma rtc_ist_plus (n1) (n2) (c1) (c2): 𝐓❪n1,c1❫ → 𝐓❪n2,c2❫ → 𝐓❪n1+n2,c1+c2❫. +#n1 #n2 #c1 #c2 #H1 #H2 destruct // +qed. + +lemma rtc_ist_plus_zero_sn (n) (c1) (c2): 𝐓❪𝟎,c1❫ → 𝐓❪n,c2❫ → 𝐓❪n,c1+c2❫. +#n #c1 #c2 #H1 #H2 >(nplus_zero_sn n) +/2 width=1 by rtc_ist_plus/ +qed. + +lemma rtc_ist_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪𝟎,c2❫ → 𝐓❪n,c1+c2❫. +/2 width=1 by rtc_ist_plus/ qed. + +lemma rtc_ist_succ (n) (c): 𝐓❪n,c❫ → 𝐓❪↑n,c+𝟘𝟙❫. +#n #c #H >nplus_one_dx +/2 width=1 by rtc_ist_plus/ +qed. + +(* Inversions with rtc_plus *************************************************) + +lemma rtc_ist_inv_plus (n) (c1) (c2): 𝐓❪n,c1 + c2❫ → + ∃∃n1,n2. 𝐓❪n1,c1❫ & 𝐓❪n2,c2❫ & n1 + n2 = n. +#n #c1 #c2 #H +elim (rtc_plus_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct +elim (eq_inv_nplus_zero … H1) -H1 #H11 #H12 destruct +elim (eq_inv_nplus_zero … H2) -H2 #H21 #H22 destruct +elim (eq_inv_nplus_zero … H3) -H3 #H31 #H32 destruct +/3 width=5 by ex3_2_intro/ +qed-. + +lemma rtc_ist_inv_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1 + c2❫ → 𝐓❪𝟎,c2❫ → 𝐓❪n,c1❫. +#n #c1 #c2 #H #H2 +elim (rtc_ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct // +qed-. + +lemma rtc_ist_inv_plus_one_dx: + ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → 𝐓❪𝟏,c2❫ → + ∃∃m. 𝐓❪m,c1❫ & n = ↑m. +#n #c1 #c2 #H #H2 destruct +elim (rtc_ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma rtc_ist_inv_plus_zu_dx (n) (c): 𝐓❪n,c+𝟙𝟘❫ → ⊥. +#n #c #H +elim (rtc_ist_inv_plus … H) -H #n1 #n2 #_ #H #_ +/2 width=2 by rtc_ist_inv_uz/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_shift.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_shift.ma new file mode 100644 index 000000000..fbb72abac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_shift.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/counters/rtc_shift.ma". +include "ground/counters/rtc_ist.ma". + +(* T-BOUND RT-TRANSITION COUNTERS *******************************************) + +(* Constructions with rtc_shift *********************************************) + +lemma rtc_ist_zero_shift (c): 𝐓❪𝟎,c❫ → 𝐓❪𝟎,↕*c❫. +#c #H destruct // +qed. + +(* Inversions with rtc_shift ************************************************) + +lemma rtc_ist_inv_shift (n) (c): 𝐓❪n,↕*c❫ → ∧∧ 𝐓❪𝟎,c❫ & 𝟎 = n. +#n #c #H +elim (rtc_shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #H1 #_ #H2 #H3 #H4 destruct +elim (eq_inv_nmax_zero … H1) -H1 #H11 #H12 destruct +elim (eq_inv_nmax_zero … H2) -H2 #H21 #H22 destruct +/2 width=1 by conj/ +qed-. + +lemma rtc_ist_inv_zero_shift (c): 𝐓❪𝟎,↕*c❫ → 𝐓❪𝟎,c❫. +#c #H elim (rtc_ist_inv_shift … H) -H // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma new file mode 100644 index 000000000..10fbce4ef --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/xoa/ex_6_8.ma". +include "ground/arith/nat_max.ma". +include "ground/counters/rtc.ma". + +(* MAXIMUM FOR RT-TRANSITION COUNTERS ***************************************) + +definition rtc_max (c1:rtc) (c2:rtc): rtc ≝ +match c1 with +[ mk_rtc ri1 rs1 ti1 ts1 ⇒ + match c2 with + [ mk_rtc ri2 rs2 ti2 ts2 ⇒ 〈ri1∨ri2,rs1∨rs2,ti1∨ti2,ts1∨ts2〉 + ] +]. + +interpretation + "maximum (rtc)" + 'or c1 c2 = (rtc_max c1 c2). + +(* Basic constructions ******************************************************) + +lemma rtc_max_rew (ri1) (ri2) (rs1) (rs2) (ti1) (ti2) (ts1) (ts2): + 〈ri1∨ri2,rs1∨rs2,ti1∨ti2,ts1∨ts2〉 = + (〈ri1,rs1,ti1,ts1〉 ∨ 〈ri2,rs2,ti2,ts2〉). +// qed. + +lemma rtc_max_zz_dx (c): c = (c ∨ 𝟘𝟘). +* #ri #rs #ti #ts (max_O2 n) /2 width=1 by isrt_max/ -qed. - -lemma isrt_max_idem1: ∀n,c1,c2. 𝐑𝐓❪n,c1❫ → 𝐑𝐓❪n,c2❫ → 𝐑𝐓❪n,c1∨c2❫. -#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by isrt_max/ -qed. - -(* Inversion properties with test for constrained rt-transition counter *****) - -lemma isrt_inv_max: ∀n,c1,c2. 𝐑𝐓❪n,c1 ∨ c2❫ → - ∃∃n1,n2. 𝐑𝐓❪n1,c1❫ & 𝐑𝐓❪n2,c2❫ & (n1 ∨ n2) = n. -#n #c1 #c2 * #ri #rs #H -elim (max_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4 -elim (max_inv_O3 … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/ -qed-. - -lemma isrt_O_inv_max: ∀c1,c2. 𝐑𝐓❪0,c1 ∨ c2❫ → ∧∧ 𝐑𝐓❪0,c1❫ & 𝐑𝐓❪0,c2❫. -#c1 #c2 #H -elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H -elim (max_inv_O3 … H) -H #H1 #H2 destruct -/2 width=1 by conj/ -qed-. - -lemma isrt_inv_max_O_dx: ∀n,c1,c2. 𝐑𝐓❪n,c1 ∨ c2❫ → 𝐑𝐓❪0,c2❫ → 𝐑𝐓❪n,c1❫. -#n #c1 #c2 #H #H2 -elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct -lapply (isrt_inj … Hn2 H2) -c2 #H destruct // -qed-. - -lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓❪n,c1 ∨ c2❫ → rtc_eq_t c1 c2 → - ∧∧ 𝐑𝐓❪n,c1❫ & 𝐑𝐓❪n,c2❫. -#n #c1 #c2 #H #Hc12 -elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct -lapply (isrt_eq_t_trans … Hc1 … Hc12) -Hc12 #H -<(isrt_inj … H … Hc2) -Hc2 -(plus_n_O n) /2 width=1 by isrt_plus/ -qed. - -lemma isrt_succ: ∀n,c. 𝐑𝐓❪n,c❫ → 𝐑𝐓❪↑n,c+𝟘𝟙❫. -/2 width=1 by isrt_plus/ qed. - -(* Inversion properties with test for constrained rt-transition counter *****) - -lemma isrt_inv_plus: ∀n,c1,c2. 𝐑𝐓❪n,c1 + c2❫ → - ∃∃n1,n2. 𝐑𝐓❪n1,c1❫ & 𝐑𝐓❪n2,c2❫ & n1 + n2 = n. -#n #c1 #c2 * #ri #rs #H -elim (plus_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4 -elim (plus_inv_O3 … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/ -qed-. - -lemma isrt_inv_plus_O_dx: ∀n,c1,c2. 𝐑𝐓❪n,c1 + c2❫ → 𝐑𝐓❪0,c2❫ → 𝐑𝐓❪n,c1❫. -#n #c1 #c2 #H #H2 -elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct -lapply (isrt_inj … Hn2 H2) -c2 #H destruct // -qed-. - -lemma isrt_inv_plus_SO_dx: ∀n,c1,c2. 𝐑𝐓❪n,c1 + c2❫ → 𝐑𝐓❪1,c2❫ → - ∃∃m. 𝐑𝐓❪m,c1❫ & n = ↑m. -#n #c1 #c2 #H #H2 -elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct -lapply (isrt_inj … Hn2 H2) -c2 #H destruct -/2 width=3 by ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma deleted file mode 100644 index 0e0b73f4a..000000000 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_shift.ma +++ /dev/null @@ -1,36 +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/steps/rtc_shift.ma". -include "ground/steps/rtc_isrt.ma". - -(* RT-TRANSITION COUNTER ****************************************************) - -(* Properties with test for constrained rt-transition counter ***************) - -lemma isr_shift: ∀c. 𝐑𝐓❪0,c❫ → 𝐑𝐓❪0,↕*c❫. -#c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/ -qed. - -(* Inversion properties with test for constrained rt-transition counter *****) - -lemma isrt_inv_shift: ∀n,c. 𝐑𝐓❪n,↕*c❫ → 𝐑𝐓❪0,c❫ ∧ 0 = n. -#n #c * #ri #rs #H -elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3 -elim (max_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/ -qed-. - -lemma isr_inv_shift: ∀c. 𝐑𝐓❪0,↕*c❫ → 𝐑𝐓❪0,c❫. -#c #H elim (isrt_inv_shift … H) -H // -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist.ma deleted file mode 100644 index c0bafa7b4..000000000 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist.ma +++ /dev/null @@ -1,56 +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/relations/istype_2.ma". -include "ground/steps/rtc.ma". - -(* T-TRANSITION COUNTER *****************************************************) - -definition ist: relation2 nat rtc ≝ - λts,c. 〈0,0,0,ts〉 = c. - -interpretation "test for t-transition counter (rtc)" - 'IsType ts c = (ist ts c). - -(* Basic properties *********************************************************) - -lemma ist_00: 𝐓❪0,𝟘𝟘❫. -// qed. - -lemma ist_01: 𝐓❪1,𝟘𝟙❫. -// qed. - -(* Basic inversion properties ***********************************************) - -lemma ist_inv_00: ∀n. 𝐓❪n,𝟘𝟘❫ → 0 = n. -#n #H destruct // -qed-. - -lemma ist_inv_01: ∀n. 𝐓❪n,𝟘𝟙❫ → 1 = n. -#n #H destruct // -qed-. - -lemma ist_inv_10: ∀n. 𝐓❪n,𝟙𝟘❫ → ⊥. -#h #H destruct -qed-. - -(* Main inversion properties ************************************************) - -theorem ist_inj: ∀n1,n2,c. 𝐓❪n1,c❫ → 𝐓❪n2,c❫ → n1 = n2. -#n1 #n2 #c #H1 #H2 destruct // -qed-. - -theorem ist_mono: ∀n,c1,c2. 𝐓❪n,c1❫ → 𝐓❪n,c2❫ → c1 = c2. -#n #c1 #c2 #H1 #H2 destruct // -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_max.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_max.ma deleted file mode 100644 index 72be5b990..000000000 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_max.ma +++ /dev/null @@ -1,61 +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/xoa/ex_3_2.ma". -include "ground/steps/rtc_max.ma". -include "ground/steps/rtc_ist.ma". - -(* RT-TRANSITION COUNTER ****************************************************) - -(* Properties with test for t-transition counter ****************************) - -lemma ist_max: ∀n1,n2,c1,c2. 𝐓❪n1,c1❫ → 𝐓❪n2,c2❫ → 𝐓❪n1∨n2,c1∨c2❫. -#n1 #n2 #c1 #c2 #H1 #H2 destruct // -qed. - -lemma ist_max_O1: ∀n,c1,c2. 𝐓❪0,c1❫ → 𝐓❪n,c2❫ → 𝐓❪n,c1∨c2❫. -/2 width=1 by ist_max/ qed. - -lemma ist_max_O2: ∀n,c1,c2. 𝐓❪n,c1❫ → 𝐓❪0,c2❫ → 𝐓❪n,c1∨c2❫. -#n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by ist_max/ -qed. - -lemma ist_max_idem1: ∀n,c1,c2. 𝐓❪n,c1❫ → 𝐓❪n,c2❫ → 𝐓❪n,c1∨c2❫. -#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by ist_max/ -qed. - -(* Inversion properties with test for t-transition counter ******************) - -lemma ist_inv_max: - ∀n,c1,c2. 𝐓❪n,c1 ∨ c2❫ → - ∃∃n1,n2. 𝐓❪n1,c1❫ & 𝐓❪n2,c2❫ & (n1 ∨ n2) = n. -#n #c1 #c2 #H -elim (max_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct -elim (max_inv_O3 … H1) -H1 #H11 #H12 destruct -elim (max_inv_O3 … H2) -H2 #H21 #H22 destruct -elim (max_inv_O3 … H3) -H3 #H31 #H32 destruct -/2 width=5 by ex3_2_intro/ -qed-. - -lemma ist_O_inv_max: ∀c1,c2. 𝐓❪0,c1 ∨ c2❫ → ∧∧ 𝐓❪0,c1❫ & 𝐓❪0,c2❫. -#c1 #c2 #H -elim (ist_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H -elim (max_inv_O3 … H) -H #H1 #H2 destruct -/2 width=1 by conj/ -qed-. - -lemma ist_inv_max_O_dx: ∀n,c1,c2. 𝐓❪n,c1 ∨ c2❫ → 𝐓❪0,c2❫ → 𝐓❪n,c1❫. -#n #c1 #c2 #H #H2 -elim (ist_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct // -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_plus.ma deleted file mode 100644 index 44f12f004..000000000 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_plus.ma +++ /dev/null @@ -1,67 +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/xoa/ex_3_2.ma". -include "ground/steps/rtc_plus.ma". -include "ground/steps/rtc_ist.ma". - -(* RT-TRANSITION COUNTER ****************************************************) - -(* Properties with test for t-transition counter ****************************) - -lemma ist_plus: ∀n1,n2,c1,c2. 𝐓❪n1,c1❫ → 𝐓❪n2,c2❫ → 𝐓❪n1+n2,c1+c2❫. -#n1 #n2 #c1 #c2 #H1 #H2 destruct // -qed. - -lemma ist_plus_O1: ∀n,c1,c2. 𝐓❪0,c1❫ → 𝐓❪n,c2❫ → 𝐓❪n,c1+c2❫. -/2 width=1 by ist_plus/ qed. - -lemma ist_plus_O2: ∀n,c1,c2. 𝐓❪n,c1❫ → 𝐓❪0,c2❫ → 𝐓❪n,c1+c2❫. -#n #c1 #c2 #H1 #H2 >(plus_n_O n) /2 width=1 by ist_plus/ -qed. - -lemma ist_succ: ∀n,c. 𝐓❪n,c❫ → 𝐓❪↑n,c+𝟘𝟙❫. -/2 width=1 by ist_plus/ qed. - -(* Inversion properties with test for constrained rt-transition counter *****) - -lemma ist_inv_plus: - ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → - ∃∃n1,n2. 𝐓❪n1,c1❫ & 𝐓❪n2,c2❫ & n1 + n2 = n. -#n #c1 #c2 #H -elim (plus_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct -elim (plus_inv_O3 … H1) -H1 #H11 #H12 destruct -elim (plus_inv_O3 … H2) -H2 #H21 #H22 destruct -elim (plus_inv_O3 … H3) -H3 #H31 #H32 destruct -/3 width=5 by ex3_2_intro/ -qed-. - -lemma ist_inv_plus_O_dx: ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → 𝐓❪0,c2❫ → 𝐓❪n,c1❫. -#n #c1 #c2 #H #H2 -elim (ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct // -qed-. - -lemma ist_inv_plus_SO_dx: - ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → 𝐓❪1,c2❫ → - ∃∃m. 𝐓❪m,c1❫ & n = ↑m. -#n #c1 #c2 #H #H2 destruct -elim (ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct -/2 width=3 by ex2_intro/ -qed-. - -lemma ist_inv_plus_10_dx: ∀n,c. 𝐓❪n,c+𝟙𝟘❫ → ⊥. -#n #c #H -elim (ist_inv_plus … H) -H #n1 #n2 #_ #H #_ -/2 width=2 by ist_inv_10/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_shift.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_shift.ma deleted file mode 100644 index fcaa4d8ba..000000000 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_ist_shift.ma +++ /dev/null @@ -1,38 +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/steps/rtc_shift.ma". -include "ground/steps/rtc_ist.ma". - -(* RT-TRANSITION COUNTER ****************************************************) - -(* Properties with test for t-transition counter ****************************) - -lemma ist_zero_shift: ∀c. 𝐓❪0,c❫ → 𝐓❪0,↕*c❫. -#c #H destruct // -qed. - -(* Inversion properties with test for t-transition counter ******************) - -lemma ist_inv_shift: ∀n,c. 𝐓❪n,↕*c❫ → ∧∧ 𝐓❪0,c❫ & 0 = n. -#n #c #H -elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #H1 #_ #H2 #H3 #H4 destruct -elim (max_inv_O3 … H1) -H1 #H11 #H12 destruct -elim (max_inv_O3 … H2) -H2 #H21 #H22 destruct -/2 width=1 by conj/ -qed-. - -lemma ist_inv_zero_shift: ∀c. 𝐓❪0,↕*c❫ → 𝐓❪0,c❫. -#c #H elim (ist_inv_shift … H) -H // -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_max.ma deleted file mode 100644 index 9e7665524..000000000 --- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_max.ma +++ /dev/null @@ -1,59 +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/xoa/ex_6_8.ma". -include "ground/steps/rtc.ma". - -(* RT-TRANSITION COUNTER ****************************************************) - -definition max (c1:rtc) (c2:rtc): rtc ≝ match c1 with [ - mk_rtc ri1 rs1 ti1 ts1 ⇒ match c2 with [ - mk_rtc ri2 rs2 ti2 ts2 ⇒ 〈ri1∨ri2,rs1∨rs2,ti1∨ti2,ts1∨ts2〉 - ] -]. - -interpretation "maximum (rtc)" - 'or c1 c2 = (max c1 c2). - -(* Basic properties *********************************************************) - -lemma max_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2. - 〈ri1∨ri2,rs1∨rs2,ti1∨ti2,ts1∨ts2〉 = - (〈ri1,rs1,ti1,ts1〉 ∨ 〈ri2,rs2,ti2,ts2〉). -// qed. - -lemma max_O_dx: ∀c. c = (c ∨ 𝟘𝟘). -* #ri #rs #ti #ts