annotate partfunc.agda @ 403:ce2ce3f62023

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jul 2020 10:51:08 +0900
parents 55f44ec2a0c6
children 9984cdd88da3
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
1 {-# OPTIONS --allow-unsolved-metas #-}
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
3 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
4 open import Relation.Binary.PropositionalEquality
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
5 open import Ordinals
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
6 module partfunc {n : Level } (O : Ordinals {n}) where
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
8 open import logic
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
9 open import Relation.Binary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
10 open import Data.Empty
392
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
11 open import Data.List hiding (filter)
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
12 open import Data.Maybe
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Relation.Binary.Core
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
16 open import filter O
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
17
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
18 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
19 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
20 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
22
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
23 record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
24 field
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
25 dom : Dom → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
26 pmap : (x : Dom ) → dom x → Cod
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
27 meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
371
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 370
diff changeset
28
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
29
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
30 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
31 v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
32 vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x)
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
33
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
34 open PFunc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
35
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
36 find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
37 find (just v ∷ _) 0 (v0 v) = v
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
38 find (_ ∷ n) (Suc i) (vn p) = find n i p
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
39
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
40 findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
41 findpeq n {0} {v0 _} {v0 _} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
42 findpeq [] {Suc x} {()}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
43 findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
44 findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q}
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
45
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
46 List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
47 List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
48 ; pmap = λ x y → find fp (lower x) (lower y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
49 ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
50 }
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
51
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
52 _3⊆b_ : (f g : List (Maybe Two)) → Bool
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
53 [] 3⊆b [] = true
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
54 [] 3⊆b (nothing ∷ g) = [] 3⊆b g
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
55 [] 3⊆b (_ ∷ g) = true
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
56 (nothing ∷ f) 3⊆b [] = f 3⊆b []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
57 (nothing ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
58 (just i0 ∷ f) 3⊆b (just i0 ∷ g) = f 3⊆b g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
59 (just i1 ∷ f) 3⊆b (just i1 ∷ g) = f 3⊆b g
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
60 _ 3⊆b _ = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
61
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
62 _3⊆_ : (f g : List (Maybe Two)) → Set
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
63 f 3⊆ g = (f 3⊆b g) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
64
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
65 _3∩_ : (f g : List (Maybe Two)) → List (Maybe Two)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
66 [] 3∩ (nothing ∷ g) = nothing ∷ ([] 3∩ g)
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
67 [] 3∩ g = []
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
68 (nothing ∷ f) 3∩ [] = nothing ∷ f 3∩ []
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
69 f 3∩ [] = []
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
70 (just i0 ∷ f) 3∩ (just i0 ∷ g) = just i0 ∷ ( f 3∩ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
71 (just i1 ∷ f) 3∩ (just i1 ∷ g) = just i1 ∷ ( f 3∩ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
72 (_ ∷ f) 3∩ (_ ∷ g) = nothing ∷ ( f 3∩ g )
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
73
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
74 3∩⊆f : { f g : List (Maybe Two) } → (f 3∩ g ) 3⊆ f
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
75 3∩⊆f {[]} {[]} = refl
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
76 3∩⊆f {[]} {just _ ∷ g} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
77 3∩⊆f {[]} {nothing ∷ g} = 3∩⊆f {[]} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
78 3∩⊆f {just _ ∷ f} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
79 3∩⊆f {nothing ∷ f} {[]} = 3∩⊆f {f} {[]}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
80 3∩⊆f {just i0 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
81 3∩⊆f {just i1 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
82 3∩⊆f {just i0 ∷ f} {just i1 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
83 3∩⊆f {just i1 ∷ f} {just i0 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
84 3∩⊆f {nothing ∷ f} {just _ ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
85 3∩⊆f {just i0 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
86 3∩⊆f {just i1 ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
87 3∩⊆f {nothing ∷ f} {nothing ∷ g} = 3∩⊆f {f} {g}
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
88
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
89 3∩sym : { f g : List (Maybe Two) } → (f 3∩ g ) ≡ (g 3∩ f )
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
90 3∩sym {[]} {[]} = refl
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
91 3∩sym {[]} {just _ ∷ g} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
92 3∩sym {[]} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {[]} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
93 3∩sym {just _ ∷ f} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
94 3∩sym {nothing ∷ f} {[]} = cong (λ k → nothing ∷ k) (3∩sym {f} {[]})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
95 3∩sym {just i0 ∷ f} {just i0 ∷ g} = cong (λ k → just i0 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
96 3∩sym {just i0 ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
97 3∩sym {just i1 ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
98 3∩sym {just i1 ∷ f} {just i1 ∷ g} = cong (λ k → just i1 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
99 3∩sym {just i0 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
100 3∩sym {just i1 ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
101 3∩sym {nothing ∷ f} {just i0 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
102 3∩sym {nothing ∷ f} {just i1 ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
103 3∩sym {nothing ∷ f} {nothing ∷ g} = cong (λ k → nothing ∷ k) (3∩sym {f} {g})
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
104
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
105 3⊆-[] : { h : List (Maybe Two) } → [] 3⊆ h
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
106 3⊆-[] {[]} = refl
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
107 3⊆-[] {just _ ∷ h} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
108 3⊆-[] {nothing ∷ h} = 3⊆-[] {h}
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
109
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
110 3⊆trans : { f g h : List (Maybe Two) } → f 3⊆ g → g 3⊆ h → f 3⊆ h
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
111 3⊆trans {[]} {[]} {[]} f<g g<h = refl
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
112 3⊆trans {[]} {[]} {just _ ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
113 3⊆trans {[]} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
114 3⊆trans {[]} {nothing ∷ g} {[]} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
115 3⊆trans {[]} {just _ ∷ g} {just _ ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
116 3⊆trans {[]} {nothing ∷ g} {just _ ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
117 3⊆trans {[]} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
118 3⊆trans {nothing ∷ f} {[]} {[]} f<g g<h = f<g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
119 3⊆trans {nothing ∷ f} {[]} {just _ ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
120 3⊆trans {nothing ∷ f} {[]} {nothing ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
121 3⊆trans {nothing ∷ f} {nothing ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
122 3⊆trans {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
123 3⊆trans {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
124 3⊆trans {[]} {just i0 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
125 3⊆trans {[]} {just i1 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
126 3⊆trans {[]} {just x ∷ g} {nothing ∷ h} f<g g<h = 3⊆-[] {h}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
127 3⊆trans {just i0 ∷ f} {[]} {h} () g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
128 3⊆trans {just i1 ∷ f} {[]} {h} () g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
129 3⊆trans {just x ∷ f} {just i0 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
130 3⊆trans {just x ∷ f} {just i1 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
131 3⊆trans {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
132 3⊆trans {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
133 3⊆trans {just x ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
134 3⊆trans {just x ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
135 3⊆trans {just i0 ∷ f} {nothing ∷ g} {_} () g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
136 3⊆trans {just i1 ∷ f} {nothing ∷ g} {_} () g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
137 3⊆trans {nothing ∷ f} {just i0 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
138 3⊆trans {nothing ∷ f} {just i1 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
139 3⊆trans {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
140 3⊆trans {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
141 3⊆trans {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
142 3⊆trans {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g ()
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
143
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
144 3⊆∩f : { f g h : List (Maybe Two) } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h )
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
145 3⊆∩f {[]} {[]} {[]} f<g f<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
146 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
147 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
148 3⊆∩f {nothing ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
149 3⊆∩f {nothing ∷ f} {[]} {just _ ∷ h} f<g f<h = f<g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
150 3⊆∩f {nothing ∷ f} {[]} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
151 3⊆∩f {just i0 ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
152 3⊆∩f {just i1 ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
153 3⊆∩f {nothing ∷ f} {just _ ∷ g} {[]} f<g f<h = f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
154 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
155 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
156 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
157 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {just i1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
158 3⊆∩f {nothing ∷ f} {just i0 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
159 3⊆∩f {nothing ∷ f} {just i1 ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
160 3⊆∩f {nothing ∷ f} {nothing ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
161 3⊆∩f {nothing ∷ f} {nothing ∷ g} {just _ ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
162 3⊆∩f {nothing ∷ f} {nothing ∷ g} {nothing ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
163
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
164 3↑22 : (f : Nat → Two) (i j : Nat) → List (Maybe Two)
382
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
165 3↑22 f Zero j = []
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
166 3↑22 f (Suc i) j = just (f j) ∷ 3↑22 f i (Suc j)
382
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
167
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
168 _3↑_ : (Nat → Two) → Nat → List (Maybe Two)
384
171a3d587d6e Three List / Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 383
diff changeset
169 _3↑_ f i = 3↑22 f i 0
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
170
384
171a3d587d6e Three List / Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 383
diff changeset
171 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x) 3⊆ (_3↑_ f y)
171a3d587d6e Three List / Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 383
diff changeset
172 3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
383
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
173 lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
174 lemma 0 y i z≤n with f i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
175 lemma Zero Zero i z≤n | i0 = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
176 lemma Zero (Suc y) i z≤n | i0 = 3⊆-[] {3↑22 f (Suc y) i}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
177 lemma Zero Zero i z≤n | i1 = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
178 lemma Zero (Suc y) i z≤n | i1 = 3⊆-[] {3↑22 f (Suc y) i}
384
171a3d587d6e Three List / Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 383
diff changeset
179 lemma (Suc x) (Suc y) i (s≤s x<y) with f i
171a3d587d6e Three List / Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 383
diff changeset
180 lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y
171a3d587d6e Three List / Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 383
diff changeset
181 lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y
383
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
182
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
183 Finite3b : (p : List (Maybe Two) ) → Bool
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
184 Finite3b [] = true
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
185 Finite3b (just _ ∷ f) = Finite3b f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
186 Finite3b (nothing ∷ f) = false
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
187
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
188 finite3cov : (p : List (Maybe Two) ) → List (Maybe Two)
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
189 finite3cov [] = []
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
190 finite3cov (just y ∷ x) = just y ∷ finite3cov x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
191 finite3cov (nothing ∷ x) = just i0 ∷ finite3cov x
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
192
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
193 Dense-3 : F-Dense (List (Maybe Two) ) (λ x → One) _3⊆_ _3∩_
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
194 Dense-3 = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
195 dense = λ x → Finite3b x ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
196 ; d⊆P = OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
197 ; dense-f = λ x → finite3cov x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
198 ; dense-d = λ {p} d → lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
199 ; dense-p = λ {p} d → lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
200 } where
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
201 lemma1 : (p : List (Maybe Two) ) → Finite3b (finite3cov p) ≡ true
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
202 lemma1 [] = refl
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
203 lemma1 (just i0 ∷ p) = lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
204 lemma1 (just i1 ∷ p) = lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
205 lemma1 (nothing ∷ p) = lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
206 lemma2 : (p : List (Maybe Two)) → p 3⊆ finite3cov p
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
207 lemma2 [] = refl
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
208 lemma2 (just i0 ∷ p) = lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
209 lemma2 (just i1 ∷ p) = lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 386
diff changeset
210 lemma2 (nothing ∷ p) = lemma2 p
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
211
388
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
212 -- min = Data.Nat._⊓_
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
213 -- m≤m⊔n = Data.Nat._⊔_
388
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
214 -- open import Data.Nat.Properties
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
215