Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1322:70d46c446b0d
using Fresh List
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 11 Jun 2023 10:26:09 +0900 |
| parents | 1f43bbfff797 |
| children | 95f6216499d7 |
| files | src/bijection.agda |
| diffstat | 1 files changed, 90 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/bijection.agda Sun Jun 11 01:20:46 2023 +0900 +++ b/src/bijection.agda Sun Jun 11 10:26:09 2023 +0900 @@ -10,7 +10,7 @@ open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty -open import Data.Unit hiding ( _≤_ ) +open import Data.Unit using ( tt ; ⊤ ) open import Relation.Binary.Core hiding (_⇔_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality @@ -41,6 +41,12 @@ bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S → Bijection S R bi-sym R S eq = record { fun← = fun→ eq ; fun→ = fun← eq ; fiso← = fiso→ eq ; fiso→ = fiso← eq } +bi-inject← : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : S} → fun← rs x ≡ fun← rs y → x ≡ y +bi-inject← rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso→ rs _) (fiso→ rs _) (cong (fun→ rs) eq) + +bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y +bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso← rs _) (fiso← rs _) (cong (fun← rs) eq) + open import Relation.Binary.Structures bijIsEquivalence : {n : Level } → IsEquivalence (Bijection {n} {n}) @@ -478,6 +484,13 @@ -- Bernstein is non constructive, so we cannot use this without some assumption -- but in case of ℕ, we can construct it directly. +open import Data.Product +open import Relation.Nary using (⌊_⌋) +open import Relation.Nullary.Decidable hiding (⌊_⌋) +open import Data.Unit.Base using (⊤ ; tt) +open import Data.List.Fresh hiding ([_]) + + record InjectiveF (A B : Set) : Set where field f : A → B @@ -585,6 +598,79 @@ ... | no nisA | yes isB = ≤-trans (ca≤cb0 n) px≤x ... | no nisA | no nisB = ca≤cb0 n + data FL : (n : ℕ ) → Set where + ca<n : {n : ℕ} → (i : ℕ) → fun→ cn (g (f (fun← an i))) < 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))) + + infixr 250 _f<?_ + + 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} + → 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} + → 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} {y} refl with <-irrelevant x y + ... | refl = refl + + FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_ + FLcmp {n} (ca<n i x) (ca<n j y) with <-cmp (fun→ cn (g (f (fun← an i)))) (fun→ cn (g (f (fun← an j))) ) + ... | tri< a ¬b ¬c = tri< a (λ eq → ¬b (FL-eq0 eq) ) ¬c + ... | tri≈ ¬a eq ¬c = tri≈ ¬a (FL-eq1 eq) ¬c + ... | tri> ¬a ¬b c = tri> ¬a (λ eq → ¬b (FL-eq0 eq) ) c + + _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y ) + _f<?_ {n} x y with FLcmp x y + ... | tri< a ¬b ¬c = yes a + ... | tri≈ ¬a b ¬c = no ¬a + ... | tri> ¬a ¬b c = no ¬a + + FList : (n : ℕ ) → Set + FList n = List# (FL n) ⌊ _f<?_ ⌋ + + ttf : {n : ℕ } {x a : FL (n)} → x f< a → (y : FList (n)) → fresh (FL (n)) ⌊ _f<?_ ⌋ a y → fresh (FL (n)) ⌊ _f<?_ ⌋ x y + ttf _ [] fr = Level.lift tt + ttf {_} {x} {a} lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf (ttf1 lt1 lt) y x1 where + ttf1 : True (a f<? a₁) → x f< a → x f< a₁ + ttf1 t x<a = f<-trans x<a (toWitness t) + + FLinsert : {n : ℕ } → FL n → FList n → FList n + FLfresh : {n : ℕ } → (a x : FL (suc n) ) → (y : FList (suc n) ) → a f< x + → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y) + FLinsert {zero} f0 y = f0 ∷# [] + FLinsert {suc n} x [] = x ∷# [] + FLinsert {suc n} x (cons a y x₁) with FLcmp x a + ... | tri≈ ¬a b ¬c = cons a y x₁ + ... | tri< lt ¬b ¬c = cons x ( cons a y x₁) ( Level.lift (fromWitness lt ) , ttf lt y x₁) + FLinsert {suc n} x (cons a [] x₁) | tri> ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) + FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a<x = cons a (FLinsert x y) (FLfresh a x y a<x yr ) + + FLfresh a x [] a<x (Level.lift tt) = Level.lift (fromWitness a<x) , Level.lift tt + FLfresh a x (cons b [] (Level.lift tt)) a<x (Level.lift a<b , a<y) with FLcmp x b + ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , Level.lift tt + ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , Level.lift tt + ... | tri> ¬a ¬b b<x = Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt + FLfresh a x (cons b y br) a<x (Level.lift a<b , a<y) with FLcmp x b + ... | tri< x<b ¬b ¬c = Level.lift (fromWitness a<x) , Level.lift a<b , ttf (toWitness a<b) y br + ... | tri≈ ¬a refl ¬c = Level.lift (fromWitness a<x) , ttf a<x y br + FLfresh a x (cons b [] br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = + Level.lift a<b , Level.lift (fromWitness (f<-trans (toWitness a<b) b<x)) , Level.lift tt + FLfresh a x (cons b (cons a₁ y x₁) br) a<x (Level.lift a<b , a<y) | tri> ¬a ¬b b<x = + Level.lift a<b , FLfresh a x (cons a₁ y x₁) a<x a<y + record maxAC (n : ℕ) : Set where field ac : ℕ @@ -604,14 +690,7 @@ lem12 (suc i) i=z with is-A (fun← cn (suc i)) | inspect ( count-A ) (suc i) ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s ; all-a = ? } ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso← cn _)) (sym (cong (fun← cn) i=z)) } ) - lem10 (suc j) with <-cmp (suc j) (count-A (maxAC.ac (lem10 j))) - ... | tri< a ¬b ¬c = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? } - ... | tri> ¬a ¬b ca<sj = ? -- maxAC (suc j) contains at least (suc j) elements of A - ... | tri≈ ¬a sj=ca ¬c = record { ac = nac ; n<ca = ? ; all-a = ? } where - -- - -- maxAC contains all 0 to j th element of A and nothing else - -- using full-a, we can take fun← cn which is smaller than suc j - -- so it cannot be fan. + lem10 (suc j) = record { ac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? } where fan = fun→ cn (g (f (fun← an (suc j)))) ac = maxAC.ac (lem10 j) @@ -624,6 +703,8 @@ n<ca0 = maxAC.n<ca (lem10 j) n<ca2 : j < count-A nac n<ca2 = ≤-trans n<ca0 (count-A-homo (y≤max fan ac)) + fun< : (i : ℕ) → count-A (fun→ cn (g (f (fun← an i)))) < count-A (suc (fun→ cn (g (f (fun← an i))))) + fun< = ? n<ca1 : (i n : ℕ ) → i ≤ suc j → n ≤ nac → i < count-A n n<ca1 zero n with is-A (fun← cn zero)