From: matitaweb Date: Sat, 27 Apr 2013 15:56:10 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1173 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=deff2f761d3e025908b6006c6fe3c07f1aa28d64;p=helm.git commit by user andrea --- diff --git a/weblib/Reverse_complexity/reverse.ma b/weblib/Reverse_complexity/reverse.ma new file mode 100644 index 000000000..73814b17a --- /dev/null +++ b/weblib/Reverse_complexity/reverse.ma @@ -0,0 +1,359 @@ + +include "arithmetics/nat.ma". +include "basics/types.ma". +include "arithmetics/min_max.ma". +include "arithmetics/bigO.ma". + +(*********************************** pairing **********************************) + +axiom pair: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +axiom fst : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +axiom snd : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +axiom fst_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a. +axiom snd_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/snd.dec"snd/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. + +interpretation "abstract pair" 'pair f g = (pair f g). + +(************************ basic complexity notions ****************************) + +(* u is the deterministic configuration relation of the universal machine (one + step) *) + +axiom u: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + +let rec U c n on n ≝ + match n with + [ O ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? + | S m ⇒ match a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a c with + [ None ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c (* halting case *) + | Some c1 ⇒ U c1 m + ] + ]. + +lemma halt_U: ∀i,n,y. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i. +#i #n #y #H cases n + [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //] +qed. + +lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? . +#n elim n + [#i #y normalize #H destruct (H) + |#m #Hind #i #y normalize + cut (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="exists" href="cic:/fakeuri.def(1)"∃/ac. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c) + [cases (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | #c %2 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a/span/span/ ]] + *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ] + ] +qed. + +lemma monotonici_U: ∀y,n,m,i. + a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y. +#y #n #m elim m + [#i normalize #H destruct + |#p #Hind #i <a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a normalize + cut (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="exists" href="cic:/fakeuri.def(1)"∃/ac. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c) + [cases (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | #c %2 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a/span/span/ ]] + *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //] + ] +qed. + +lemma monotonic_U: ∀i,n,m,y.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → + a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y. +#i #n #m #y #lenm #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a m n) // @a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"monotonici_U/a // +qed. + +(* axiom U: nat → nat → option nat. *) +(* axiom monotonic_U: ∀i,n,m,y.n ≤m → + U i n = Some ? y → U i m = Some ? y. *) + +lemma unique_U: ∀i,n,m,yn,ym. + a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? yn → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? ym → yn a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ym. +#i #n #m #yn #ym #Hn #Hm cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m) + [#lenm lapply (a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … lenm Hn) >Hm #HS destruct (HS) // + |#ltmn lapply (a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … n … Hm) [@a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"lt_to_le/a @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //] + >Hn #HS destruct (HS) // + ] +qed. + +definition code_for ≝ λf,i.∀x. + a title="exists" href="cic:/fakeuri.def(1)"∃/an.∀m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x. + +definition terminate ≝ λc,r. a title="exists" href="cic:/fakeuri.def(1)"∃/ay. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a c r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y. + +interpretation "termination" 'fintersects c r = (terminate c r). + +definition lang ≝ λi,x.a title="exists" href="cic:/fakeuri.def(1)"∃/ar,ya title="exists" href="cic:/fakeuri.def(1)"./a a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. + +lemma lang_cf :∀f,i,x. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i → + a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i x a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="exists" href="cic:/fakeuri.def(1)"∃/ay.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. +#f #i #x normalize #H % + [* #n * #y * #H1 #posy %{y} % // + cases (H x) -H #m #H <(H (a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m)) [2:@(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … n) //] + @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … H1) @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … m) // + |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm // + ] +qed. + +(******************************* complexity classes ***************************) + +axiom size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. +axiom of_size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. + +interpretation "size" 'card n = (size n). + +axiom size_of_size: ∀n. |a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n. +axiom of_size_max: ∀i,n. |ia title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n. + +axiom size_fst : ∀n. |a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |na title="size" href="cic:/fakeuri.def(1)"|/a. + +axiom a : Max0. + +definition size_f ≝ λf,n.Max_{ifont class="Apple-style-span" color="#FF0000" < /fontS (of_size n) | eqb (|i|) n }|(f i)|. + +lemma size_f_def: ∀f,n. size_f f n = + Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|. +// qed. + +lemma size_f_size : ∀f,n. size_f (f ∘ size) n = |(f n)|. +#f #n @le_to_le_to_eq + [@Max_le #a #lta #Ha normalize >(eqb_true_to_eq … Ha) // + |<(size_of_size n) in ⊢ (?%?); >size_f_def + @(le_Max (λi.|f (|i|)|) ? (S (of_size n)) (of_size n) ??) + [@le_S_S // | @eq_to_eqb_true //] + ] +qed. + +lemma size_f_id : ∀n. size_f (λx.x) n = n. +#n @le_to_le_to_eq + [@Max_le #a #lta #Ha >(eqb_true_to_eq … Ha) // + |<(size_of_size n) in ⊢ (?%?); >size_f_def + @(le_Max (λi.|i|) ? (S (of_size n)) (of_size n) ??) + [@le_S_S // | @eq_to_eqb_true //] + ] +qed. + +lemma size_f_fst : ∀n. size_f fst n ≤ n. +#n @Max_le #a #lta #Ha <(eqb_true_to_eq … Ha) // +qed. + +(* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*) + +(* C s i means that the complexity of i is O(s) *) + +definition C ≝ λs,i.∃c.∃a.∀x.a ≤ |x| → ∃y. + U 〈i,x〉 (c*(s(|x|))) = Some ? y. + +definition CF ≝ λs,f.∃i.code_for f i ∧ C s i. + +lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g. +#f #g #s #Hext * #i * #Hcode #HC %{i} % + [#x cases (Hcode x) #a #H %{a} associative_times @le_times // @H @(le_maxl … Hmax) +qed. + +(************************** The diagonal language *****************************) + +(* the diagonal language used for the hierarchy theorem *) + +definition diag ≝ λs,i. + U 〈fst i,i〉 (s (|i|)) = Some ? 0. + +lemma equiv_diag: ∀s,i. + diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i. +#s #i % + [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y * + #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/ + |* * #y cases y // + #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % // + ] +qed. + +(* Let us define the characteristic function diag_cf for diag, and prove +it correctness *) + +definition diag_cf ≝ λs,i. + match U 〈fst i,i〉 (s (|i|)) with + [ None ⇒ None ? + | Some y ⇒ if (eqb y 0) then (Some ? 1) else (Some ? 0)]. + +lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y. +#s #x % + [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H // + |* #y * whd in ⊢ (??%?→?→%); + cases (U 〈fst x,x〉 (s (|x|))) normalize + [#H destruct + |#x cases (true_or_false (eqb x 0)) #Hx >Hx + [>(eqb_true_to_eq … Hx) // + |normalize #H destruct #H @False_ind @(absurd ? H) @lt_to_not_le // + ] + ] + ] +qed. + +lemma diag_spec: ∀s,i. code_for (diag_cf s) i → ∀x. lang i x ↔ diag s x. +#s #i #Hcode #x @(iff_trans … (lang_cf … Hcode)) @iff_sym @diag_cf_OK +qed. + +(******************************************************************************) + +lemma absurd1: ∀P. iff P (¬ P) →False. +#P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //] +#H3 @(absurd ?? H3) @H2 @H3 +qed. + +(* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *) +axiom pad : ∀a,n. |a| < n → ∃b. |〈a,b〉| = n. + +lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i → + ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|). +#s1 #s2 #H #i * #c * #x0 #H1 +cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?) + [#b #H4 %{b} + cases (H1 〈i,b〉 ?) + [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le // + |>H4 @(le_maxr … H2) + ] + |@(le_maxl … H2) + ] +qed. + +lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf s1). +#s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i +cases (not_included_ex … H1 ? Hs2_i) #b #H2 +lapply (diag_spec … Hcode_i) #H3 +@(absurd1 (lang i 〈i,b〉)) +@(iff_trans … (H3 〈i,b〉)) +@(iff_trans … (equiv_diag …)) >fst_pair +%[* #_ // |#H6 % // ] +qed. + +(******************************************************************************) +(* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *) + +definition to_Some ≝ λf.λx:nat. Some nat (f x). + +definition deopt ≝ λn. match n with + [ None ⇒ 1 + | Some n ⇒ n]. + +definition opt_comp ≝ λf,g:nat → option nat. λx. + match g x with + [ None ⇒ None ? + | Some y ⇒ f y ]. + +(* axiom CFU: ∀h,g,s. CF s (to_Some h) → CF s (to_Some (of_size ∘ g)) → + CF (Slow s) (λx.U (h x) (g x)). *) + +axiom sU2: nat → nat → nat. +axiom sU: nat → nat → nat → nat. + +(* axiom CFU: CF sU (λx.U (fst x) (snd x)). *) + +axiom CFU: ∀h,g,f,s1,s2,s3. + CF s1 (to_Some h) → CF s2 (to_Some g) → CF s3 (to_Some f) → + CF (λx. s1 x + s2 x + s3 x + sU (size_f h x) (size_f g x) (size_f f x)) + (λx.U 〈h x,g x〉 (|f x|)). + +axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 → + sU a1 b1 c1 ≤ sU a2 b2 c2. + +definition sU_space ≝ λi,x,r.i+x+r. +definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r). + +(* +axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → + CF (λx.s2 x + s1 (size (deopt (g x)))) (opt_comp f g). + +(* axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → + CF (s1 ∘ (λx. size (deopt (g x)))) (opt_comp f g). *) + +axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g → + CF (s1 ∘ s2) (opt_comp f g). *) + +definition IF ≝ λb,f,g:nat →option nat. λx. + match b x with + [None ⇒ None ? + |Some n ⇒ if (eqb n 0) then f x else g x]. + +axiom IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g → + CF (λn. sb n + sf n + sg n) (IF b f g). + +lemma diag_cf_def : ∀s.∀i. + diag_cf s i = + IF (λi.U (pair (fst i) i) (|of_size (s (|i|))|)) (λi.Some ? 1) (λi.Some ? 0) i. +#s #i normalize >size_of_size // qed. + +(* and now ... *) +axiom CF_pair: ∀f,g,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (g x)) → + CF s (λx.Some ? (pair (f x) (g x))). + +axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))). + +definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c). + + +(* +axiom le_snd: ∀n. |snd n| ≤ |n|. +axiom daemon: ∀P:Prop.P. *) + +definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))). + +(* +lemma compl1: ∀s. + CF s (to_Some fst) → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) → + CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (size_f (λx.(s (|x|))) x)) + (λx.U 〈fst x,x〉 (|s (|x|)|)). +#s #H1 #H2 #H3 @CFU // +qed. + +lemma compl1: ∀s. + CF s (to_Some fst) → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) → + CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (|(s x)| )) + (λx.U 〈fst x,x〉 (|s (|x|)|)). +#s #H1 #H2 #H3 @monotonic_CF [3: @(CFU ??? s s s) @CFU // +qed. *) + +lemma diag_s: ∀s. minimal s → constructible s → + CF (λx.s x + sU x x (s x)) (diag_cf s). +#s * #Hs_id #Hs_c #Hs_constr +@ext_CF [2: #n @sym_eq @diag_cf_def | skip] +@(monotonic_CF ???? (IF_CF (λi:ℕ.U (pair (fst i) i) (|of_size (s (|i|))|)) + … (λi.s i + s i + s i + (sU (size_f fst i) (size_f (λi.i) i) (size_f (λi.of_size (s (|i|))) i))) … (Hs_c 1) (Hs_c 0) … )) + [2: @CFU [@CF_fst // | // |@Hs_constr] + |@(O_ext2 (λn:ℕ.s n+sU (size_f fst n) n (s n) + (s n+s n+s n+s n))) + [2: #i >size_f_size >size_of_size >size_f_id //] + @O_absorbr + [%{1} %{0} #n #_ >commutative_times associative_times +@le_times // @Hs1s2 @(le_maxr … lemax) +qed. \ No newline at end of file diff --git a/weblib/arithmetics/bigops.ma b/weblib/arithmetics/bigops.ma index 0c10b02bb..41c680088 100644 --- a/weblib/arithmetics/bigops.ma +++ b/weblib/arithmetics/bigops.ma @@ -322,7 +322,7 @@ qed. @(a href="cic:/matita/arithmetics/nat/le_gen.def(1)"le_gen/a ? n1) #i generalize in match p2; (elim i) [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2 >a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a - [@(Hind ? (a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"le_O_n/a ?)) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"sub_hkO/a/span/span/ | @(a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"transitive_sub/a … (a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"sub_lt/a …) sub2) //] + [@(Hind ? (a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"le_O_n/a ?)) [@a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"sub_hkO/a % | @(a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"transitive_sub/a … (a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"sub_lt/a …) sub2) //] |@(a href="cic:/matita/arithmetics/bigops/sub0_to_false.def(4)"sub0_to_false/a … sub2) // ] |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/an1)) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/] #len diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index 8c3231ee1..28248bdfc 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -11,7 +11,7 @@ include "basics/relations.ma". -inductive nat : Type[0] ≝ +img class="anchor" src="icons/tick.png" id="nat"inductive nat : Type[0] ≝ | O : nat | S : nat → nat. @@ -19,37 +19,37 @@ interpretation "Natural numbers" 'N = nat. alias num (instance 0) = "natural number". -definition pred ≝ +img class="anchor" src="icons/tick.png" id="pred"definition pred ≝ λn. match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ p]. -theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n). +img class="anchor" src="icons/tick.png" id="pred_Sn"theorem pred_Sn : ∀n.n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n). // qed. -theorem injective_S : a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a. +img class="anchor" src="icons/tick.png" id="injective_S"theorem injective_S : a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a. // qed. (* theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m. //. qed. *) -theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. +img class="anchor" src="icons/tick.png" id="not_eq_S"theorem not_eq_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed. -definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ +img class="anchor" src="icons/tick.png" id="not_zero"definition not_zero: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. match n with [ O ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a | (S p) ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a ]. -theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. +img class="anchor" src="icons/tick.png" id="not_eq_O_S"theorem not_eq_O_S : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #eqOS (change with (a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a)) >eqOS // qed. -theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. +img class="anchor" src="icons/tick.png" id="not_eq_n_Sn"theorem not_eq_n_Sn: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/ qed. -theorem nat_case: +img class="anchor" src="icons/tick.png" id="nat_case"theorem nat_case: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀P:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a → P a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) → (∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → P (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m)) → P n. #n #P (elim n) /span class="autotactic"2span class="autotrace" trace /span/span/ qed. -theorem nat_elim2 : +img class="anchor" src="icons/tick.png" id="nat_elim2"theorem nat_elim2 : ∀R:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop. (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a n) → (∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) @@ -57,18 +57,18 @@ theorem nat_elim2 : → ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. R n m. #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /span class="autotactic"2span class="autotrace" trace /span/span/ qed. -theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am). +img class="anchor" src="icons/tick.png" id="decidable_eq_nat"theorem decidable_eq_nat : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (na title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/am). @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a #n [ (cases n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a/span/span/ | #m #Hind (cases Hind) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"not_eq_S/a/span/span/] qed. (*************************** plus ******************************) -let rec plus n m ≝ +img class="anchor" src="icons/tick.png" id="plus"let rec plus n m ≝ match n with [ O ⇒ m | S p ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (plus p m) ]. interpretation "natural plus" 'plus x y = (plus x y). -theorem plus_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an. +img class="anchor" src="icons/tick.png" id="plus_O_n"theorem plus_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural plus" href="cic:/fakeuri.def(1)"+/an. // qed. (* @@ -76,10 +76,10 @@ theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m. // qed. *) -theorem plus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a. +img class="anchor" src="icons/tick.png" id="plus_n_O"theorem plus_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="natural number" href="cic:/fakeuri.def(1)"0/a. #n (elim n) normalize // qed. -theorem plus_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. +img class="anchor" src="icons/tick.png" id="plus_n_Sm"theorem plus_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. #n (elim n) normalize // qed. (* @@ -92,16 +92,16 @@ theorem plus_n_1 : ∀n:nat. S n = n+1. // qed. *) -theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. +img class="anchor" src="icons/tick.png" id="commutative_plus"theorem commutative_plus: a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a ? a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. #n (elim n) normalize // qed. -theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. +img class="anchor" src="icons/tick.png" id="associative_plus"theorem associative_plus : a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. #n (elim n) normalize // qed. -theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a. +img class="anchor" src="icons/tick.png" id="assoc_plus1"theorem assoc_plus1: ∀a,b,c. c a title="natural plus" href="cic:/fakeuri.def(1)"+/a (b a title="natural plus" href="cic:/fakeuri.def(1)"+/a a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a a. // qed. -theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am). +img class="anchor" src="icons/tick.png" id="injective_plus_r"theorem injective_plus_r: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (λm.na title="natural plus" href="cic:/fakeuri.def(1)"+/am). #n (elim n) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a/span/span/ qed. (* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m @@ -115,43 +115,43 @@ theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m). (*************************** times *****************************) -let rec times n m ≝ +img class="anchor" src="icons/tick.png" id="times"let rec times n m ≝ match n with [ O ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | S p ⇒ ma title="natural plus" href="cic:/fakeuri.def(1)"+/a(times p m) ]. interpretation "natural times" 'times x y = (times x y). -theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am. +img class="anchor" src="icons/tick.png" id="times_Sn_m"theorem times_Sn_m: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. ma title="natural plus" href="cic:/fakeuri.def(1)"+/ana title="natural times" href="cic:/fakeuri.def(1)"*/am a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a na title="natural times" href="cic:/fakeuri.def(1)"*/am. // qed. -theorem times_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an. +img class="anchor" src="icons/tick.png" id="times_O_n"theorem times_O_n: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/aa title="natural times" href="cic:/fakeuri.def(1)"*/an. // qed. -theorem times_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +img class="anchor" src="icons/tick.png" id="times_n_O"theorem times_n_O: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. #n (elim n) // qed. -theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m). +img class="anchor" src="icons/tick.png" id="times_n_Sm"theorem times_n_Sm : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural plus" href="cic:/fakeuri.def(1)"+/a(na title="natural times" href="cic:/fakeuri.def(1)"*/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m). #n (elim n) normalize // qed. -theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. +img class="anchor" src="icons/tick.png" id="commutative_times"theorem commutative_times : a href="cic:/matita/basics/relations/commutative.def(1)"commutative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. #n (elim n) normalize // qed. (* variant sym_times : \forall n,m:nat. n*m = m*n \def symmetric_times. *) -theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. +img class="anchor" src="icons/tick.png" id="distributive_times_plus"theorem distributive_times_plus : a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"plus/a. #n (elim n) normalize // qed. -theorem distributive_times_plus_r : +img class="anchor" src="icons/tick.png" id="distributive_times_plus_r"theorem distributive_times_plus_r : ∀a,b,c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. (ba title="natural plus" href="cic:/fakeuri.def(1)"+/ac)a title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ba title="natural times" href="cic:/fakeuri.def(1)"*/aa a title="natural plus" href="cic:/fakeuri.def(1)"+/a ca title="natural times" href="cic:/fakeuri.def(1)"*/aa. // qed. -theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. +img class="anchor" src="icons/tick.png" id="associative_times"theorem associative_times: a href="cic:/matita/basics/relations/associative.def(1)"associative/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a. #n (elim n) normalize // qed. -lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az). +img class="anchor" src="icons/tick.png" id="times_times"lemma times_times: ∀x,y,z. xa title="natural times" href="cic:/fakeuri.def(1)"*/a(ya title="natural times" href="cic:/fakeuri.def(1)"*/az) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ya title="natural times" href="cic:/fakeuri.def(1)"*/a(xa title="natural times" href="cic:/fakeuri.def(1)"*/az). // qed. -theorem times_n_1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a. +img class="anchor" src="icons/tick.png" id="times_n_1"theorem times_n_1 : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural times" href="cic:/fakeuri.def(1)"*/a a title="natural number" href="cic:/fakeuri.def(1)"1/a. #n // qed. (* ci servono questi risultati? @@ -182,7 +182,7 @@ qed. (******************** ordering relations ************************) -inductive le (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ +img class="anchor" src="icons/tick.png" id="le"inductive le (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ | le_n : le n n | le_S : ∀ m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. le n m → le n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m). @@ -190,7 +190,7 @@ interpretation "natural 'less or equal to'" 'leq x y = (le x y). interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)). -definition lt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. +img class="anchor" src="icons/tick.png" id="lt"definition lt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. interpretation "natural 'less than'" 'lt x y = (lt x y). interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). @@ -198,16 +198,16 @@ interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). (* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m). // qed. *) -definition ge: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. +img class="anchor" src="icons/tick.png" id="ge"definition ge: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. interpretation "natural 'greater or equal to'" 'geq x y = (ge x y). -definition gt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an. +img class="anchor" src="icons/tick.png" id="gt"definition gt: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Prop ≝ λn,m.ma title="natural 'less than'" href="cic:/fakeuri.def(1)"</an. interpretation "natural 'greater than'" 'gt x y = (gt x y). interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)). -theorem transitive_le : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a. +img class="anchor" src="icons/tick.png" id="transitive_le"theorem transitive_le : a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a. #a #b #c #leab #lebc (elim lebc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. @@ -215,29 +215,29 @@ qed. theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p \def transitive_le. *) -theorem transitive_lt: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a. +img class="anchor" src="icons/tick.png" id="transitive_lt"theorem transitive_lt: a href="cic:/matita/basics/relations/transitive.def(2)"transitive/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a. #a #b #c #ltab #ltbc (elim ltbc) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/qed. (* theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p \def transitive_lt. *) -theorem le_S_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. +img class="anchor" src="icons/tick.png" id="le_S_S"theorem le_S_S: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m. #n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. -theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. +img class="anchor" src="icons/tick.png" id="le_O_n"theorem le_O_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. #n (elim n) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. -theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. +img class="anchor" src="icons/tick.png" id="le_n_Sn"theorem le_n_Sn : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n. /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a, a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a/span/span/ qed. -theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. +img class="anchor" src="icons/tick.png" id="le_pred_n"theorem le_pred_n : ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. #n (elim n) // qed. -theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a. +img class="anchor" src="icons/tick.png" id="monotonic_pred"theorem monotonic_pred: a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a ? a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"le/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a. #n #m #lenm (elim lenm) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. -theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. +img class="anchor" src="icons/tick.png" id="le_S_S_to_le"theorem le_S_S_to_le: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. (* demo *) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ qed. @@ -248,10 +248,14 @@ theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m. theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m. /2/ qed. *) -theorem lt_to_not_zero : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a m. +img class="anchor" src="icons/tick.png" id="lt_to_not_zero"theorem lt_to_not_zero : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/not_zero.def(1)"not_zero/a m. #n #m #Hlt (elim Hlt) // qed. (* lt vs. le *) + +img class="anchor" src="icons/tick.png" id="lt_to_le"lemma lt_to_le: ∀n,m. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. +#n #m #H @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a @H qed-. + theorem not_le_Sn_O: ∀ n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"≰/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. #n @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Hlen0 @(a href="cic:/matita/arithmetics/nat/lt_to_not_zero.def(2)"lt_to_not_zero/a ?? Hlen0) qed.