(* 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.
include "arithmetics/bounded_quantifiers.ma".
-include "basics/list.ma".
+include "basics/lists/search.ma".
(* A bit of combinatorics *)
interpretation "list membership" 'mem a l = (mem ? a l).
-lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
+\ 5img class="anchor" src="icons/tick.png" id="decidable_mem_nat"\ 6lemma decidable_mem_nat: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀l. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l).
#n #l elim l
- [%2 % @False_ind |#a #tl #Htl @decidable_or //]
+ [%2 % @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 |#a #tl #Htl @\ 5a href="cic:/matita/arithmetics/bounded_quantifiers/decidable_or.def(3)"\ 6decidable_or\ 5/a\ 6 //]
qed.
-lemma length_unique_le: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| ≤ n.
+\ 5img class="anchor" src="icons/tick.png" id="length_unique_le"\ 6lemma length_unique_le: ∀n,l. \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l → (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n) → |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
#n elim n
- [* // #a #tl #_ #H @False_ind @(absurd (a < 0))
- [@H %1 % | @le_to_not_lt //]
- |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
- lapply (length_filter_eqb … m l Huni) #Hle
- @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
- [@le_plus //
- |@le_S_S @Hind
- [@unique_filter //
- |#x #memx cut (x ≤ m)
- [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
- cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
- @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
- @injective_notb @(mem_filter_true ???? memx)
+ [* // #a #tl #_ #H @\ 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 (a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6))
+ [@H %1 % | @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //]
+ |#m #Hind #l #Huni #Hmem <(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l)
+ lapply (\ 5a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"\ 6length_filter_eqb\ 5/a\ 6 … m l Huni) #Hle
+ @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m x) l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 //
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 @Hind
+ [@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
+ |#x #memx cut (x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m)
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Hmem @(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx)] #Hcut
+ cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … Hcut) // #eqxm @\ 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 ? eqxm) @\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx)
]
]
]
qed.
-lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l →
- (∀x. x ∈ l → x ≤ n) → n ∈ l.
-#n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) //
-#H4 @False_ind @(absurd (|l| > n))
+\ 5img class="anchor" src="icons/tick.png" id="eq_length_to_mem"\ 6lemma eq_length_to_mem : ∀n,l. |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l →
+ (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n) → n \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l.
+#n #l #H1 #H2 #H3 cases (\ 5a href="cic:/matita/arithmetics/pidgeon_hole/decidable_mem_nat.def(6)"\ 6decidable_mem_nat\ 5/a\ 6 n l) //
+#H4 @\ 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 (|l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'greater than'" href="cic:/fakeuri.def(1)"\ 6>\ 5/a\ 6 n))
[>H1 //
- |@le_to_not_lt @length_unique_le //
- #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
- #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/pidgeon_hole/length_unique_le.def(9)"\ 6length_unique_le\ 5/a\ 6 //
+ #x #memx cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (H3 x memx)) //
+ #Heq @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H4) #_ <Heq //
]
qed.
-lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l →
- (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
+\ 5img class="anchor" src="icons/tick.png" id="eq_length_to_mem_all"\ 6lemma eq_length_to_mem_all: ∀n,l. |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l →
+ (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n) → ∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → i \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l.
#n elim n
- [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
- |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
- [#leim @(mem_filter… (λi.¬(eqb m i)))
- cases (filter_eqb m … H1)
- [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
- #x #memx @le_S_S_to_le @H2 //]
+ [#l #_ #_ #_ #i #lti0 @\ 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 ? lti0 (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 ?))
+ |#m #Hind #l #H #H1 #H2 #i #lei cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lei)
+ [#leim @(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6… (λi.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m i)))
+ cases (\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"\ 6filter_eqb\ 5/a\ 6 m … H1)
+ [2: * #H @\ 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 ?? H) @\ 5a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"\ 6eq_length_to_mem\ 5/a\ 6 //
+ #x #memx @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H2 //]
* #memm #Hfilter @Hind
- [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
- |@unique_filter @H1
- |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
- [@le_S_S_to_le @H3
- |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
- @injective_notb >(mem_filter_true ???? memx) %
+ [@\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 <H <(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l) >Hfilter %
+ |@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 @H1
+ |#x #memx cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (H2 x (\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx))) #H3
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H3
+ |@\ 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 (m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) [@\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 //] @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 >(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx) %
]
- |@le_S_S_to_le @leim
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @leim
]
- |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
+ |#eqi @\ 5a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"\ 6eq_length_to_mem\ 5/a\ 6 >eqi [@H |@H1 |#x #Hx @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 >eqi @H2 //]
]
]
qed.
-lemma lt_length_to_not_mem: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| < n →
-∃i. i < n ∧ ¬ (i ∈ l).
+\ 5img class="anchor" src="icons/tick.png" id="lt_length_to_not_mem"\ 6lemma lt_length_to_not_mem: ∀n,l. \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l → (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n) → |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
+\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i. 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 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 (i \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l).
#n elim n
- [#l #_ #_ #H @False_ind /2/
- |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
+ [#l #_ #_ #H @\ 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/
+ |#m #Hind #l #Huni #Hmem #Hlen cases (\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"\ 6filter_eqb\ 5/a\ 6 m … Huni)
[2: * #H #_ %{m} % //
- |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
- [#i * #ltim #memi %{i} % [@le_S // ]
- @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
- @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
- |@unique_filter //
- |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
- [#H @le_S_S_to_le @H
- |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
- @injective_notb >(mem_filter_true ???? memx) %
- |@(mem_filter … memx)
+ |* #memm #Hfilter cases (Hind (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx. \ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m x)) l) ? ? ?)
+ [#i * #ltim #memi %{i} % [@\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 // ]
+ @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … memi) @\ 5a href="cic:/matita/basics/lists/search/mem_filter_l.def(4)"\ 6mem_filter_l\ 5/a\ 6 @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 >\ 5a href="cic:/matita/basics/bool/notb_notb.def(2)"\ 6notb_notb\ 5/a\ 6
+ @\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 //
+ |@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
+ |#x #memx cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (Hmem x ?))
+ [#H @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H
+ |#H @\ 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 (m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) [@\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 //] @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 >(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx) %
+ |@(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx)
]
- |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
- @le_S_S_to_le @H
+ |<(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m)) in Hlen; >Hfilter #H
+ @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H
]
]
]
projects / helm.git / commitdiff