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

annotate LEMC.agda @ 283:2d77b6d12a22

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 Sun, 10 May 2020 00:18:59 +0900
parents 6630dab08784
children a8f9c8a27e8d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
1 open import Level
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
2 open import Ordinals
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
3 open import logic
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
4 open import Relation.Nullary
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
5 module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
7 open import zf
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
9 open import Relation.Binary.PropositionalEquality
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
10 open import Data.Nat.Properties
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
14
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
15 open import nat
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
16 import OD
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
17
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
18 open inOrdinal O
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
19 open OD O
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
20 open OD.OD
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
21 open OD._==_
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
22 open ODAxiom odAxiom
119
6e264c78e420 infinite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
23
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
24 open import zfc
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
25
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
26 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
27 ---
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
28 record choiced ( X : OD) : Set (suc n) where
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
29 field
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
30 a-choice : OD
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
31 is-in : X ∋ a-choice
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
32
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
33 open choiced
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
34
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
35 OD→ZFC : ZFC
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
36 OD→ZFC = record {
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
37 ZFSet = OD
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
38 ; _∋_ = _∋_
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
39 ; _≈_ = _==_
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
40 ; ∅ = od∅
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
41 ; Select = Select
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
42 ; isZFC = isZFC
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
43 } where
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
44 -- infixr 200 _∈_
96
f239ffc27fd0 Power Set and L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
45 -- infixr 230 _∩_ _∪_
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
46 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
47 isZFC = record {
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
48 choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
49 choice = λ A {X} A∋X not → is-in (choice-func X not)
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
50 } where
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
51 choice-func : (X : OD ) → ¬ ( X == od∅ ) → choiced X
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
52 choice-func X not = have_to_find where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
53 ψ : ( ox : Ordinal ) → Set (suc n)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
54 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
55 lemma-ord : ( ox : Ordinal ) → ψ ox
235
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
56 lemma-ord ox = TransFinite {ψ} induction ox where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
57 ∋-p : (A x : OD ) → Dec ( A ∋ x )
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
58 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
59 ∋-p A x | case1 (lift t) = yes t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
60 ∋-p A x | case2 t = no (λ x → t (lift x ))
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
61 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
62 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
63 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
64 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
65 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
66 lemma : ¬ ((x : Ordinal ) → A x) → B
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
67 lemma not with p∨¬p B
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
68 lemma not | case1 b = b
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
69 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
70 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
71 induction x prev with ∋-p X ( ord→od x)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
72 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
73 ... | no ¬p = lemma where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
74 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
75 lemma1 y with ∋-p X (ord→od y)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
76 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
77 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
78 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
79 lemma = ∀-imply-or lemma1
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
80 have_to_find : choiced X
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
81 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
82 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
83 ¬¬X∋x nn = not record {
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
84 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
85 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
86 }
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
87 record Minimal (x : OD) (ne : ¬ (x == od∅ ) ) : Set (suc n) where
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
88 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
89 min : OD
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
90 x∋min : x ∋ min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
91 min-empty : (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
92 open Minimal
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
93 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
94 induction : {x : OD} → ({y : OD} → x ∋ y → (ne : ¬ (y == od∅ )) → Minimal y ne ) → (ne : ¬ (x == od∅ )) → Minimal x ne
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
95 induction {x} prev ne = c2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
96 where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
97 ch : choiced x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
98 ch = choice-func x ne
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 279
diff changeset
99 c1 : OD
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
100 c1 = a-choice ch -- x ∋ c1
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
101 c2 : Minimal x ne
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
102 c2 with p∨¬p ( (y : OD ) → ¬ ( def c1 (od→ord y) ∧ (def x (od→ord y))) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
103 c2 | case1 Yes = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
104 min = c1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
105 ; x∋min = is-in ch
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
106 ; min-empty = Yes
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
107 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
108 c2 | case2 No = c3 where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
109 y1 : OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
110 y1 = record { def = λ y → ( def c1 y ∧ def x y) }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
111 noty1 : ¬ (y1 == od∅ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
112 noty1 not = ⊥-elim ( No (λ z n → ∅< n not ) )
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
113 ch1 : choiced y1 -- a-choice ch1 ∈ c1 , a-choice ch1 ∈ x
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
114 ch1 = choice-func y1 noty1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
115 c3 : Minimal x ne
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
116 c3 with is-o∅ (od→ord (a-choice ch1))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
117 ... | yes eq = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
118 min = od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
119 ; x∋min = def-subst {x} {od→ord (a-choice ch1)} {x} (proj2 (is-in ch1)) refl (trans eq (sym ord-od∅) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
120 ; min-empty = λ z p → ⊥-elim ( ¬x<0 (proj1 p) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
121 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
122 ... | no n = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
123 min = min min3
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
124 ; x∋min = x∋min3 (x∋min min3)
282
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
125 ; min-empty = min3-empty -- λ y p → min3-empty min3 y p -- p : (min min3 ∋ y) ∧ (x ∋ y)
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
126 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
127 lemma : (a-choice ch1 == od∅ ) → od→ord (a-choice ch1) ≡ o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
128 lemma eq = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
129 od→ord (a-choice ch1)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
130 ≡⟨ cong (λ k → od→ord k ) (==→o≡ eq ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
131 od→ord od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
132 ≡⟨ ord-od∅ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
133 o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
134 ∎ where open ≡-Reasoning
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
135 -- Minimal (a-choice ch1) ch1not
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
136 -- min ∈ a-choice ch1 , min ∩ a-choice ch1 ≡ ∅
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
137 ch1not : ¬ (a-choice ch1 == od∅)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
138 ch1not ch1=0 = n (lemma ch1=0)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
139 min3 : Minimal (a-choice ch1) ch1not
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
140 min3 = prev (proj2 (is-in ch1)) (λ ch1=0 → n (lemma ch1=0))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
141 x∋min3 : a-choice ch1 ∋ min min3 → x ∋ min min3
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
142 x∋min3 lt = {!!}
282
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
143 min3-empty : (y : OD ) → ¬ ((min min3 ∋ y) ∧ (x ∋ y))
283
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 282
diff changeset
144 min3-empty y p = min-empty min3 y record { proj1 = proj1 p ; proj2 = ? } -- (min min3 ∋ y) ∧ (a-choice ch1 ∋ y)
282
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 281
diff changeset
145 -- p : (min min3 ∋ y) ∧ (x ∋ y)
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
146
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
147
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
148 Min1 : (x : OD) → (ne : ¬ (x == od∅ )) → Minimal x ne
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
149 Min1 x ne = (ε-induction {λ y → (ne : ¬ (y == od∅ ) ) → Minimal y ne } induction x ne )
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
150 minimal : (x : OD ) → ¬ (x == od∅ ) → OD
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
151 minimal x not = min (Min1 x not )
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
152 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
153 x∋minimal x ne = x∋min (Min1 x ne)
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
154 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
281
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 280
diff changeset
155 minimal-1 x ne y = min-empty (Min1 x ne ) y
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
156
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
157
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
158
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
159