agda-programming-with-finite-sets/Examples/Pauli.agda at main · dfirsov/agda-programming-with-finite-sets · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115


module Examples.Pauli where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Relation.Nullary

open import Data.List
open import Data.Sum
open import Data.Empty

open import Utilities.ListProperties
  using (_∈_ ; here ; there)


data Pauli : Set where
  X : Pauli
  Y : Pauli
  Z : Pauli
  I : Pauli


listPauli : List Pauli
listPauli = X ∷ Y ∷ Z ∷ I ∷ []


allPauli : (p : Pauli) → p ∈ listPauli
allPauli X = here
allPauli Y = there here
allPauli Z = there (there here)
allPauli I = there (there (there here))


_==_ : (p₁ p₂ : Pauli) → p₁ ≡ p₂ ⊎ (p₁ ≡ p₂ → ⊥)
X == X = inj₁ refl
X == Y = inj₂ (λ { () })
X == Z = inj₂ (λ { () })
X == I = inj₂ (λ { () })
Y == X = inj₂ (λ { () })
Y == Y = inj₁ refl
Y == Z = inj₂ (λ { () })
Y == I = inj₂ (λ { () })
Z == X = inj₂ (λ { () })
Z == Y = inj₂ (λ { () })
Z == Z = inj₁ refl
Z == I = inj₂ (λ { () })
I == X = inj₂ (λ { () })
I == Y = inj₂ (λ { () })
I == Z = inj₂ (λ { () })
I == I = inj₁ refl


_⋅_ : Pauli → Pauli → Pauli
X ⋅ X = I
X ⋅ Y = Z
X ⋅ Z = Y
Y ⋅ X = Z
Y ⋅ Y = I
Y ⋅ Z = X
Z ⋅ X = Y
Z ⋅ Y = X
Z ⋅ Z = I
a ⋅ I = a
I ⋅ a = a


⋅-comm : (p₁ p₂ : Pauli) → p₁ ⋅ p₂ ≡ p₂ ⋅ p₁
⋅-comm X X = refl
⋅-comm X Y = refl
⋅-comm X Z = refl
⋅-comm X I = refl
⋅-comm Y X = refl
⋅-comm Y Y = refl
⋅-comm Y Z = refl
⋅-comm Y I = refl
⋅-comm Z X = refl
⋅-comm Z Y = refl
⋅-comm Z Z = refl
⋅-comm Z I = refl
⋅-comm I X = refl
⋅-comm I Y = refl
⋅-comm I Z = refl
⋅-comm I I = refl


open import Data.Fin
open import Data.Fin.Dec
open import Data.Nat
open import Data.Bool
open import Relation.Nullary.Decidable

p2f : Pauli → Fin 4
p2f X = zero
p2f Y = suc zero
p2f Z = suc (suc zero)
p2f I = suc (suc (suc zero))

f2p : Fin 4 → Pauli
f2p zero = X
f2p (suc zero) = Y
f2p (suc (suc zero)) = Z
f2p (suc (suc (suc zero))) = I
f2p (suc (suc (suc (suc ()))))

fp-inv : ∀ p → f2p (p2f p) ≡ p
fp-inv X = refl
fp-inv Y = refl
fp-inv Z = refl
fp-inv I = refl