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

changeset 1289:95b62a08c3d0

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 Mon, 29 May 2023 09:29:28 +0900
parents 29dcea36a182
children 8bf6db0b82df
files src/OD.agda
diffstat 1 files changed, 35 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/OD.agda	Sun May 28 21:15:53 2023 +0900
+++ b/src/OD.agda	Mon May 29 09:29:28 2023 +0900
@@ -472,25 +472,48 @@
 infinite-od : OD
 infinite-od = record { def = λ x → infinite-d x } 
 
-nat-Ord : {x : Ordinal} → infinite-d x → (Union (* x , (* x , * x ))) ≡ Ord (osuc x)
-nat-Ord {.(Ordinals.o∅ O)} iφ = ==→o≡ record { eq→ = lemma10 ; eq← = ? } where
+nat=Ord : {x : Ordinal} → infinite-d x → (Union (* x , (* x , * x ))) ≡ Ord (osuc x)
+nat=Ord {.(Ordinals.o∅ O)} iφ = ==→o≡ record { eq→ = lemma10 ; eq← = lemma11 } where
        lemma10 : {x : Ordinal} → Own (* o∅ , (* o∅ , * o∅)) x → x o< osuc o∅
-       lemma10 {x} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ?
+       lemma10 {x} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ⊥-elim (o<¬≡ (sym &iso) (∈∅< lemma4)) where
+             lemma4 : odef (* o∅) x
+             lemma4 = subst (λ k → odef k x) (trans (cong (*) eq) *iso )  ox
        lemma10 {x} record { owner = owner ; ao = (case2 eq) ; ox = ox } with (subst (λ k → odef k x) (trans (cong (*) eq) *iso )  ox)
-       ... | case1 eq1 = ?
-       ... | case2 eq1 = ?
+       ... | case1 eq1 = subst (λ k → k o< osuc o∅) (trans (sym &iso) (sym eq1) ) <-osuc
+       ... | case2 eq1 = subst (λ k → k o< osuc o∅) (trans (sym &iso) (sym eq1) ) <-osuc
        lemma11 : {x : Ordinal} → x o< osuc o∅ → Own (* o∅ , (* o∅ , * o∅)) x 
-       lemma11 {x} lt = record { owner = _ ; ao = case2 refl ; ox = ? } 
-nat-Ord {.(& (Union (* x , (* x , * x))))} (isuc {x} it) = ==→o≡ record { eq→ = ? ; eq← = ? } where
+       lemma11 {x} lt with osuc-≡< lt
+       ... | case1 eq = record { owner = _ ; ao = case2 refl ; ox = subst (λ k → odef k x) (sym *iso) (case1 (trans eq (sym &iso))) } 
+       ... | case2 x<0 = ⊥-elim (¬x<0 x<0)
+nat=Ord {.(& (Union (* x , (* x , * x))))} (isuc {x} it) = ==→o≡ record { eq→ = lemma12 ; eq← = lemma14 } where
        lemma12 : {z : Ordinal} →
             Own (* (& (Union (* x , (* x , * x)))) , (* (& (Union (* x , (* x , * x)))) , * (& (Union (* x , (* x , * x)))))) z →
             z o< osuc (& (Union (* x , (* x , * x))))
-       lemma12 {z} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ? where
-           lemma13 : ?
-           lemma13 = ?
+       lemma12 {z} record { owner = owner ; ao = (case1 eq) ; ox = ox } = ordtrans lemma13 <-osuc where
+           lemma15 : odef (* (& (Union (* x , (* x , * x))))) z
+           lemma15 = subst (λ k → odef k z) (trans (cong (*) eq) *iso )  ox 
+           lemma13 : z o< & (Union (* x , (* x , * x)))
+           lemma13 = subst₂ (λ j k → j o< k) &iso refl ( c<→o< (subst₂ (λ j k → odef j k) *iso (sym &iso) lemma15 ))
        lemma12 {z} record { owner = owner ; ao = (case2 eq) ; ox = ox } with (subst (λ k → odef k z) (trans (cong (*) eq) *iso )  ox)
-       ... | case1 eq1 = o≤-refl0 ?
-       ... | case2 eq1 = ?
+       ... | case1 eq1 = o≤-refl0 (trans eq1 &iso )
+       ... | case2 eq1 = o≤-refl0 (trans eq1 &iso )
+       lemma14 : {z : Ordinal} →
+            z o< osuc (& (Union (* x , (* x , * x)))) → 
+            Own (* (& (Union (* x , (* x , * x)))) , (* (& (Union (* x , (* x , * x)))) , * (& (Union (* x , (* x , * x)))))) z 
+       lemma14 {z} lt with osuc-≡< lt
+       ... | case1 eq   = record { owner = _ ; ao = case2 refl ; ox = subst (λ k → odef k z) (sym *iso) ( case2 (trans eq (sym &iso) )) } 
+       ... | case2 z<ux = record { owner = _ ; ao = case1 refl ; ox = lemma17 } where
+            lemma16 : (Union (* x , (* x , * x ))) ≡ Ord (osuc x)
+            lemma16 = nat=Ord it
+            lemma19 : odef (Union (* x , (* x , * x))) x
+            lemma19 = record { owner = _ ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) &iso (case1 refl) } 
+            lemma18 : z o< osuc x
+            lemma18 = begin
+               z <⟨ z<ux ⟩
+               & (Union (* x , (* x , * x))) ≤⟨ ? ⟩
+               x ∎ where open o≤-Reasoning O
+            lemma17 : odef (* (& (* (& (Union (* x , (* x , * x))))))) z
+            lemma17 = subst (λ k → odef k z) (trans (sym lemma16) (sym (trans *iso *iso))) lemma18
 
 infinite : HOD
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = osuc (& (Ord (next o∅))) ; <odmax = lemma }