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

changeset 1325:8b909deb840e

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, 11 Jun 2023 19:57:52 +0900
parents 1eefc6600354
children 1fe857e51f49
files src/bijection.agda src/nat.agda
diffstat 2 files changed, 45 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Sun Jun 11 18:49:13 2023 +0900
+++ b/src/bijection.agda	Sun Jun 11 19:57:52 2023 +0900
@@ -600,7 +600,7 @@
     ... | no nisA | no nisB = ca≤cb0 n
 
     data  FL (n : ℕ ) : Set where
-       ca<n : (i : ℕ) →  fun→ cn (g (f (fun← an i))) < n →  FL n
+       ca<n : (i : ℕ) →  fun→ cn (g (f (fun← an i))) < suc n →  FL n
 
     _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  
     _f<_  {n} (ca<n i i<n) (ca<n j j<n) = fun→ cn (g (f (fun← an i))) < fun→ cn (g (f (fun← an j))) 
@@ -610,20 +610,20 @@
     f<-trans : {n : ℕ } { x y z : FL n } → x f< y → y f< z → x f< z
     f<-trans {n} {ca<n i x} {ca<n i₁ x₁} {ca<n i₂ x₂} x<y y<z = <-trans x<y y<z
 
-    FL-eq0 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n}  
+    FL-eq0 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < suc n } {y : fun→ cn (g (f (fun← an j))) < suc n}  
          → ca<n i x ≡ ca<n j y 
          → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j)))
     FL-eq0 {n} {i} {.i} {x} {.x} refl = refl
 
     -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
 
-    FL-eq1 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n}  
+    FL-eq1 : {n i j : ℕ} → {x : fun→ cn (g (f (fun← an i))) < suc n } {y : fun→ cn (g (f (fun← an j))) < suc n}  
          → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j)))
          → ca<n i x ≡ ca<n j y 
     FL-eq1 {n} {i} {j} {x} {y} eq = lem00 i=j where
         i=j : i ≡ j
         i=j = bi-inject← an (InjectiveF.inject fi ( InjectiveF.inject gi (bi-inject→ cn eq) ))
-        lem00 : {x : fun→ cn (g (f (fun← an i))) < n } {y : fun→ cn (g (f (fun← an j))) < n} → i ≡ j → ca<n i x ≡ ca<n j y
+        lem00 : {x : fun→ cn (g (f (fun← an i))) < suc n } {y : fun→ cn (g (f (fun← an j))) < suc n} → i ≡ j → ca<n i x ≡ ca<n j y
         lem00 {x} {y} refl with <-irrelevant x y
         ... | refl = refl
 
@@ -682,6 +682,28 @@
     x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
     x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
 
+    FL0uniq : {a b : FL zero} → a ≡ b
+    FL0uniq {ca<n i x} {ca<n j y} = FL-eq1 (trans lem01 (sym lem02))  where
+       lem01 : fun→ cn (g (f (fun← an i))) ≡ 0
+       lem01 with <-cmp (fun→ cn (g (f (fun← an i))))  0
+       ... | tri≈ ¬a b ¬c = b
+       ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c x )
+       lem02 : fun→ cn (g (f (fun← an j))) ≡ 0
+       lem02 with <-cmp (fun→ cn (g (f (fun← an j))))  0
+       ... | tri≈ ¬a b ¬c = b
+       ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c y )
+
+    insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
+    insAny {zero} {f1} {f2} (cons a L xr) (here eq) = here FL0uniq
+    insAny {zero} {f1} {f2} (cons a L xr) (there any) = insAny {zero} {f1} {f2} L any 
+    insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a 
+    ... | tri< x<a ¬b ¬c = there any
+    ... | tri≈ ¬a b ¬c = any
+    insAny {suc n} {a} {h} (cons a [] (Level.lift tt)) (here refl) | tri> ¬a ¬b c = here refl
+    insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl
+    insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)
+
+
     record maxAC (n : ℕ) : Set where
        field
            ac : ℕ
@@ -692,7 +714,7 @@
     fla-max zero = fun→ cn (g (f (fun← an zero)))
     fla-max (suc n) = max (fun→ cn (g (f (fun← an (suc n))))) (fla-max n)
 
-    fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < fla-max n
+    fla-max< : (i n : ℕ) → i < suc n → fun→ cn (g (f (fun← an i))) < suc (fla-max n)
     fla-max< zero n i≤n = ?
     fla-max< (suc i) n i≤n = ?
 
@@ -702,7 +724,7 @@
         fl0 = ca<n zero (fla-max< zero n 0<s )
     fla0 (suc i) n (s≤s lt) = FLinsert fl0 fl1  where
         fl0 : FL (fla-max n )
-        fl0 = ca<n (suc i) (fla-max< (suc i) n ? )
+        fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ lt a<sa) )
         fl1 = fla0 i n (≤-trans refl-≤s (s≤s lt)) 
     fla : (n : ℕ) → FList (fla-max n)
     fla n = fla0 n n a<sa  
@@ -713,18 +735,22 @@
           flany  : (i : ℕ) → (i<n : i < suc n ) →  Any ( ca<n i (fla-max< i n i<n ) ≡_) flist
 
     flany : (n : ℕ) → FLany n
-    flany n = record { flist = fla0 n n a<sa ; flany = ? } where
-        flany0  : (i : ℕ) → (i<n : i < suc n ) → Any ( ca<n i (fla-max< i n i<n ) ≡_) (fla0 i n i<n)
-        flany0 zero i<n = fl1 where
+    flany n = record { flist = fla0 n n a<sa ; flany = λ j j<n → flany0 n a<sa j j<n (x<sy→x≤y j<n) } where
+        flany0  : (i : ℕ) → (i<n : i < suc n ) → (j : ℕ) → (j<n : j < suc n) → j ≤ i → Any ( ca<n j (fla-max< j n j<n ) ≡_) (fla0 i n i<n)
+        flany0 zero i<n zero j<n z≤n = fl1 where
             fl0 = ca<n zero (fla-max< zero n 0<s )
             fl1 = x∈FLins fl0 [] 
-        flany0 (suc i) (s≤s i<n) = fl3 where
+        flany0 (suc i) (s≤s i<n) j j<n j≤i with ≤-∨ j≤i
+        ... | case1 refl = fl3 where
             fl0 : FL (fla-max n )
-            fl0 = ca<n (suc i) (fla-max< (suc i) n ? )
+            fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa) )
             fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n)) 
             fl3 = x∈FLins fl0 fl1 
-            fl4  : Any ( ca<n i (fla-max< i n (≤-trans refl-≤s (s≤s i<n)) ) ≡_) (fla0 i n (≤-trans refl-≤s (s≤s i<n)))
-            fl4 = flany0 i (≤-trans refl-≤s (s≤s i<n)) 
+        ... | case2 (s≤s j<i) = insAny fl1 (flany0 i (≤-trans refl-≤s (s≤s i<n)) j j<n j<i) where
+            fl0 : FL (fla-max n )
+            fl0 = ca<n (suc i) (fla-max< (suc i) n (<-transʳ i<n a<sa) )
+            fl1 = fla0 i n (≤-trans refl-≤s (s≤s i<n)) 
+            fl3 = x∈FLins fl0 fl1 
 
  
     lem02 : (n : ℕ) → maxAC n
--- a/src/nat.agda	Sun Jun 11 18:49:13 2023 +0900
+++ b/src/nat.agda	Sun Jun 11 19:57:52 2023 +0900
@@ -256,6 +256,12 @@
 sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n
 sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le)
 
+x<sy→x≤y : {x y : ℕ } → x < suc y → x  ≤ y 
+x<sy→x≤y {zero} {suc y} (s≤s le) = z≤n
+x<sy→x≤y {suc x} {suc y} (s≤s le) = s≤s (x<sy→x≤y {x} {y} le)
+x<sy→x≤y {zero} {zero} (s≤s z≤n) = ≤-refl
+
+
 open import Data.Product
 
 i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j