[Added ¬∀⟶∃¬ and ¬∀⟶∃¬-smallest.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20090120172256] hunk ./Data/Fin/Dec.agda 8
-open import Data.Nat
+open import Data.Nat hiding (_<_)
hunk ./Data/Fin/Dec.agda 13
-open import Data.Product
+open import Data.Product as Prod
hunk ./Data/Fin/Dec.agda 16
-open import Relation.Nullary.Negation
+open import Relation.Unary using (Pred)
hunk ./Data/Fin/Dec.agda 48
-  helper (suc f , p') = contradiction (_ , p') ¬p'
+  helper (suc f , p') = ¬p' (_ , p')
hunk ./Data/Fin/Dec.agda 81
-    hlpr zero    q₀ = contradiction q₀ ¬q₀
+    hlpr zero    q₀ = ⊥-elim (¬q₀ q₀)
hunk ./Data/Fin/Dec.agda 130
+
+-- If a decidable predicate P over a finite set is sometimes false,
+-- then we can find the smallest value for which this is the case.
+
+¬∀⟶∃¬-smallest :
+  ∀ n (P : Pred (Fin n)) → (∀ i → Dec (P i)) →
+  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin (toℕ i)) → P (inject j))
+¬∀⟶∃¬-smallest zero    P dec ¬∀iPi = ⊥-elim (¬∀iPi (λ()))
+¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi with dec zero
+¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | no ¬P0 = (zero , ¬P0 , λ ())
+¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | yes P0 =
+  Prod.map suc (Prod.map id extend′) $
+    ¬∀⟶∃¬-smallest n (λ n → P (suc n)) (dec ∘ suc) (¬∀iPi ∘ extend)
+  where
+  extend : (∀ i → P (suc i)) → (∀ i → P i)
+  extend ∀iP[1+i] zero    = P0
+  extend ∀iP[1+i] (suc i) = ∀iP[1+i] i
+
+  extend′ : ∀ {i : Fin n} →
+            ((j : Fin (toℕ i)) → P (suc (inject j))) →
+            ((j : Fin (suc (toℕ i))) → P (inject j))
+  extend′ g zero    = P0
+  extend′ g (suc j) = g j
hunk ./Data/Fin/Subset/Props.agda 14
-open import Relation.Nullary.Negation
hunk ./Data/Fin/Subset/Props.agda 61
-  contradiction (zero , here) ¬¬∅
+  ⊥-elim (¬¬∅ (zero , here))
hunk ./Relation/Nullary/Negation.agda 11
-open import Data.Product
+open import Data.Product as Prod
+open import Data.Fin
+open import Data.Fin.Dec
hunk ./Relation/Nullary/Negation.agda 46
+-- When P is a decidable predicate over a finite set the following
+-- lemma can be proved.
+
+¬∀⟶∃¬ : ∀ n (P : Pred (Fin n)) → (∀ i → Dec (P i)) →
+        ¬ (∀ i → P i) → ∃ λ i → ¬ P i
+¬∀⟶∃¬ n P dec ¬P = Prod.map id proj₁ $ ¬∀⟶∃¬-smallest n P dec ¬P
+