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

changeset 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 0a1804cc9d0a
children e05575588191
files OD.agda logic.agda nat.agda ordinal.agda zf.agda
diffstat 5 files changed, 103 insertions(+), 81 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Thu Aug 01 15:38:08 2019 +0900
+++ b/OD.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -11,6 +11,9 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
+open import logic
+open import nat
+
 -- Ordinal Definable Set
 
 record OD {n : Level}  : Set (suc n) where
@@ -21,6 +24,8 @@
 
 open Ordinal
 open _∧_
+open _∨_
+open Bool
 
 record _==_ {n : Level} ( a b :  OD {n} ) : Set n where
   field
@@ -155,9 +160,6 @@
 o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
 o≡→== {n} {x} {.x} refl = eq-refl
 
->→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
->→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
-
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -0,0 +1,50 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+
+data Bool : Set where
+   true : Bool
+   false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+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 )
+
+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 ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nat.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -0,0 +1,40 @@
+module nat where
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Empty
+open import Relation.Nullary
+open import  Relation.Binary.PropositionalEquality
+open import  logic
+
+
+nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+
+nat-<≡ : { x : Nat } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
+
+a<sa : {la : Nat} → la < Suc la 
+a<sa {Zero} = s≤s z≤n
+a<sa {Suc la} = s≤s a<sa 
+
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
+<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {Suc x} {Zero} (s≤s ())
+<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
+<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+
--- a/ordinal.agda	Thu Aug 01 15:38:08 2019 +0900
+++ b/ordinal.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -7,6 +7,8 @@
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
 open import  Relation.Binary.PropositionalEquality
+open import  logic
+open import  nat
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
@@ -100,34 +102,6 @@
 osucc {n} {ox} {oy} (case2 x) with d<→lv x
 ... | refl = case2 (s< x)
 
-nat-<> : { x y : Nat } → x < y → y < x → ⊥
-nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
-
-nat-<≡ : { x : Nat } → x < x → ⊥
-nat-<≡  (s≤s lt) = nat-<≡ lt
-
-nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
-nat-≡< refl lt = nat-<≡ lt
-
-¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
-¬a≤a  (s≤s lt) = ¬a≤a  lt
-
-a<sa : {la : Nat} → la < Suc la 
-a<sa {Zero} = s≤s z≤n
-a<sa {Suc la} = s≤s a<sa 
-
-=→¬< : {x : Nat  } → ¬ ( x < x )
-=→¬< {Zero} ()
-=→¬< {Suc x} (s≤s lt) = =→¬< lt
-
-<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
-<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
-<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
-<-∨ {Suc x} {Zero} (s≤s ())
-<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
-<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
-<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
-
 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
 ... | refl = nat-≡< refl lt1
@@ -344,11 +318,11 @@
       lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
       lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
       lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
-      lemma lx1 ox1 (case1 lt) with <-∨ lt
-      lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
-      lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa)) 
-      lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0  lx (Φ lx) (case1 (s≤s lt1))
-      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 
+      lemma lx1 ox1            (case1 lt) with <-∨ lt
+      lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
+      lemma lx (Φ lx)          (case1 lt) | case2 (s≤s lt1) = lemma0  lx (Φ lx) (case1 (s≤s lt1))
+      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1  ( lemma lx ox1 (case1 a<sa)) 
+      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1  = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 
   TransFinite1 lx (OSuc lx ox)  = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )}
 
 -- we cannot prove this in intutionistic logic 
--- a/zf.agda	Thu Aug 01 15:38:08 2019 +0900
+++ b/zf.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -2,56 +2,12 @@
 
 open import Level
 
-data Bool : Set where
-   true : Bool
-   false : Bool
-
-record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
-   field 
-      proj1 : A
-      proj2 : B
-
-data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
-   case1 : A → A ∨ B
-   case2 : B → A ∨ B
-
-_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
-_⇔_ A B =  ( A → B ) ∧ ( B → A )
-
+open import logic
 
 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 ) 
-
-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 ))
-
-dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
-dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
-dont-or {A} {B} (case2 b) ¬A = b
-
-dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
-dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
-dont-orb {A} {B} (case1 a) ¬B = a
-
--- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
--- mid-ex-neg {n} {A} = {!!}
-
-infixr  130 _∧_
-infixr  140 _∨_
-infixr  150 _⇔_
-
 record IsZF {n m : Level }
      (ZFSet : Set n)
      (_∋_ : ( A x : ZFSet  ) → Set m)