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

comparison zf.agda @ 213:22d435172d1a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate logic and nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2019 12:17:10 +0900
parents e59e682ad120
children 2e1f19c949dc
comparison
equal deleted inserted replaced
212:0a1804cc9d0a 213:22d435172d1a
1 module zf where 1 module zf where
2 2
3 open import Level 3 open import Level
4 4
5 data Bool : Set where 5 open import logic
6 true : Bool
7 false : Bool
8
9 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
10 field
11 proj1 : A
12 proj2 : B
13
14 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
15 case1 : A → A ∨ B
16 case2 : B → A ∨ B
17
18 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
19 _⇔_ A B = ( A → B ) ∧ ( B → A )
20
21 6
22 open import Relation.Nullary 7 open import Relation.Nullary
23 open import Relation.Binary 8 open import Relation.Binary
24 open import Data.Empty 9 open import Data.Empty
25
26
27 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
28 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
29
30 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ 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 dont-or :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B
41 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
42 dont-or {A} {B} (case2 b) ¬A = b
43
44 dont-orb :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A
45 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
46 dont-orb {A} {B} (case1 a) ¬B = a
47
48 -- mid-ex-neg : {n : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
49 -- mid-ex-neg {n} {A} = {!!}
50
51 infixr 130 _∧_
52 infixr 140 _∨_
53 infixr 150 _⇔_
54 10
55 record IsZF {n m : Level } 11 record IsZF {n m : Level }
56 (ZFSet : Set n) 12 (ZFSet : Set n)
57 (_∋_ : ( A x : ZFSet ) → Set m) 13 (_∋_ : ( A x : ZFSet ) → Set m)
58 (_≈_ : Rel ZFSet m) 14 (_≈_ : Rel ZFSet m)