(* maximization *)
-let rec max' i f d ≝
+\ 5img class="anchor" src="icons/tick.png" id="max'"\ 6let rec max' i f d ≝
match i with
[ O ⇒ d
| S j ⇒
[ true ⇒ j
| false ⇒ max' j f d]].
-definition max ≝ λn.λf.max' n f O.
+\ 5img class="anchor" src="icons/tick.png" id="max"\ 6definition max ≝ λn.λf.\ 5a href="cic:/matita/arithmetics/minimization/max'.fix(0,0,1)"\ 6max'\ 5/a\ 6 n f \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
-theorem max_O: ∀f. \ 5A href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/A\ 6 O f = O.
+\ 5img class="anchor" src="icons/tick.png" id="max_O"\ 6theorem max_O: ∀f. \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
// qed.
-theorem max_cases: ∀f.∀n.
- (f n = true ∧ max (S n) f = n) ∨
- (f n = false ∧ max (S n) f = max n f).
-#f #n normalize cases (f n) normalize /3/ qed.
+\ 5img class="anchor" src="icons/tick.png" id="max_cases"\ 6theorem max_cases: ∀f.∀n.
+ (f n \ 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 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6
+ (f n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f).
+#f #n normalize cases (f n) normalize /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem le_max_n: ∀f.∀n. max n f ≤ n.
+\ 5img class="anchor" src="icons/tick.png" id="le_max_n"\ 6theorem le_max_n: ∀f.∀n. \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"\ 6max\ 5/a\ 6 n f \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
#f #n (elim n) // #m #Hind
-normalize (cases (f m)) normalize @le_S //
+normalize (cases (f m)) normalize @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
(* non trova Hind *)
@Hind
qed.
-theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
-#f #n #posn @(lt_O_n_elim ? posn) #m
-normalize (cases (f m)) normalize apply le_S_S //
+\ 5img class="anchor" src="icons/tick.png" id="lt_max_n"\ 6theorem lt_max_n : ∀f.∀n. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"\ 6max\ 5/a\ 6 n f \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n.
+#f #n #posn @(\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"\ 6lt_O_n_elim\ 5/a\ 6 ? posn) #m
+normalize (cases (f m)) normalize \ 5font class="Apple-style-span" color="#FF0000"\ 6@\ 5/font\ 6\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 //
@le_max_n qed.
-theorem le_to_le_max : ∀f.∀n,m.
-n ≤ m → max n f ≤ max m f.
+\ 5img class="anchor" src="icons/tick.png" id="le_to_le_max"\ 6theorem le_to_le_max : ∀f.∀n,m.
+n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"\ 6max\ 5/a\ 6 m f.
#f #n #m #H (elim H) //
-#i #leni #Hind @(transitive_le … Hind)
-(cases (max_cases f i)) * #_ /2/
+#i #leni #Hind @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … Hind)
+(cases (\ 5a href="cic:/matita/arithmetics/minimization/max_cases.def(3)"\ 6max_cases\ 5/a\ 6 f i)) * #_ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem true_to_le_max: ∀f.∀n,m.
- m < n → f m = true → m ≤ max n f.
+\ 5img class="anchor" src="icons/tick.png" id="true_to_le_max"\ 6theorem true_to_le_max: ∀f.∀n,m.
+ m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f m \ 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 → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f.
#f #n (elim n)
- [#m #ltmO @False_ind /2/
+ [#m #ltmO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|#i #Hind #m #ltm
- (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm)))
- [#ltm #fm @(transitive_le ? (max i f))
- [@Hind /2/ | @le_to_le_max //]
+ (cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 … ltm)))
+ [#ltm #fm @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 i f))
+ [@Hind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ | @\ 5a href="cic:/matita/arithmetics/minimization/le_to_le_max.def(4)"\ 6le_to_le_max\ 5/a\ 6 //]
|#eqm >eqm #eqf normalize >eqf //
]
qed.
-theorem lt_max_to_false: ∀f.∀n,m.
- m < n → max n f < m → f m = false.
-#f #n #m #ltnm #eqf cases(true_or_false (f m)) //
-#fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max //
+\ 5img class="anchor" src="icons/tick.png" id="lt_max_to_false"\ 6theorem lt_max_to_false: ∀f.∀n,m.
+ m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → f m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#f #n #m #ltnm #eqf cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f m)) //
+#fm @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … eqf) @(\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6) @\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_max.def(6)"\ 6true_to_le_max\ 5/a\ 6 //
qed.
-lemma max_exists: ∀f.∀n,m.m < n → f m =true →
- (∀i. m < i → i < n → f i = false) → max n f = m.
+\ 5img class="anchor" src="icons/tick.png" id="max_exists"\ 6lemma max_exists: ∀f.∀n,m.m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f m \ 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 →
+ (∀i. m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
#f #n (elim n) #m
- [#ltO @False_ind /2/
+ [#ltO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|#Hind #max #ltmax #fmax #ismax
- cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …)))
+ cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 …(\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 …(ltmax …)))
#ltm normalize
[>(ismax m …) // normalize @(Hind max ltm fmax)
- #i #Hl #Hr @ismax // @le_S //
+ #i #Hl #Hr @ismax // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
|<ltm >fmax //
]
]
qed.
-lemma max_not_exists: ∀f.∀n.
- (∀i. i < n → f i = false) → max n f = O.
-#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
-normalize >ffalse // @Hind /2/
+\ 5img class="anchor" src="icons/tick.png" id="max_not_exists"\ 6lemma max_not_exists: ∀f.∀n.
+ (∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+#f #n #ffalse @(\ 5a href="cic:/matita/arithmetics/nat/le_gen.def(1)"\ 6le_gen\ 5/a\ 6 ? n) #i (elim i) // #j #Hind #ltj
+normalize >ffalse // @Hind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O.
+\ 5img class="anchor" src="icons/tick.png" id="fmax_false"\ 6lemma fmax_false: ∀f.∀n,m.\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m → f m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
#f #n #m (elim n) //
-#i #Hind normalize cases(true_or_false … (f i)) #fi >fi
+#i #Hind normalize cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (f i)) #fi >fi
normalize
- [#eqm #fm @False_ind @(absurd … fi) // |@Hind]
+ [#eqm #fm @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … fi) // |@Hind]
qed.
-inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝
- | found : ∀m:nat.m < n → f m =true →
- (∀i. m < i → i < n → f i = false) → max_spec n f m
- | not_found: (∀i.i < n → f i = false) → max_spec n f O.
+\ 5img class="anchor" src="icons/tick.png" id="max_spec"\ 6inductive max_spec (n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→Prop ≝
+ | found : ∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f m \ 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 →
+ (∀i. m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → max_spec n f m
+ | not_found: (∀i.i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → max_spec n f \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
-theorem max_spec_to_max: ∀f.∀n,m.
- max_spec n f m → max n f = m.
+\ 5img class="anchor" src="icons/tick.png" id="max_spec_to_max"\ 6theorem max_spec_to_max: ∀f.∀n,m.
+ \ 5a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"\ 6max_spec\ 5/a\ 6 n f m → \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
#f #n #m #spec (cases spec)
- [#max #ltmax #fmax #ismax @max_exists // @ismax
- |#ffalse @max_not_exists @ffalse
+ [#max #ltmax #fmax #ismax @\ 5a href="cic:/matita/arithmetics/minimization/max_exists.def(6)"\ 6max_exists\ 5/a\ 6 // @ismax
+ |#ffalse @\ 5a href="cic:/matita/arithmetics/minimization/max_not_exists.def(9)"\ 6max_not_exists\ 5/a\ 6 @ffalse
]
qed.
-theorem max_to_max_spec: ∀f.∀n,m.
- max n f = m → max_spec n f m.
+\ 5img class="anchor" src="icons/tick.png" id="max_to_max_spec"\ 6theorem max_to_max_spec: ∀f.∀n,m.
+ \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"\ 6max_spec\ 5/a\ 6 n f m.
#f #n #m (cases n)
- [#eqm <eqm %2 #i #ltiO @False_ind /2/
- |#n #eqm cases(true_or_false (f m)) #fm
+ [#eqm <eqm %2 #i #ltiO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#n #eqm cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f m)) #fm
(* non trova max_to_false *)
- [%1 /2/
- |lapply (fmax_false ??? eqm fm) #eqmO >eqmO
- %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) //
+ [%1 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/minimization/lt_max_n.def(5)"\ 6lt_max_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"\ 6lt_max_to_false\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |lapply (\ 5a href="cic:/matita/arithmetics/minimization/fmax_false.def(4)"\ 6fmax_false\ 5/a\ 6 ??? eqm fm) #eqmO >eqmO
+ %2 #i (cases i) // #j #ltj @(\ 5a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"\ 6lt_max_to_false\ 5/a\ 6 … ltj) //
qed.
-theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) →
- max n f = max n g.
+\ 5img class="anchor" src="icons/tick.png" id="max_f_g"\ 6theorem max_f_g: ∀f,g,n.(∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g i) →
+ \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n g.
#f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
-#i #ltim @ext /2/
+#m #Hind #ext whd in ⊢(??%%); >ext // normalize in Hind; >Hind //
+# i #ltim @ext /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"\ 6transitive_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
-max n f ≤ max n g.
+\ 5img class="anchor" src="icons/tick.png" id="le_max_f_max_g"\ 6theorem le_max_f_max_g: ∀f,g,n. (∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → f i \ 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 → g i \ 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) →
+\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n g.
#f #g #n (elim n) //
-#m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq
+#m #Hind #ext normalize (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f m))) #Heq >Heq
[>ext //
- |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
+ |(cases (g m)) normalize [@\ 5a href="cic:/matita/arithmetics/minimization/le_max_n.def(3)"\ 6le_max_n\ 5/a\ 6] @Hind #i #ltim @ext /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"\ 6transitive_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem f_max_true : ∀ f.∀n.
-(∃i:nat. i < n ∧ f i = true) → f (max n f) = true.
-#f #n cases(max_to_max_spec f n (max n f) (refl …)) //
-#Hall * #x * #ltx #fx @False_ind @(absurd … fx) >Hall /2/
+\ 5img class="anchor" src="icons/tick.png" id="f_max_true"\ 6theorem f_max_true : ∀ f.∀n.
+(∃i:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 f i \ 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 (\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f) \ 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 #n cases(\ 5a href="cic:/matita/arithmetics/minimization/max_to_max_spec.def(10)"\ 6max_to_max_spec\ 5/a\ 6 f n (\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/a\ 6 n f) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
+#Hall * #x * #ltx #fx @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … fx) >Hall /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
(* minimization *)
(* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
returns b + k otherwise *)
-let rec min k b f ≝
+\ 5img class="anchor" src="icons/tick.png" id="min"\ 6let rec min k b f ≝
match k with
[ O ⇒ b
| S p ⇒
match f b with
[ true ⇒ b
- | false ⇒ min p (S b) f]].
+ | false ⇒ min p (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b) f]].
-definition min0 ≝ λn.λf. min n 0 f.
+\ 5img class="anchor" src="icons/tick.png" id="min0"\ 6definition min0 ≝ λn.λf. \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 f.
-theorem min_O_f : ∀f.∀b. min O b f = b.
+\ 5img class="anchor" src="icons/tick.png" id="min_O_f"\ 6theorem min_O_f : ∀f.∀b. \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
// qed.
-theorem true_min: ∀f.∀b.
- f b = true → ∀n.min n b f = b.
+\ 5img class="anchor" src="icons/tick.png" id="true_min"\ 6theorem true_min: ∀f.∀b.
+ f b \ 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 → ∀n.\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
#f #b #fb #n (cases n) // #n normalize >fb normalize //
qed.
-theorem false_min: ∀f.∀n,b.
- f b = false → min (S n) b f = min n (S b) f.
+\ 5img class="anchor" src="icons/tick.png" id="false_min"\ 6theorem false_min: ∀f.∀n,b.
+ f b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b) f.
#f #n #b #fb normalize >fb normalize //
qed.
#f #n #b1 #b2 #leb (elim n) //
#m #Hind normalize (cases (f m)) normalize *)
-theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
+\ 5img class="anchor" src="icons/tick.png" id="le_min_r"\ 6theorem le_min_r: ∀f.∀n,b. \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
#f #n normalize (elim n) // #m #Hind #b
normalize (cases (f b)) normalize //
qed.
-theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
+\ 5img class="anchor" src="icons/tick.png" id="le_min_l"\ 6theorem le_min_l: ∀f.∀n,b. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f.
#f #n normalize (elim n) // #m #Hind #b
-normalize (cases (f b)) normalize /2/
+normalize (cases (f b)) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem le_to_le_min : ∀f.∀n,m.
-n ≤ m → ∀b.min n b f ≤ min m b f.
-#f @nat_elim2 //
- [#n #leSO @False_ind /2/
+\ 5img class="anchor" src="icons/tick.png" id="le_to_le_min"\ 6theorem le_to_le_min : ∀f.∀n,m.
+n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → ∀b.\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 m b f.
+#f @\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 //
+ [#n #leSO @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|#n #m #Hind #leSS #b
- (cases (true_or_false (f b))) #fb
- [lapply (true_min …fb) #H >H >H //
- |>false_min // >false_min // @Hind /2/
+ (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b))) #fb
+ [lapply (\ 5a href="cic:/matita/arithmetics/minimization/true_min.def(4)"\ 6true_min\ 5/a\ 6 …fb) #H >H >H //
+ |>\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"\ 6false_min\ 5/a\ 6 // >\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"\ 6false_min\ 5/a\ 6 // @Hind /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"\ 6monotonic_pred\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
]
qed.
-theorem true_to_le_min: ∀f.∀n,m,b.
- b ≤ m → f m = true → min n b f ≤ m.
+\ 5img class="anchor" src="icons/tick.png" id="true_to_le_min"\ 6theorem true_to_le_min: ∀f.∀n,m,b.
+ b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → f m \ 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 → \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
#f #n (elim n) //
-#i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
+#i #Hind #m #b #leb (cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … leb))
[#ltm #fm normalize (cases (f b)) normalize // @Hind //
|#eqm <eqm #eqb normalize >eqb normalize //
]
qed.
-theorem lt_min_to_false: ∀f.∀n,m,b.
- b ≤ m → m < min n b f → f m = false.
-#f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
-#fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
+\ 5img class="anchor" src="icons/tick.png" id="lt_min_to_false"\ 6theorem lt_min_to_false: ∀f.∀n,m,b.
+ b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f → f m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#f #n #m #b #lebm #ltm cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f m)) //
+#fm @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … ltm) @(\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6) @\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"\ 6true_to_le_min\ 5/a\ 6 //
qed.
-theorem fmin_true: ∀f.∀n,m,b.
- m = min n b f → m < n + b → f m = true.
+\ 5img class="anchor" src="icons/tick.png" id="fmin_true"\ 6theorem fmin_true: ∀f.∀n,m,b.
+ m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f → m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b → f m \ 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 #n (elim n)
- [#m #b normalize #eqmb >eqmb #leSb @(False_ind)
- @(absurd … leSb) //
- |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
- [>true_min //
- |>false_min // #eqm #ltm @(Hind m (S b)) /2/
+ [#m #b normalize #eqmb >eqmb #leSb @(\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6)
+ @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … leSb) //
+ |#n #Hind #m #b (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b))) #caseb
+ [>\ 5a href="cic:/matita/arithmetics/minimization/true_min.def(4)"\ 6true_min\ 5/a\ 6 //
+ |>\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"\ 6false_min\ 5/a\ 6 // #eqm #ltm @(Hind m (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
]
]
qed.
-lemma min_exists: ∀f.∀t,m. m < t → f m = true →
-∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b →
- min k b f = m.
+\ 5img class="anchor" src="icons/tick.png" id="min_exists"\ 6lemma min_exists: ∀f.∀t,m. m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 t → f m \ 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 →
+∀k,b.b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → (∀i. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 k \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b →
+ \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 k b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
#f #t #m #ltmt #fm #k (elim k)
- [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
- @lt_to_not_le //
- |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
- [#ltbm >false_min /2/ @Hind //
- [#i #H #H1 @ismin /2/ | >eqt normalize //]
- |#eqbm >true_min //
+ [#b #lebm #ismin #eqtb @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … lebm) <eqtb
+ @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 //
+ |#d #Hind #b #lebm #ismin #eqt cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 …lebm)
+ [#ltbm >\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"\ 6false_min\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ @Hind //
+ [#i #H #H1 @ismin /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | >eqt normalize //]
+ |#eqbm >\ 5a href="cic:/matita/arithmetics/minimization/true_min.def(4)"\ 6true_min\ 5/a\ 6 //
]
]
qed.
-lemma min_not_exists: ∀f.∀n,b.
- (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
+\ 5img class="anchor" src="icons/tick.png" id="min_not_exists"\ 6lemma min_not_exists: ∀f.∀n,b.
+ (∀i. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
#f #n (elim n) //
-#p #Hind #b #ffalse >false_min
- [>Hind // #i #H #H1 @ffalse /2/
+#p #Hind #b #ffalse >\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"\ 6false_min\ 5/a\ 6
+ [>Hind // #i #H #H1 @ffalse /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|@ffalse //
]
qed.
-lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in
- f m = false → m = n+b.
+\ 5img class="anchor" src="icons/tick.png" id="fmin_false"\ 6lemma fmin_false: ∀f.∀n,b.let m ≝ \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f in
+ f m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6b.
#f #n (elim n) //
-#i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
+#i #Hind #b normalize cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (f b)) #fb >fb
normalize
- [#eqm @False_ind @(absurd … fb) //
- |>plus_n_Sm @Hind]
+ [#eqm @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … fb) //
+ |>\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 @Hind]
qed.
-inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
- | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
- (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
- | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
+\ 5img class="anchor" src="icons/tick.png" id="min_spec"\ 6inductive min_spec (n,b:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (f:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→Prop ≝
+ | found : ∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → m \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b → f m \ 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 →
+ (∀i. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → min_spec n b f m
+ | not_found: (∀i.b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 (n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b) → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) →
+ min_spec n b f (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6b).
-theorem min_spec_to_min: ∀f.∀n,b,m.
- min_spec n b f m → min n b f = m.
+\ 5img class="anchor" src="icons/tick.png" id="min_spec_to_min"\ 6theorem min_spec_to_min: ∀f.∀n,b,m.
+ \ 5a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"\ 6min_spec\ 5/a\ 6 n b f m → \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m.
#f #n #b #m #spec (cases spec)
- [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
- |#ffalse @min_not_exists @ffalse
+ [#m #lem #ltm #fm #ismin @(\ 5a href="cic:/matita/arithmetics/minimization/min_exists.def(9)"\ 6min_exists\ 5/a\ 6 f (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6b)) // @ismin
+ |#ffalse @\ 5a href="cic:/matita/arithmetics/minimization/min_not_exists.def(9)"\ 6min_not_exists\ 5/a\ 6 @ffalse
]
qed.
-theorem min_to_min_spec: ∀f.∀n,b,m.
- min n b f = m → min_spec n b f m.
+\ 5img class="anchor" src="icons/tick.png" id="min_to_min_spec"\ 6theorem min_to_min_spec: ∀f.∀n,b,m.
+ \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"\ 6min_spec\ 5/a\ 6 n b f m.
#f #n #b #m (cases n)
- [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
+ [#eqm <eqm %2 #i #lei #lti @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … lti) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
|#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
- lapply (le_min_r f (S n) b) >eqm #lem
- (cases (le_to_or_lt_eq … lem)) #mcase
- [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
- |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
+ lapply (\ 5a href="cic:/matita/arithmetics/minimization/le_min_r.def(9)"\ 6le_min_r\ 5/a\ 6 f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) b) >eqm #lem
+ (cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lem)) #mcase
+ [%1 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/minimization/fmin_true.def(7)"\ 6fmin_true\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ #i #H #H1 @(\ 5a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"\ 6lt_min_to_false\ 5/a\ 6 f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) i b) //
+ |>mcase %2 #i #lebi #lti @(\ 5a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"\ 6lt_min_to_false\ 5/a\ 6 f (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) i b) //
]
]
qed.
-theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
- min n b f = min n b g.
+\ 5img class="anchor" src="icons/tick.png" id="min_f_g"\ 6theorem min_f_g: ∀f,g,n,b.(∀i. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b → f i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g i) →
+ \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b g.
#f #g #n (elim n) //
-#m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
-#i #ltib #ltim @ext /2/
+#m #Hind #b #ext normalize >(ext b (\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 b) ?) // >Hind //
+#i #ltib #ltim @ext /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
-min n b g ≤ min n b f.
+\ 5img class="anchor" src="icons/tick.png" id="le_min_f_min_g"\ 6theorem le_min_f_min_g: ∀f,g,n,b.
+ (∀i. b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i → i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6b → f i \ 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 → g i \ 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) →
+ \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b g \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f.
#f #g #n (elim n) //
-#m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq
+#m #Hind #b #ext normalize (cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b))) #Heq >Heq
[>ext //
- |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
- @ext /2/
+ |(cases (g b)) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ @Hind #i #ltb #ltim #fi
+ @ext /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-theorem f_min_true : ∀ f.∀n,b.
-(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
-#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
-#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
+\ 5img class="anchor" src="icons/tick.png" id="f_min_true"\ 6theorem f_min_true : ∀ f.∀n,b.
+(∃i:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 f i \ 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 (\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f) \ 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 #n #b cases(\ 5a href="cic:/matita/arithmetics/minimization/min_to_min_spec.def(10)"\ 6min_to_min_spec\ 5/a\ 6 f n b (\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
+#Hall * #x * * #leb #ltx #fx @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … fx) >Hall /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="lt_min"\ 6theorem lt_min : ∀ f.∀n,b.
+(∃i:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 b \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 i \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 f i \ 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) → \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"\ 6min\ 5/a\ 6 n b f \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
+#f #n #b #H cases H #i * * #lebi #ltin #fi_true
+@(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 … ltin) @\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"\ 6true_to_le_min\ 5/a\ 6 //
qed.
projects / helm.git / blobdiff