Mercurial > hg > Members > kono > Proof > category

changeset 451:3ee32e4df4c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add negation example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Feb 2017 12:38:23 +0900
parents e9ece23ab94e
children 7ed0045e4adf
files discrete.agda negnat.agda
diffstat 2 files changed, 174 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Mon Feb 27 21:20:34 2017 +0900
+++ b/discrete.agda	Tue Feb 28 12:38:23 2017 +0900
@@ -34,10 +34,10 @@
 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set ( c₂)  where
    field
        hom   :  Maybe ( Arrow {c₁} {c₂} a b )
-   constraint1 :  {c₁ c₂ : Level } → TwoObject {c₁}  → TwoObject {c₁} → Maybe ( TwoObject {c₁} -> Set   )
+   constraint1 :  {c₁ c₂ : Level } → TwoObject {c₁}  → TwoObject {c₁} → Maybe (  ⊥   )
    constraint1 t0 t0  = nothing
-   constraint1 {c₁} {c₂} t0 t1  = just ( \ (X : TwoObject   {c₁} ) ->  ⊥  )
-   constraint1 t1 t0  = nothing
+   constraint1 {c₁} {c₂} t1 t0  = just ( {!!}  )
+   constraint1 t0 t1  = nothing
    constraint1 t1 t1  = nothing
 
 comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  Maybe ( Arrow {c₁} {c₂} b c ) →  Maybe ( Arrow {c₁} {c₂} a b )  →  Maybe ( Arrow {c₁} {c₂} a c )
@@ -185,7 +185,8 @@
    }  where
         identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  == hom f
         identityL  {c₁}  {c₂}  {a} {b} {f}  with hom f | constraint1 f a b
-        identityL  {c₁}  {c₂}  {a} {_} {f} | _  | just C = ⊥-elim C
+        identityL  {c₁}  {c₂}  {t1} {t0} {f} | _  | just C = ⊥-elim C
+        identityL  {c₁}  {c₂}  {t1} {t0} {_} | just _ | nothing = {!!}
         identityL  {c₁}  {c₂}  {t0} {t0} {_} | nothing  | _ = nothing
         identityL  {c₁}  {c₂}  {t0} {t1} {_} | nothing  | _ = nothing
         identityL  {c₁}  {c₂}  {t1} {t0} {_} | nothing  | _ = nothing
@@ -194,7 +195,6 @@
         identityL  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 | _ = ==refl
         identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f | _ = ==refl
         identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g | _ = ==refl
-        identityL  {c₁}  {c₂}  {t1} {t0} {_} | just _ | _ = ⊥-elim {!!}
         identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  == hom f
         identityR  {c₁}  {c₂}  {_} {_} {f}  with hom f
         identityR  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing 
--- /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))
+   ∎
+
+