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

changeset 85:7494ae6b83c6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
omax-induction does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Jun 2019 02:58:17 +0900
parents 4b2aff372b7c
children 08be6351927e
files ordinal.agda
diffstat 1 files changed, 24 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal.agda	Tue Jun 04 23:58:58 2019 +0900
+++ b/ordinal.agda	Wed Jun 05 02:58:17 2019 +0900
@@ -199,6 +199,9 @@
 maxα x y | tri> ¬a ¬b c = y
 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
 
+--
+--  max ( osuc x , osuc y )
+--
 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
 omax {n} x y with <-cmp (lv x) (lv y)
 omax {n} x y | tri< a ¬b ¬c = osuc y
@@ -208,6 +211,21 @@
 omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x
 omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x
 
+omax-induction : {n : Level} ( x y : Ordinal {suc n} ) → { ψ : ( m : Ordinal {suc n} ) → m ≡ omax x y  → Set (suc n) }
+   → (  lv x < lv y → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
+   → (  lv y < lv x → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
+   → (  lv y ≡ lv x → ord x ≅ ord y  → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
+   → (  lv y ≡ lv x → ord x d< ord y  → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
+   → (  lv y ≡ lv x → ord y d< ord x  → ( m : Ordinal {suc n} ) → (eq : m ≡ omax x y ) → ψ m eq )
+   → ψ ( omax x y ) refl
+omax-induction {n} x y c1 c2 c3 c4 c5 with <-cmp (lv x) (lv y)
+omax-induction {n} x y c1 c2 c3 c4 c5 | tri< a ¬b ¬c = c1 a (osuc y) refl
+omax-induction {n} x y c1 c2 c3 c4 c5 | tri> ¬a ¬b c = c2 c (osuc x) refl
+omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y)
+omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = c4 refl a (osuc y) refl
+omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = c3 refl refl (osuc x) refl
+omax-induction {n} x y c1 c2 c3 c4 c5 | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = c5 refl c (osuc x) refl
+
 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
 omax< {n} x y lt with <-cmp (lv x) (lv y)
 omax< {n} x y lt | tri< a ¬b ¬c = refl
@@ -220,10 +238,12 @@
 omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) )
 
 omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
-omaxx {n} x y with trio< x y 
-omaxx {n} x y | tri< a ¬b ¬c = {!!}
-omaxx {n} x y | tri> ¬a ¬b c = {!!}
-omaxx {n} x y | tri≈ ¬a b ¬c = {!!}
+omaxx {n} x y = omax-induction {n} x y {λ om refl → x o< om }
+     ( λ lx<ly omax refl → ordtrans (case1 lx<ly) <-osuc )
+     ( λ lx>ly omax → {!!} ) -- ordtrans (case1 lx>ly) <-osuc )
+     ( λ refl refl omax refl → {!!} ) -- <-osuc )
+     ( λ refl ox<oy omax → {!!} ) -- ordtrans (case2 ox<oy) <-osuc )
+     ( λ refl ox>oy omax → {!!} ) -- ordtrans (case2 ox>oy) <-osuc )
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl