matita/matita/lib/arithmetics/bounded_quantifiers.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 lemma decidable_not: ∀P. decidable P → decidable (¬P).
  15 #P * #H [%2 % * /2/ | /2/]
  16 qed.
  17
  18 lemma decidable_or: ∀P,Q. decidable P → decidable Q → decidable (P∨Q).
  19 #P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /2/]
  20 qed.
  21
  22 lemma decidable_forall: ∀P. (∀i.decidable (P i))→
  23   ∀n.decidable (∀i. i < n → P i).
  24 #P #Hdec #n elim n
  25   [%1 #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
  26   |#m * #H
  27     [cases (Hdec m) #HPm
  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 //
  31       ]
  32     |%2 @(not_to_not … H) #H1 #i #leim @H1 @le_S //
  33     ]
  34   ]
  35 qed.
  36
  37 lemma not_exists_to_forall: ∀P,n.
  38   ¬(∃i. i < n ∧ P i) → ∀i. i < n → ¬ P i.
  39 #P #n elim n
  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} % //
  45     ]
  46   ]
  47 qed.
  48
  49 lemma not_forall_to_exists: ∀P,n. (∀i.decidable (P i)) →
  50   ¬(∀i. i < n → P i) → (∃i. i < n ∧ ¬ (P i)).
  51 #P #n #decP elim n
  52   [* #H @False_ind @H #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt //
  53   |#m #Hind #H1 cases (decP m) #H2
  54     [cases (Hind ?)
  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 //]
  58       ]
  59     |%{m} % //
  60     ]
  61   ]
  62 qed.