--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/negnat.agda	Tue Feb 28 12:38:23 2017 +0900
@@ -0,0 +1,169 @@
+
+
+module negnat where
+
+
+open import Data.Nat
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Unit
+open import Data.Fin renaming ( suc to fsuc ; zero to fzero ; _+_ to _++_ )
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+
+
+--  http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda
+
+
+ℕ-elim : ∀ {p} (P : ℕ → Set p)
+  (s : ∀ {n} → P n → P (suc n))
+  (z : P 0) → ∀ n → P n
+ℕ-elim P s z zero    = z
+ℕ-elim P s z (suc n) = s (ℕ-elim P s z n)
+
+-- peano : ∀ n → suc n ≡ zero → ⊥
+
+Nope : (m n : ℕ) → Set
+Nope (suc _) zero = ⊥
+Nope _    _       = ⊤
+
+nope : ∀ m n → m ≡ n → Nope m n
+nope zero    ._ refl = _
+nope (suc m) ._ refl = _
+
+peano : ∀ n → suc n ≡ zero → ⊥
+peano _ p = nope _ _ p
+
+
+J : ∀ {a p} {A : Set a} (P : ∀ (x : A) y → x ≡ y → Set p)
+  (f : ∀ x → P x x refl) → ∀ x y → (p : x ≡ y) → P x y p
+J P f x .x refl = f x
+
+Fin-elim : ∀ {p} (P : ∀ n → Fin n → Set p)
+  (s : ∀ {n} {fn : Fin n} → P n fn → P (suc n) (fsuc fn))
+  (z : ∀ {n} → P (suc n) fzero) →
+  ∀ {n} (fn : Fin n) → P n fn
+Fin-elim P s z fzero    = z
+Fin-elim P s z (fsuc x) = s (Fin-elim P s z x)
+
+Nope0 : ℕ → Set
+Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥
+
+-- Nope1 zero    = ⊥
+-- Nope1 (suc _) = ⊤
+
+bad : Fin 0 → ⊥
+bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _
+
+
+--  http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type
+
+even : ℕ -> Set
+even zero = ⊤
+even (suc zero) =  ⊥
+even (suc (suc n)) = even n
+
+div : (n :  ℕ) -> even n ->  ℕ
+div zero p = zero
+div (suc (suc n)) p = suc (div n p)
+div (suc zero) () 
+
+proof : (suc (suc zero) + (suc (suc (suc zero)))) ≡ (suc (suc (suc (suc (suc zero)))))
+proof = refl
+
+-- data ⊥ : Set where
+--
+-- ¬_ : Set → Set
+-- ¬ A = A → ⊥
+--
+-- data Dec (P : Set) : Set where
+--   yes :   P → Dec P
+--   no  : ¬ P → Dec P
+
+EvenDecidable : Set
+EvenDecidable = ∀ n → Dec (even n)
+
+isEven : EvenDecidable
+isEven zero          = yes _
+isEven (suc zero)    = no λ ()
+isEven (suc (suc n)) = isEven n
+
+data Bool : Set where
+  true false : Bool
+
+if_then_else_ : {A : Set} → Bool → A → A → A
+if true  then t else _ = t
+if false then _ else f = f
+
+⌊_⌋ : {P : Set} → Dec P → Bool
+⌊ yes _ ⌋ = true
+⌊ no  _ ⌋ = false
+
+bad1 : ∀ n → even n → even (suc n) → ⊥
+bad1 zero          p q = q
+bad1 (suc zero)    p q = p
+bad1 (suc (suc n)) p q = bad1 n p q
+
+odd : ∀ n → ¬ even n → even (suc n)
+odd zero          p = p _
+odd (suc zero)    p = _
+odd (suc (suc n)) p = odd n p
+
+g : ℕ → ℕ
+g n with isEven n
+... | yes e = div n e
+... | no  o = div (suc n) (odd n o)
+
+-- g-bad : ℕ → ℕ
+-- g-bad n = if  ⌊ isEven n  ⌋
+--   then (div n {!!})
+--   else (div (suc n) (odd n {!!}))
+
+
+if-dec_then_else_ : {P A : Set} → Dec P → (P → A) → (¬ P → A) → A
+if-dec yes p then t else _ = t  p
+if-dec no ¬p then _ else f = f ¬p
+
+g' : ℕ → ℕ
+g' n = if-dec isEven n
+  then (λ e → div n e)
+  else (λ o → div (suc n) (odd n o))
+
+if-syntax = if-dec_then_else_
+
+syntax if-syntax dec (λ yup → yupCase) (λ nope → nopeCase)
+  = if-dec dec then[ yup ] yupCase else[ nope ] nopeCase
+
+g'' : ℕ → ℕ
+g'' n = if-dec isEven n
+  then[ e ] div n e
+  else[ o ] div (suc n) (odd n o)
+
+
+mod :  ℕ  ->  ℕ 
+mod zero = zero
+mod (suc zero) = suc zero
+mod (suc (suc N)) = mod N
+
+lemma1 : { n :  ℕ } -> mod (suc (suc n ))  ≡  mod n
+lemma1 = refl
+
+lemma2 : { n :  ℕ } -> isEven (suc (suc n ))  ≡  isEven n
+lemma2 = refl
+
+
+proof1 : (n :  ℕ ) -> ( if ⌊ isEven n ⌋  then zero else (suc zero)  )  ≡ ( mod n )
+proof1 zero =  refl
+proof1 (suc zero) = refl
+proof1 (suc (suc n)) =   let open ≡-Reasoning in 
+   begin 
+        if ⌊ isEven (suc (suc n)) ⌋ then zero else suc zero
+   ≡⟨ cong ( \x -> (if ⌊ x ⌋ then zero else suc zero)) (lemma2 {n} )⟩
+        if ⌊ isEven  n ⌋ then zero else suc zero
+   ≡⟨ proof1 n ⟩
+       mod n
+   ≡⟨ sym (lemma1 {n}) ⟩
+       mod (suc (suc n))
+   ∎
+
+