Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 204:d4802eb159ff
Transfinite induction fixed
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 31 Jul 2019 15:29:51 +0900 |
parents | 8edd2a13a7f3 |
children | 22d435172d1a |
line wrap: on
line diff
--- a/ordinal.agda Wed Jul 31 12:40:02 2019 +0900 +++ b/ordinal.agda Wed Jul 31 15:29:51 2019 +0900 @@ -331,23 +331,25 @@ → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) → ∀ (x : Ordinal) → ψ x -TransFinite {n} {m} {ψ} caseΦ caseOSuc x = TransFinite1 (lv x) (ord x) where - TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) - TransFinite1 Zero (Φ 0) = caseΦ Zero lemma where +TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where + TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) ) + TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x lemma x (case1 ()) lemma x (case2 ()) - TransFinite1 (Suc lx) (Φ (Suc lx)) = caseΦ (Suc lx) lemma where - lemma : (x : Ordinal) → x o< ordinal (Suc lx) (Φ (Suc lx)) → ψ x - lemma (ordinal lx1 ox1) (case1 lt) with <-∨ lt - lemma (ordinal lx (Φ lx)) (case1 lt) | case1 refl = TransFinite1 lx (Φ lx) - lemma (ordinal lx (OSuc lx ox1)) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma (ordinal lx ox1) (case1 a<sa)) - lemma (ordinal Zero (Φ 0)) (case1 lt) | case2 (s≤s lt1) = caseΦ Zero ( λ x lt → ⊥-elim (¬x<0 lt) ) - lemma (ordinal (Suc lx1) (Φ (Suc lx1))) (case1 lt) | case2 (s≤s lt1) = caseΦ (Suc lx1) lemma2 where - lemma2 : (y : Ordinal) → (Suc (lv y) ≤ Suc lx1) ∨ (ord y d< Φ (Suc lx1)) → ψ y - lemma2 y (case1 lt2 ) = {!!} - lemma (ordinal lx1 (OSuc lx1 ox1)) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma (ordinal lx1 ox1) (case1 (<-trans lt1 a<sa ))) - TransFinite1 lx (OSuc lx ox) = caseOSuc lx ox (TransFinite1 lx ox ) + lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x + lemma1 x (case1 ()) + lemma1 x (case2 ()) + TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where + 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 ))) + 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 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p