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

comparison src/partfunc.agda @ 1472:d0b4be1cab0d

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 Sat, 22 Jun 2024 19:23:56 +0900
parents 7d2bae0ff36b
children
comparison
equal deleted inserted replaced
1471:e970149a6af5 1472:d0b4be1cab0d
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 open import Level 2 open import Level
3 open import Relation.Nullary 3 open import Ordinals
4 open import Relation.Binary.PropositionalEquality
5 -- open import Ordinals
6 module partfunc {n : Level } where -- (O : Ordinals {n}) where
7
8 open import logic 4 open import logic
9 open import Relation.Binary 5 open import Relation.Nullary
10 open import Data.Empty 6
11 open import Data.Unit using ( ⊤ ; tt ) 7 open import Level
12 open import Data.List hiding (filter) 8 open import Ordinals
13 open import Data.Maybe 9 import HODBase
14 open import Relation.Binary 10 import OD
15 open import Relation.Binary.Core 11 open import Relation.Nullary
16 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 12 module partfunc {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where
17 -- open import filter O 13
14 open import Relation.Binary.PropositionalEquality hiding ( [_] )
15 open import Data.Empty
16
17 import OrdUtil
18
19 open Ordinals.Ordinals O
20 open Ordinals.IsOrdinals isOrdinal
21 import ODUtil
22
23 open import logic
24 open import nat
25
26 open OrdUtil O
27 open ODUtil O HODAxiom ho<
18 28
19 open _∧_ 29 open _∧_
20 open _∨_ 30 open _∨_
21 open Bool 31 open Bool
22 32
33 open HODBase._==_
34
35 open HODBase.ODAxiom HODAxiom
36 open OD O HODAxiom
37
38 open HODBase.HOD
39
40
41 open import Relation.Nullary
42 open import Relation.Binary
43 open import Data.Empty
44 open import Relation.Binary
45 open import Relation.Binary.Core
46 open import Relation.Binary.PropositionalEquality
47 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
48
49 open import Data.Empty
50 open import Data.Unit using ( ⊤ ; tt )
51 open import Data.List hiding (filter ; find)
52 open import Data.Maybe
53
54 open _∧_
55 open _∨_
56 open Bool
57
58 data Two : Set where
59 i0 : Two
60 i1 : Two
61
23 ---- 62 ----
24 -- 63 --
25 -- Partial Function without ZF 64 -- Partial Function without ZF
26 -- 65 --
27 66
28 record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where 67 record PFunc {n m l : Level } (Dom : Set n) (Cod : Set m) : Set (suc (n ⊔ m ⊔ l)) where
29 field 68 field
30 dom : Dom → Set n 69 dom : Dom → Set l
31 pmap : (x : Dom ) → dom x → Cod 70 pmap : (x : Dom ) → dom x → Cod
32 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q 71 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
33 72
34 ---- 73 ----
35 -- 74 --
36 -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod) 75 -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod)
37 -- 76 --
38 77
39 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where 78 data Findp {n : Level} {Cod : Set n} : List (Maybe Cod) → (x : Nat) → Set (suc n) where
40 v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero 79 v0 : {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero
41 vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) 80 vn : {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x)
42 81
43 open PFunc 82 open PFunc
44 83
45 find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod 84 find : {n : Level} {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
46 find (just v ∷ _) 0 (v0 v) = v 85 find (just v ∷ _) 0 (v0 v) = v
47 find (_ ∷ n) (Suc i) (vn p) = find n i p 86 find (_ ∷ n) (Suc i) (vn p) = find n i p
48 87
49 findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q 88 findpeq : {n : Level} {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
50 findpeq n {0} {v0 _} {v0 _} = refl 89 findpeq n {0} {v0 _} {v0 _} = refl
51 findpeq [] {Suc x} {()} 90 findpeq [] {Suc x} {()}
52 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} 91 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
53 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} 92 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
54 93
55 List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod 94 List→PFunc : {Cod : Set (suc n)} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
56 List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) 95 List→PFunc fp = record { dom = λ x → Lift zero (Findp fp (lower x))
57 ; pmap = λ x y → find fp (lower x) (lower y) 96 ; pmap = λ x y → find fp (lower x) (lower y)
58 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} 97 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q}
59 } 98 }
60 ---- 99 ----
61 -- 100 --
62 -- to List (Maybe Two) is a Latice 101 -- to List (Maybe Two) is a Latice
63 -- 102 --