[Added ¬∀⟶∃¬ and ¬∀⟶∃¬-smallest. Nils Anders Danielsson **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 +