source: Papers/polymorphic-variants-2012/Variants.agda @ 2544

Last change on this file since 2544 was 2544, checked in by mulligan, 7 years ago

More added, painful crash course in learning Agda. Seem to have the hang of it now.

File size: 7.1 KB
Line 
1module Variants where
2
3  open import Data.Bool
4  open import Data.Empty
5  open import Data.List
6  open import Data.Nat hiding (_≟_)
7  open import Data.Sum
8  open import Data.Unit hiding (_≟_)
9
10  open import Function
11
12  open import Relation.Nullary
13  open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉)
14
15  -- The following is ported from `test.ma'.
16
17  data Expression (α : Set) : Set where
18       : ℕ  Expression α
19    _⊕_ : Expression α  Expression α  Expression α
20    _⊗_ : Expression α  Expression α  Expression α
21
22  module MissingStandardLibrary where
23
24    toSet : Bool  Set
25    toSet true  = ⊤
26    toSet false = ⊥
27
28    not-not-elim : (b : Bool)  not (not b) ≡ b
29    not-not-elim true  = refl
30    not-not-elim false = refl
31
32    not-self-adjoint₁ : (b c : Bool)  not b ≡ c  b ≡ not c
33    not-self-adjoint₁ true  true  ()
34    not-self-adjoint₁ true  false not-b≡c = refl
35    not-self-adjoint₁ false true  not-b≡c = refl
36    not-self-adjoint₁ false false ()
37
38    not-self-adjoint₂ : (b c : Bool)  b ≡ not c  not b ≡ c
39    not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
40
41    _≈_ : Bool  Bool  Bool
42    true  ≈ c = c
43    false ≈ c = not c
44
45    ≈-reflexive : (b : Bool)  b ≈ b ≡ true
46    ≈-reflexive true  = refl
47    ≈-reflexive false = refl
48
49    ≈-true₁ : (b c : Bool)  b ≈ c ≡ true  b ≡ c
50    ≈-true₁ true  true  b≈c-true = refl
51    ≈-true₁ true  false ()
52    ≈-true₁ false true  b≈c-true = b≈c-true
53    ≈-true₁ false false b≈c-true = refl
54
55    ≈-true₂ : (b c : Bool)  b ≡ c  b ≈ c ≡ true
56    ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c
57
58  -- Tags, and their equality
59  module Tag where
60
61    data Tag : Set where
62      literal : Tag
63      plus    : Tag
64      times   : Tag
65
66    _≈_ : Tag  Tag  Bool
67    literal ≈ literal = true
68    plus    ≈ plus    = true
69    times   ≈ times   = true
70    _       ≈ _       = false
71
72    _≉_ : Tag  Tag  Bool
73    l ≉ r = not $ l ≈ r
74
75    ≈-≉-dual : (l r : Tag)  l ≈ r ≡ not (l ≉ r)
76    ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl
77
78    ≈-reflexive : (l : Tag)  l ≈ l ≡ true
79    ≈-reflexive literal = refl
80    ≈-reflexive plus    = refl
81    ≈-reflexive times   = refl
82
83    ≈-true₁ : (l r : Tag)  l ≈ r ≡ true  l ≡ r
84    ≈-true₁ literal literal l≈r-true = refl
85    ≈-true₁ literal plus    ()
86    ≈-true₁ literal times   ()
87    ≈-true₁ plus    literal ()
88    ≈-true₁ plus    plus    l≈r-true = refl
89    ≈-true₁ plus    times   ()
90    ≈-true₁ times   literal ()
91    ≈-true₁ times   plus    ()
92    ≈-true₁ times   times   l≈r-true = refl
93
94    ≈-true₂ : (l r : Tag)  l ≡ r  l ≈ r ≡ true
95    ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r
96
97    ≉-true₁ : (l r : Tag)  l ≉ r ≡ true  l ≢ r
98    ≉-true₁ literal literal ()
99    ≉-true₁ literal plus    l≉r-true = λ ()
100    ≉-true₁ literal times   l≉r-true = λ ()
101    ≉-true₁ plus    literal l≉r-true = λ ()
102    ≉-true₁ plus    plus    ()
103    ≉-true₁ plus    times   l≉r-true = λ ()
104    ≉-true₁ times   literal l≉r-true = λ ()
105    ≉-true₁ times   plus    l≉r-true = λ ()
106    ≉-true₁ times   times   ()
107
108    ≉-true₂ : (l r : Tag)  l ≢ r  l ≉ r ≡ true
109    ≉-true₂ literal literal l≢r = ⊥-elim $ l≢r refl
110    ≉-true₂ literal plus    l≢r = refl
111    ≉-true₂ literal times   l≢r = refl
112    ≉-true₂ plus    literal l≢r = refl
113    ≉-true₂ plus    plus    l≢r = ⊥-elim $ l≢r refl
114    ≉-true₂ plus    times   l≢r = refl
115    ≉-true₂ times   literal l≢r = refl
116    ≉-true₂ times   plus    l≢r = refl
117    ≉-true₂ times   times   l≢r = ⊥-elim $ l≢r refl
118
119    ≈-≉-decidable : (l r : Tag)  l ≈ r ≡ true ⊎ l ≉ r ≡ true
120    ≈-≉-decidable literal literal = inj₁ refl
121    ≈-≉-decidable literal plus    = inj₂ refl
122    ≈-≉-decidable literal times   = inj₂ refl
123    ≈-≉-decidable plus    literal = inj₂ refl
124    ≈-≉-decidable plus    plus    = inj₁ refl
125    ≈-≉-decidable plus    times   = inj₂ refl
126    ≈-≉-decidable times   literal = inj₂ refl
127    ≈-≉-decidable times   plus    = inj₂ refl
128    ≈-≉-decidable times   times   = inj₁ refl
129
130  module DeqSet where
131
132    record DeqSet (α : Set) : Set where
133      constructor
134        mkDeqSet
135      field
136        _≈_           : α  α  Bool
137        _≉_           : α  α  Bool
138
139        ≈-≉-dual      : (l r : α)  l ≈ r ≡ not (l ≉ r)
140        ≈-true₁       : (l r : α)  l ≈ r ≡ true  l ≡ r
141        ≈-true₂       : (l r : α)  l ≡ r  l ≈ r ≡ true
142        ≉-true₁       : (l r : α)  l ≉ r ≡ true  l ≢ r
143        ≉-true₂       : (l r : α)  l ≢ r  l ≉ r ≡ true
144        ≈-≉-decidable : (l r : α)  l ≈ r ≡ true ⊎ l ≉ r ≡ true
145
146    Tag-DeqSet : DeqSet Tag.Tag
147    Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable
148 
149  module Random where
150  -- Random stuff
151
152    Tag-DeqSet : DeqSet.DeqSet Tag.Tag
153    Tag-DeqSet = {!!}
154
155    toTag : {α : Set}  Expression α  Tag.Tag
156    toTag (↑ _)   = Tag.literal
157    toTag (_ ⊕ _) = Tag.plus
158    toTag (_ ⊗ _) = Tag.times
159
160    [_holds-for_] : {α : Set}  (Expression α  Set)  Tag.Tag  Set
161    [ Q holds-for Tag.literal ] = (n : ℕ)  Q $ ↑ n
162    [ Q holds-for Tag.plus ]    = (x y : _)  Q $ x ⊕ y
163    [ Q holds-for Tag.times ]   = (x y : _)  Q $ x ⊗ y
164
165    holds-for-tag-specialise : {α : Set}  (Q : Expression α  Set)  (x : Expression α) 
166      [ Q holds-for (toTag x) ]  Q x
167    holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n
168    holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y
169    holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y
170
171    -- The following is ported from `variants.ma'.
172
173    _∈_ : {α : Set}  Expression α  List Tag.Tag  Bool
174    tag ∈ []        = false
175    tag ∈ (x ∷ xs) = (Tag._≈_ (toTag tag) x) ∨ (tag ∈ xs)
176
177    record Subexpression (α : Set) (l : List Tag.Tag) : Set where
178      field
179        element   : Expression α
180        ∈-element : MissingStandardLibrary.toSet $ element ∈ l
181
182    -- The following two functions are coercions in Matita.
183    subexpression : List Tag.Tag  Set  Set
184    subexpression l = λ α  Subexpression α l
185
186    mkSubexpression : {α : Set}  (l : List Tag.Tag)  (e : Expression α) 
187      MissingStandardLibrary.toSet $ e ∈ l  Subexpression α l
188    mkSubexpression l e p = record { element = e; ∈-element = p }
189
190    -- Missing from the Agda standard library, seemingly.
191    member : {α : Set}  (α  α  Bool)  α  List α  Bool
192    member p e []       = false
193    member p e (x ∷ xs) = (p e x) ∨ (member p e xs)
Note: See TracBrowser for help on using the repository browser.