Skip to content

Commit 0bbf193

Browse files
dfirsovdfirsov
committed
up-to-date with current Agda version
1 parent e7f015c commit 0bbf193

23 files changed

+3569
-0
lines changed

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
1+
*~
12
*.agdai
23
MAlonzo/**

‎Combinators.agda

+180
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
2+
module Combinators where
3+
4+
5+
open import Relation.Binary.PropositionalEquality
6+
hiding (inspect)
7+
open import Relation.Binary.Core
8+
open import Relation.Nullary
9+
10+
open import Data.List hiding (product ; sum ; [_] ; filter)
11+
open import Data.Empty
12+
open import Data.Unit hiding (_≟_ ; _≤_)
13+
open import Data.Sum hiding (map ; [_,_])
14+
open import Data.Product hiding (map ; <_,_>)
15+
open import Data.Bool
16+
17+
open import Utilities.ListMonad
18+
open import Utilities.ListProperties
19+
open import Utilities.ListsAddition
20+
open import Utilities.Logic
21+
22+
23+
open import Finiteness
24+
25+
26+
27+
union : {X : Set} → {P Q : X → Set}
28+
→ ListableSubset X P
29+
→ ListableSubset X Q
30+
→ ListableSubset X (λ x → P x ⊎ Q x)
31+
union {X} {P} {Q} (els1 , p2i1 , i2p1) (els2 , p2i2 , i2p2)
32+
= els1 ++ els2 , i2p' , p2i'
33+
where
34+
∈-split' : {X : Set} → {x : X} → (xs₁ xs₂ : List X)
35+
→ x ∈ (xs₁ ++ xs₂) → (x ∈ xs₁) ⊎ (x ∈ xs₂)
36+
∈-split' xs₁ xs₂ = ∈-split {_} {xs₁} {xs₂}
37+
38+
p2i' : (x : X) → P x ⊎ Q x → x ∈ (els1 ++ els2)
39+
p2i' x (inj₁ x₁) = ∈-weak-rgt {_} {els2} (i2p1 x x₁)
40+
p2i' x (inj₂ y) = ∈-weak-lft {_} {els1} (i2p2 x y)
41+
42+
i2p' : (x : X) → x ∈ (els1 ++ els2) → P x ⊎ Q x
43+
i2p' x xin with ∈-split' els1 els2 xin
44+
i2p' x xin | inj₁ x₁ = inj₁ (p2i1 x x₁)
45+
i2p' x xin | inj₂ y = inj₂ (p2i2 x y)
46+
47+
48+
49+
open import Relation.Nullary.Decidable
50+
51+
rest : {X : Set} → (x : X) → (P : X → Set) → (pd : Dec (P x))
52+
→ ⌊ pd ⌋ ≡ true → P x
53+
rest x p (yes p₁) pr = p₁
54+
rest x p (no ¬p) ()
55+
56+
restOp : {X : Set} → (x : X) → (P : X → Set) → (pd : Dec (P x))
57+
→ P x → ⌊ pd ⌋ ≡ true
58+
restOp x p (yes p₁) px = refl
59+
restOp x p (no ¬p) px = ex-falso-quodlibet (¬p px)
60+
61+
intersection : {X : Set} → {P Q : X → Set}
62+
→ (Pdec : (x : X) → Dec (P x))
63+
→ ListableSubset X P
64+
→ ListableSubset X Q
65+
→ ListableSubset X (λ x → P x × Q x)
66+
intersection {X} {P} {Q} pd (els1 , p2i1 , i2p1)
67+
(els2 , p2i2 , i2p2)
68+
= filter (λ x → ⌊ pd x ⌋) els2 , i2p' , p2i'
69+
70+
where
71+
72+
p2i' : (x : X) → P x × Q x → x ∈ filter (λ x₁ → ⌊ pd x₁ ⌋) els2
73+
p2i' x (px , qx) = filter-in2 els2 x (λ x₁ → ⌊ pd x₁ ⌋) (i2p2 x qx) (restOp x P (pd x) px)
74+
75+
i2p' : (x : X) → x ∈ filter (λ x₁ → ⌊ pd x₁ ⌋) els2 → P x × Q x
76+
i2p' x xin = p2i1 x (i2p1 x (rest x P (pd x) ((filter-el x els2 (λ x₁ → ⌊ pd x₁ ⌋) xin)))) ,
77+
p2i2 x (filter-∈ x els2 (λ x₁ → ⌊ pd x₁ ⌋) xin)
78+
79+
80+
81+
82+
<_,_> : {X Y : Set} → (X → Set) → (Y → Set) → (X × Y → Set)
83+
<_,_> P Q (x , y) = P x × Q y
84+
85+
86+
87+
[_,,_] : {X Y : Set} → (X → Set) → (Y → Set) → (X ⊎ Y → Set)
88+
[_,,_] P Q (inj₁ x) = P x
89+
[_,,_] P Q (inj₂ y) = Q y
90+
91+
92+
93+
product : {X : Set}{P : X → Set}{Y : Set}{Q : Y → Set}
94+
→ ListableSubset X P
95+
→ ListableSubset Y Q
96+
→ ListableSubset (X × Y) < P , Q >
97+
product {X} {P} {Y} {Q} (els1 , p2i1 , i2p1)
98+
(els2 , p2i2 , i2p2) =
99+
els1 >>= (λ x →
100+
els2 >>= (λ y →
101+
return (x , y))) , hlp , hlp2
102+
103+
where
104+
hlp2 : (x : X × Y) → < P , Q > x →
105+
x ∈ els1 >>= (λ x₁ → els2 >>= (λ y → return (x₁ , y)))
106+
hlp2 (x1 , y1) (pr1 , pr2) = list-monad-ht (x1 , y1) els1
107+
(λ x₁ → els2 >>= (λ y → return (x₁ , y))) x1
108+
(i2p1 x1 pr1)
109+
(list-monad-ht (x1 , y1) els2 _ y1 (i2p2 y1 pr2) here)
110+
111+
hlp : (x : X × Y) →
112+
x ∈ els1 >>= (λ x₁ → els2 >>= (λ y → return (x₁ , y))) →
113+
< P , Q > x
114+
hlp x pr with list-monad-th x els1 (λ x₁ → els2 >>= (λ y → return (x₁ , y))) pr
115+
... | o1 , o2 , o3 with list-monad-th x els2 _ o3
116+
hlp .(o1 , p1) pr | o1 , o2 , o3 | p1 , p2 , here = p2i1 o1 o2 , p2i2 p1 p2
117+
hlp x pr | o1 , o2 , o3 | p1 , p2 , there ()
118+
119+
120+
121+
122+
123+
sum : {X : Set}{P : X → Set}{Y : Set}{Q : Y → Set}
124+
→ ListableSubset X P
125+
→ ListableSubset Y Q
126+
→ ListableSubset (X ⊎ Y) [ P ,, Q ]
127+
sum {X} {P} {Y} {Q} (els1 , p2i1 , i2p1) (els2 , p2i2 , i2p2)
128+
= Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2 , hlp , hlp2
129+
where
130+
hlp : (x : X ⊎ Y) → x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2) → [ P ,, Q ] x
131+
hlp (inj₁ x) xi = p2i1 x (xi1' x els1 els2 xi)
132+
where
133+
xi1' : {X : Set} → (x : X) → (els1 : List X)
134+
→ {Y : Set} → (els2 : List Y)
135+
→ inj₁ x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
136+
→ x ∈ els1
137+
xi1' x [] [] ()
138+
xi1' x [] (x₁ ∷ ys) (there pr) = xi1' x [] ys pr
139+
xi1' x₁ (.x₁ ∷ els1) ys here = here
140+
xi1' x (x₁ ∷ els1) ys (there pr) = there (xi1' x els1 ys pr)
141+
hlp (inj₂ y) xi = p2i2 y (xi2' y els1 els2 xi)
142+
where
143+
xi2' : {X : Set}{Y : Set} → (y : Y) → (els1 : List X)
144+
→ (els2 : List Y)
145+
→ inj₂ y ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
146+
→ y ∈ els2
147+
xi2' y [] [] ()
148+
xi2' y [] (.y ∷ els2) here = here
149+
xi2' y [] (x ∷ els2) (there pr) = there (xi2' y [] els2 pr)
150+
xi2' y (x ∷ els1) els2 (there pr) = xi2' y els1 els2 pr
151+
152+
153+
hlp2 : (x : X ⊎ Y) → [ P ,, Q ] x →
154+
x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
155+
hlp2 (inj₁ x) pr = xi1 x els1 els2 (i2p1 x pr)
156+
where
157+
xi1 : {X : Set} → (x : X) → (els1 : List X)
158+
→ {Y : Set} → (els2 : List Y) → x ∈ els1
159+
→ inj₁ x ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
160+
xi1 x ._ els2 here = here
161+
xi1 x ._ els2 (there xi) = there (xi1 x _ els2 xi)
162+
hlp2 (inj₂ y) pr = xi2 y els1 els2 (i2p2 y pr)
163+
where
164+
xi2 : {X Y : Set} → (y : Y) → (els1 : List X)
165+
→ (els2 : List Y) → y ∈ els2
166+
→ inj₂ y ∈ (Data.List.map inj₁ els1 ++ Data.List.map inj₂ els2)
167+
xi2 y [] [] ()
168+
xi2 y [] (.y ∷ els2) here = here
169+
xi2 y [] (x ∷ els2) (there pr) = there (xi2 y [] els2 pr)
170+
xi2 y (x ∷ els1) els2 pr = there (xi2 y els1 els2 pr)
171+
172+
173+
174+
kfWithEq2Dec : {X : Set}{P : X → Set}
175+
→ DecEq X
176+
→ ListableSubset X P
177+
→ ∀ x → Dec (P x)
178+
kfWithEq2Dec d (l , s , c) x with eq2in d x l
179+
kfWithEq2Dec d (l , s , c) x | yes p = yes (s _ p)
180+
kfWithEq2Dec d (l , s , c) x | no ¬p = no (λ px → ¬p (c _ px))

‎Examples/Combinators.agda

+43
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
2+
module Examples.Combinators where
3+
4+
5+
open import Combinators
6+
open import Finiteness
7+
8+
open import Data.Product
9+
open import Data.List hiding (product ; sum)
10+
open import Data.Nat
11+
open import Data.Bool hiding (_≟_)
12+
open import Data.Unit
13+
open import Examples.Pauli
14+
15+
open import Utilities.ListProperties
16+
17+
-- Bool is listable
18+
BoolListable : Listable Bool
19+
BoolListable = true ∷ false ∷ [] ,
20+
(λ { true → here ; false → there here })
21+
22+
23+
-- Pauli is Listable
24+
PauliListable : Listable Pauli
25+
PauliListable = listPauli , allPauli
26+
27+
28+
-- Bool × Pauli is listable
29+
Pauli×Bool : Listable (Bool × Pauli)
30+
Pauli×Bool with product
31+
(lstbl2subset BoolListable)
32+
(lstbl2subset PauliListable)
33+
Pauli×Bool | bp , s , c = bp , (λ x → c x (tt , tt))
34+
35+
36+
-- Bool ⊎ Pauli is listable
37+
open import Data.Sum
38+
Pauli⊎Bool : Listable (Bool ⊎ Pauli)
39+
Pauli⊎Bool with sum
40+
(lstbl2subset BoolListable)
41+
(lstbl2subset PauliListable)
42+
... | bp , s , c = bp , (λ { (inj₁ x) → c _ tt ;
43+
(inj₂ y) → c _ tt })

‎Examples/FiniteSubset.agda

+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
2+
3+
module Examples.FiniteSubset where
4+
5+
open import Relation.Binary.PropositionalEquality hiding (inspect)
6+
7+
open import Data.Product
8+
open import Data.List hiding (product)
9+
open import Data.Nat
10+
open import Data.Bool hiding (_≟_)
11+
open import Data.Unit
12+
13+
open import Utilities.ListProperties
14+
15+
open import FiniteSubset
16+
open import Finiteness
17+
18+
open import Examples.Pauli
19+
20+
21+
-- MyNats1 is a newly defined finite subset of natural numbers
22+
MyNats1 : FiniteSubSet ℕ Data.Nat._≟_ false
23+
MyNats1 = fs-nojunk (1 ∷ 3 ∷ [])
24+
25+
-- we could generate all the elements of MyNats1
26+
elements : List (Element MyNats1)
27+
elements = elementsOf MyNats1
28+
29+
-- Elements of MyNats1 are the pairs of natural numbers together
30+
-- with the squashed proof of their inclusion in the underlying list
31+
-- of MyNats1
32+
prf : elements ≡ (1 , tt) ∷ (3 , tt) ∷ []
33+
prf = refl
34+
35+
36+
-- MyNats1Elements is complete
37+
elementsComplete : ∀ p → p ∈ elements
38+
elementsComplete = elementsOfComplete MyNats1
39+
40+
41+
-- we could define another finite subset of natural numbers
42+
MyNats2 : FiniteSubSet ℕ Data.Nat._≟_ false
43+
MyNats2 = fs-nojunk (1 ∷ 6 ∷ [])
44+
45+
46+
-- now we could use the combinators of FiniteSubset
47+
-- to get new finite subsets
48+
p : MyNats1 ∩ MyNats2 ≡ fs-nojunk (1 ∷ [])
49+
p = refl
50+
51+

0 commit comments

Comments
 (0)