Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 188:1f2c8b094908
axiom of choice → p ∨ ¬ p
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 25 Jul 2019 13:11:21 +0900 |
parents | 914cc522c53a |
children | 64ef1db53c49 |
line wrap: on
line diff
--- a/zf.agda Tue Jul 23 11:08:24 2019 +0900 +++ b/zf.agda Thu Jul 25 13:11:21 2019 +0900 @@ -21,6 +21,8 @@ open import Relation.Nullary open import Relation.Binary +open import Data.Empty + contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) @@ -28,6 +30,16 @@ double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A double-neg A notnot = notnot A +double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A +double-neg2 notnot A = notnot ( double-neg A ) + +de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) ) +de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) +de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) + +-- mid-ex-neg : {n : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A) +-- mid-ex-neg {n} {A} = {!!} + infixr 130 _∧_ infixr 140 _∨_ infixr 150 _⇔_