Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison zf.agda @ 188:1f2c8b094908

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
187:ac872f6b8692 188:1f2c8b094908
19 _⇔_ A B = ( A → B ) ∧ ( B → A ) 19 _⇔_ A B = ( A → B ) ∧ ( B → A )
20 20
21 21
22 open import Relation.Nullary 22 open import Relation.Nullary
23 open import Relation.Binary 23 open import Relation.Binary
24 open import Data.Empty
25
24 26
25 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 27 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
26 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) 28 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
27 29
28 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A 30 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
29 double-neg A notnot = notnot A 31 double-neg A notnot = notnot A
32
33 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
34 double-neg2 notnot A = notnot ( double-neg A )
35
36 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
37 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
38 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
39
40 -- mid-ex-neg : {n : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
41 -- mid-ex-neg {n} {A} = {!!}
30 42
31 infixr 130 _∧_ 43 infixr 130 _∧_
32 infixr 140 _∨_ 44 infixr 140 _∨_
33 infixr 150 _⇔_ 45 infixr 150 _⇔_
34 46