From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Sat, 27 Apr 2013 14:49:38 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1176
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5571ac6bf4e43a0175f2ccf8ae1c129e949c84a8;p=helm.git

commit by user andrea
---

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.
+
+