← Back to branch summary

~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Data/Nat/InfinitelyOften.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/InfinitelyOften.agda
 
1
------------------------------------------------------------------------
 
2
-- Definition of and lemmas related to "true infinitely often"
 
3
------------------------------------------------------------------------
 
4
 
 
5
module Data.Nat.InfinitelyOften where
 
6
 
 
7
open import Algebra
 
8
open import Category.Monad
 
9
open import Data.Empty
 
10
open import Data.Function
 
11
open import Data.Nat
 
12
import Data.Nat.Properties as NatProp
 
13
open import Data.Product as Prod hiding (map)
 
14
open import Data.Sum hiding (map)
 
15
open import Relation.Binary.PropositionalEquality
 
16
open import Relation.Nullary
 
17
open import Relation.Nullary.Negation
 
18
open import Relation.Unary using (_∪_; _⊆_)
 
19
open RawMonad ¬¬-Monad
 
20
private
 
21
  module NatLattice = DistributiveLattice NatProp.distributiveLattice
 
22
 
 
23
-- Only true finitely often.
 
24
 
 
25
Fin : (ℕ → Set) → Set
 
26
Fin P = ∃ λ i → ∀ j → i ≤ j → ¬ P j
 
27
 
 
28
-- Fin is preserved by binary sums.
 
29
 
 
30
_∪-Fin_ : ∀ {P Q} → Fin P → Fin Q → Fin (P ∪ Q)
 
31
_∪-Fin_ {P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
 
32
  where
 
33
  open ≤-Reasoning
 
34
 
 
35
  helper : ∀ k → i ⊔ j ≤ k → ¬ (P ∪ Q) k
 
36
  helper k i⊔j≤k (inj₁ p) = ¬p k (begin
 
37
    i      ≤⟨ NatProp.m≤m⊔n i j ⟩
 
38
    i ⊔ j  ≤⟨ i⊔j≤k ⟩
 
39
    k      ∎) p
 
40
  helper k i⊔j≤k (inj₂ q) = ¬q k (begin
 
41
    j      ≤⟨ NatProp.m≤m⊔n j i ⟩
 
42
    j ⊔ i  ≡⟨ NatLattice.∧-comm j i ⟩
 
43
    i ⊔ j  ≤⟨ i⊔j≤k ⟩
 
44
    k      ∎) q
 
45
 
 
46
-- A non-constructive definition of "true infinitely often".
 
47
 
 
48
Inf : (ℕ → Set) → Set
 
49
Inf P = ¬ Fin P
 
50
 
 
51
-- Inf commutes with binary sums (in the double-negation monad).
 
52
 
 
53
commutes-with-∪ : ∀ {P Q} → Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
 
54
commutes-with-∪ p∪q =
 
55
  call/cc λ ¬[p⊎q] →
 
56
  (λ ¬p ¬q → ⊥-elim (p∪q (¬p ∪-Fin ¬q)))
 
57
    <$> ¬[p⊎q] ∘ inj₁ ⊛ ¬[p⊎q] ∘ inj₂
 
58
 
 
59
-- Inf is functorial.
 
60
 
 
61
map : ∀ {P Q} → P ⊆ Q → Inf P → Inf Q
 
62
map P⊆Q ¬fin = ¬fin ∘ Prod.map id (λ fin j i≤j → fin j i≤j ∘ P⊆Q)
 
63
 
 
64
-- Inf is upwards closed.
 
65
 
 
66
up : ∀ {P} n → Inf P → Inf (P ∘ _+_ n)
 
67
up     zero    = id
 
68
up {P} (suc n) = up n ∘ up₁
 
69
  where
 
70
  up₁ : Inf P → Inf (P ∘ suc)
 
71
  up₁ ¬fin (i , fin) = ¬fin (suc i , helper)
 
72
    where
 
73
    helper : ∀ j → 1 + i ≤ j → ¬ P j
 
74
    helper ._ (s≤s i≤j) = fin _ i≤j
 
75
 
 
76
-- A witness.
 
77
 
 
78
witness : ∀ {P} → Inf P → ¬ ¬ ∃ P
 
79
witness ¬fin ¬p = ¬fin (0 , λ i _ Pi → ¬p (i , Pi))
 
80
 
 
81
-- Two different witnesses.
 
82
 
 
83
twoDifferentWitnesses
 
84
  : ∀ {P} → Inf P → ¬ ¬ ∃₂ λ m n → m ≢ n × P m × P n
 
85
twoDifferentWitnesses inf =
 
86
  witness inf                     >>= λ w₁ →
 
87
  witness (up (1 + proj₁ w₁) inf) >>= λ w₂ →
 
88
  return (_ , _ , NatProp.m≢1+m+n (proj₁ w₁) , proj₂ w₁ , proj₂ w₂)