commit by user andrea

diff --git a/weblib/arithmetics/min_max.ma b/weblib/arithmetics/min_max.ma
new file mode 100644 (file)
index 0000000..3b93593
--- /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)))}.
+
+\ 5img class="anchor" src="icons/tick.png" id="Max_assoc"\ 6lemma Max_assoc: ∀a,b,c. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 a b) c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 a (\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 b c).
+#a #b #c normalize cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 a b)) #leab >leab normalize
+  [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 b c )) #lebc >lebc normalize
+    [>(\ 5a href="cic:/matita/arithmetics/nat/le_to_leb_true.def(7)"\ 6le_to_leb_true\ 5/a\ 6 a c) // @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? b) @\ 5a href="cic:/matita/arithmetics/nat/leb_true_to_le.def(7)"\ 6leb_true_to_le\ 5/a\ 6 //
+    |>leab //
+    ]
+  |cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 b c )) #lebc >lebc normalize //
+   >leab normalize >(\ 5a href="cic:/matita/arithmetics/nat/not_le_to_leb_false.def(7)"\ 6not_le_to_leb_false\ 5/a\ 6 a c) // @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 
+   @(\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"\ 6transitive_lt\ 5/a\ 6 ? b) @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/leb_false_to_not_le.def(7)"\ 6leb_false_to_not_le\ 5/a\ 6 //
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="Max0"\ 6lemma Max0 : ∀n. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+// qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="Max0r"\ 6lemma Max0r : ∀n. \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+#n >\ 5a href="cic:/matita/arithmetics/nat/commutative_max.def(8)"\ 6commutative_max\ 5/a\ 6 //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="MaxA"\ 6definition MaxA ≝ 
+  \ 5a href="cic:/matita/arithmetics/bigops/Aop.con(0,1,2)"\ 6mk_Aop\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/min_max/Max0.def(3)"\ 6Max0\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/min_max/Max0r.def(9)"\ 6Max0r\ 5/a\ 6 (λa,b,c.\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/min_max/Max_assoc.def(8)"\ 6Max_assoc\ 5/a\ 6 a b c)). 
+
+\ 5img class="anchor" src="icons/tick.png" id="MaxAC"\ 6definition MaxAC ≝ \ 5a href="cic:/matita/arithmetics/bigops/ACop.con(0,1,2)"\ 6mk_ACop\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/min_max/MaxA.def(10)"\ 6MaxA\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/commutative_max.def(8)"\ 6commutative_max\ 5/a\ 6.
+
+\ 5img class="anchor" src="icons/tick.png" id="le_Max"\ 6lemma le_Max: ∀f,p,n,a. a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
+  f a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6  Max_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i).
+#f #p #n #a #ltan #pa 
+>(\ 5a href="cic:/matita/arithmetics/bigops/bigop_diff.def(8)"\ 6bigop_diff\ 5/a\ 6 p ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/min_max/MaxAC.def(11)"\ 6MaxAC\ 5/a\ 6 f a n) // @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 ?))
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="Max_le"\ 6lemma Max_le: ∀f,p,n,b. 
+  (∀a.a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → f a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b) → Max_{i < n | p i\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6(f i) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b.
+#f #p #n elim n #b #H // 
+#b0 #H1 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p b)) #Hb
+  [>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Strue.def(3)"\ 6bigop_Strue\ 5/a\ 6 [2:@Hb] @\ 5a href="cic:/matita/arithmetics/nat/to_max.def(3)"\ 6to_max\ 5/a\ 6 [@H1 // | @H #a #ltab #pa @H1 // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //]
+  |>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6 [2:@Hb] @H #a #ltab #pa @H1 // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
+  ]
+qed.
+
+