2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/nat.ma".
14 lemma decidable_not: ∀P. decidable P → decidable (¬P).
15 #P * #H [%2 % * /2/ | /2/]
18 lemma decidable_or: ∀P,Q. decidable P → decidable Q → decidable (P∨Q).
19 #P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /2/]
22 lemma decidable_forall: ∀P. (∀i.decidable (P i))→
23 ∀n.decidable (∀i. i < n → P i).
25 [%1 #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
28 [%1 #i #lei0 cases (le_to_or_lt_eq … lei0) #H1
29 [@H @le_S_S_to_le @H1 |>(injective_S … H1) @HPm]
30 |%2 @(not_to_not … HPm) #H1 @H1 //
32 |%2 @(not_to_not … H) #H1 #i #leim @H1 @le_S //
37 lemma not_exists_to_forall: ∀P,n.
38 ¬(∃i. i < n ∧ P i) → ∀i. i < n → ¬ P i.
40 [#_ #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
41 |#m #Hind #H1 #i #leiS cases (le_to_or_lt_eq … leiS) #H2
42 [@(Hind … (le_S_S_to_le … H2)) @(not_to_not … H1) *
43 #a * #leam #Pa %{a} % // @le_S //
44 |@(not_to_not … H1) #Pi %{i} % //
49 lemma not_forall_to_exists: ∀P,n. (∀i.decidable (P i)) →
50 ¬(∀i. i < n → P i) → (∃i. i < n ∧ ¬ (P i)).
52 [* #H @False_ind @H #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
53 |#m #Hind #H1 cases (decP m) #H2
55 [#i * #leim #nPi %{i} % // @le_S //
56 |@(not_to_not … H1) #H3 #i #leiS cases (le_to_or_lt_eq … leiS)
57 [#ltiS @H3 @le_S_S_to_le // |#eqi //]