From 5571ac6bf4e43a0175f2ccf8ae1c129e949c84a8 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Sat, 27 Apr 2013 14:49:38 +0000 Subject: [PATCH] commit by user andrea --- weblib/arithmetics/min_max.ma | 60 +++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 weblib/arithmetics/min_max.ma diff --git a/weblib/arithmetics/min_max.ma b/weblib/arithmetics/min_max.ma new file mode 100644 index 000000000..3b93593b6 --- /dev/null +++ b/weblib/arithmetics/min_max.ma @@ -0,0 +1,60 @@ +include "arithmetics/bigops.ma". + +notation "Max_{ ident i < n | p } f" + with precedence 80 +for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}. + +notation "Max_{ ident i < n } f" + with precedence 80 +for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}. + +notation "Max_{ ident j ∈ [a,b[ } f" + with precedence 80 +for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "Max_{ ident j ∈ [a,b[ | p } f" + with precedence 80 +for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +img class="anchor" src="icons/tick.png" id="Max_assoc"lemma Max_assoc: ∀a,b,c. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a b) c a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a (a href="cic:/matita/arithmetics/nat/max.def(2)"max/a b c). +#a #b #c normalize cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a a b)) #leab >leab normalize + [cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a b c )) #lebc >lebc normalize + [>(a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"le_to_leb_true/a a c) // @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? b) @a href="cic:/matita/arithmetics/nat/leb_true_to_le.def(7)"leb_true_to_le/a // + |>leab // + ] + |cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a b c )) #lebc >lebc normalize // + >leab normalize >(a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"not_le_to_leb_false/a a c) // @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a + @(a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a ? b) @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @a href="cic:/matita/arithmetics/nat/leb_false_to_not_le.def(7)"leb_false_to_not_le/a // + ] +qed. + +img class="anchor" src="icons/tick.png" id="Max0"lemma Max0 : ∀n. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a title="natural number" href="cic:/fakeuri.def(1)"0/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n. +// qed. + +img class="anchor" src="icons/tick.png" id="Max0r"lemma Max0r : ∀n. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n. +#n >a href="cic:/matita/arithmetics/nat/commutative_max.def(8)"commutative_max/a // +qed. + +img class="anchor" src="icons/tick.png" id="MaxA"definition MaxA ≝ + a href="cic:/matita/arithmetics/bigops/Aop.con(0,1,2)"mk_Aop/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a href="cic:/matita/arithmetics/min_max/Max0.def(3)"Max0/a a href="cic:/matita/arithmetics/min_max/Max0r.def(9)"Max0r/a (λa,b,c.a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a … (a href="cic:/matita/arithmetics/min_max/Max_assoc.def(8)"Max_assoc/a a b c)). + +img class="anchor" src="icons/tick.png" id="MaxAC"definition MaxAC ≝ a href="cic:/matita/arithmetics/bigops/ACop.con(0,1,2)"mk_ACop/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a href="cic:/matita/arithmetics/min_max/MaxA.def(10)"MaxA/a a href="cic:/matita/arithmetics/nat/commutative_max.def(8)"commutative_max/a. + +img class="anchor" src="icons/tick.png" id="le_Max"lemma le_Max: ∀f,p,n,a. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + f a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a Max_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i). +#f #p #n #a #ltan #pa +>(a href="cic:/matita/arithmetics/bigops/bigop_diff.def(8)"bigop_diff/a p ? a title="natural number" href="cic:/fakeuri.def(1)"0/a a href="cic:/matita/arithmetics/min_max/MaxAC.def(11)"MaxAC/a f a n) // @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a ?)) +qed. + +img class="anchor" src="icons/tick.png" id="Max_le"lemma Max_le: ∀f,p,n,b. + (∀a.a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → f a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b) → Max_{i < n | p ia title="bigop" href="cic:/fakeuri.def(1)"}/a(f i) a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b. +#f #p #n elim n #b #H // +#b0 #H1 cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p b)) #Hb + [>a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"bigop_Strue/a [2:@Hb] @a href="cic:/matita/arithmetics/nat/to_max.def(3)"to_max/a [@H1 // | @H #a #ltab #pa @H1 // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a //] + |>a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"bigop_Sfalse/a [2:@Hb] @H #a #ltab #pa @H1 // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a // + ] +qed. + + -- 2.39.2