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

changeset 208:64ef1db53c49

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 01 Aug 2019 08:28:20 +0900
parents 3e4eb4da1453
children e59e682ad120
files OD.agda zf.agda
diffstat 2 files changed, 10 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Thu Aug 01 00:13:07 2019 +0900
+++ b/OD.agda	Thu Aug 01 08:28:20 2019 +0900
@@ -567,18 +567,18 @@
          choice-func' X ∋-p not = have_to_find 
            where
             ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
-            ψ ox = ( x : Ordinal {suc n}) → x o< ox  → ¬ (def X x ) ∨ choiced X
+            ψ ox = ( x : Ordinal {suc n}) → x o< ox  → ( ¬ def X x ) ∨ choiced X
             lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
             lemma-ord  ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where
                caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) 
                caseΦ lx prev with ∋-p X ( ord→od (ordinal lx (Φ lx) ))
-               caseΦ lx prev | yes p = ? -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
-               caseΦ lx prev | no ¬p = ?
+               caseΦ lx prev | yes p = {!!} -- case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
+               caseΦ lx prev | no ¬p = {!!}
                caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
                caseOSuc lx x prev with ∋-p X (ord→od record { lv = lx ; ord = x } )
-               caseOSuc lx x prev | yes p = ? -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
-               caseOSuc lx x prev | no ¬p =  ?
+               caseOSuc lx x prev | yes p = {!!} -- case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
+               caseOSuc lx x prev | no ¬p =  {!!}
             have_to_find : choiced X
             have_to_find with lemma-ord (od→ord X )
-            have_to_find | t = ?
+            have_to_find | t = dont-or ( t (od→ord X) {!!} ) {!!}
 
--- a/zf.agda	Thu Aug 01 00:13:07 2019 +0900
+++ b/zf.agda	Thu Aug 01 08:28:20 2019 +0900
@@ -37,6 +37,10 @@
 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
+
 -- mid-ex-neg : {n  : Level } {A : Set n} → ( ¬ ¬ A ) ∨ (¬ A)
 -- mid-ex-neg {n} {A} = {!!}