weblib/arithmetics/min_max.ma

   1 include "arithmetics/bigops.ma".
   2
   3 notation "Max_{ ident i < n | p } f"
   4   with precedence 80
   5 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
   6
   7 notation "Max_{ ident i < n } f"
   8   with precedence 80
   9 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  10
  11 notation "Max_{ ident j ∈ [a,b[ } f"
  12   with precedence 80
  13 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  14   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  15
  16 notation "Max_{ ident j ∈ [a,b[ | p } f"
  17   with precedence 80
  18 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  19   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  20
  21 \ 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).
  22 #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
  23   [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
  24     [>(\ 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 //
  25     |>leab //
  26     ]
  27   |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 //
  28    >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
  29    @(\ 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 //
  30   ]
  31 qed.
  32
  33 \ 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.
  34 // qed.
  35
  36 \ 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.
  37 #n >\ 5a href="cic:/matita/arithmetics/nat/commutative_max.def(8)"\ 6commutative_max\ 5/a\ 6 //
  38 qed.
  39
  40 \ 5img class="anchor" src="icons/tick.png" id="MaxA"\ 6definition MaxA ≝
  41   \ 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)).
  42
  43 \ 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.
  44
  45 \ 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 →
  46   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).
  47 #f #p #n #a #ltan #pa
  48 >(\ 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 ?))
  49 qed.
  50
  51 \ 5img class="anchor" src="icons/tick.png" id="Max_le"\ 6lemma Max_le: ∀f,p,n,b.
  52   (∀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.
  53 #f #p #n elim n #b #H //
  54 #b0 #H1 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p b)) #Hb
  55   [>\ 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 //]
  56   |>\ 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 //
  57   ]
  58 qed.
  59
  60