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

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

Some more progress.

File size: 8.2 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    -- Lifting Bool into Set
25    toSet : Bool  Set
26    toSet true  = ⊤
27    toSet false = ⊥
28
29    -- Properties of Boolean negation
30    not-not-elim : (b : Bool)  not (not b) ≡ b
31    not-not-elim true  = refl
32    not-not-elim false = refl
33
34    not-self-adjoint₁ : (b c : Bool)  not b ≡ c  b ≡ not c
35    not-self-adjoint₁ true  true  ()
36    not-self-adjoint₁ true  false not-b≡c = refl
37    not-self-adjoint₁ false true  not-b≡c = refl
38    not-self-adjoint₁ false false ()
39
40    not-self-adjoint₂ : (b c : Bool)  b ≡ not c  not b ≡ c
41    not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
42
43    -- Properties of Boolean disjunction
44    ∨-elim₂ : (b : Bool)  b ∨ true ≡ true
45    ∨-elim₂ true  = refl
46    ∨-elim₂ false = refl
47
48    ∨-cases : (b c : Bool)  b ∨ c ≡ true  b ≡ true ⊎ c ≡ true
49    ∨-cases true  c b∨c-true = inj₁ refl
50    ∨-cases false c b∨c-true = inj₂ b∨c-true
51
52    -- Boolean equality
53    _≈_ : Bool  Bool  Bool
54    true  ≈ c = c
55    false ≈ c = not c
56
57    ≈-reflexive : (b : Bool)  b ≈ b ≡ true
58    ≈-reflexive true  = refl
59    ≈-reflexive false = refl
60
61    ≈-true₁ : (b c : Bool)  b ≈ c ≡ true  b ≡ c
62    ≈-true₁ true  true  b≈c-true = refl
63    ≈-true₁ true  false ()
64    ≈-true₁ false true  b≈c-true = b≈c-true
65    ≈-true₁ false false b≈c-true = refl
66
67    ≈-true₂ : (b c : Bool)  b ≡ c  b ≈ c ≡ true
68    ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c
69
70  -- Tags, and their equality
71  module Tag where
72
73    data Tag : Set where
74      literal : Tag
75      plus    : Tag
76      times   : Tag
77
78    toTag : {α : Set}  Expression α  Tag
79    toTag (↑ _)   = literal
80    toTag (_ ⊕ _) = plus
81    toTag (_ ⊗ _) = times
82
83    _≈_ : Tag  Tag  Bool
84    literal ≈ literal = true
85    plus    ≈ plus    = true
86    times   ≈ times   = true
87    _       ≈ _       = false
88
89    _≉_ : Tag  Tag  Bool
90    l ≉ r = not $ l ≈ r
91
92    ≈-≉-dual : (l r : Tag)  l ≈ r ≡ not (l ≉ r)
93    ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl
94
95    ≈-reflexive : (l : Tag)  l ≈ l ≡ true
96    ≈-reflexive literal = refl
97    ≈-reflexive plus    = refl
98    ≈-reflexive times   = refl
99
100    ≈-true₁ : (l r : Tag)  l ≈ r ≡ true  l ≡ r
101    ≈-true₁ literal literal l≈r-true = refl
102    ≈-true₁ literal plus    ()
103    ≈-true₁ literal times   ()
104    ≈-true₁ plus    literal ()
105    ≈-true₁ plus    plus    l≈r-true = refl
106    ≈-true₁ plus    times   ()
107    ≈-true₁ times   literal ()
108    ≈-true₁ times   plus    ()
109    ≈-true₁ times   times   l≈r-true = refl
110
111    ≈-true₂ : (l r : Tag)  l ≡ r  l ≈ r ≡ true
112    ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r
113
114    ≉-true₁ : (l r : Tag)  l ≉ r ≡ true  l ≢ r
115    ≉-true₁ literal literal ()
116    ≉-true₁ literal plus    l≉r-true = λ ()
117    ≉-true₁ literal times   l≉r-true = λ ()
118    ≉-true₁ plus    literal l≉r-true = λ ()
119    ≉-true₁ plus    plus    ()
120    ≉-true₁ plus    times   l≉r-true = λ ()
121    ≉-true₁ times   literal l≉r-true = λ ()
122    ≉-true₁ times   plus    l≉r-true = λ ()
123    ≉-true₁ times   times   ()
124
125    ≉-true₂ : (l r : Tag)  l ≢ r  l ≉ r ≡ true
126    ≉-true₂ literal literal l≢r = ⊥-elim $ l≢r refl
127    ≉-true₂ literal plus    l≢r = refl
128    ≉-true₂ literal times   l≢r = refl
129    ≉-true₂ plus    literal l≢r = refl
130    ≉-true₂ plus    plus    l≢r = ⊥-elim $ l≢r refl
131    ≉-true₂ plus    times   l≢r = refl
132    ≉-true₂ times   literal l≢r = refl
133    ≉-true₂ times   plus    l≢r = refl
134    ≉-true₂ times   times   l≢r = ⊥-elim $ l≢r refl
135
136    ≈-≉-decidable : (l r : Tag)  l ≈ r ≡ true ⊎ l ≉ r ≡ true
137    ≈-≉-decidable literal literal = inj₁ refl
138    ≈-≉-decidable literal plus    = inj₂ refl
139    ≈-≉-decidable literal times   = inj₂ refl
140    ≈-≉-decidable plus    literal = inj₂ refl
141    ≈-≉-decidable plus    plus    = inj₁ refl
142    ≈-≉-decidable plus    times   = inj₂ refl
143    ≈-≉-decidable times   literal = inj₂ refl
144    ≈-≉-decidable times   plus    = inj₂ refl
145    ≈-≉-decidable times   times   = inj₁ refl
146
147  module DeqSet where
148
149    record DeqSet (α : Set) : Set where
150      constructor
151        mkDeqSet
152      field
153        _≈_           : α  α  Bool
154        _≉_           : α  α  Bool
155        ≈-≉-dual      : (l r : α)  l ≈ r ≡ not (l ≉ r)
156        ≈-true₁       : (l r : α)  l ≈ r ≡ true  l ≡ r
157        ≈-true₂       : (l r : α)  l ≡ r  l ≈ r ≡ true
158        ≉-true₁       : (l r : α)  l ≉ r ≡ true  l ≢ r
159        ≉-true₂       : (l r : α)  l ≢ r  l ≉ r ≡ true
160        ≈-≉-decidable : (l r : α)  l ≈ r ≡ true ⊎ l ≉ r ≡ true
161
162    Tag-DeqSet : DeqSet Tag.Tag
163    Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable
164
165    _∈_ : {α : Set}  ⦃ DS : DeqSet α ⦄  α  List α  Bool
166    _∈_ ⦃ DS ⦄ e []       = false
167    _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs)
168
169    _⊂_ : {α : Set}  ⦃ DS : DeqSet α ⦄  List α  List α  Bool
170    _⊂_ ⦃ DS ⦄ sub sup = all (λ x  x ∈ sup) sub
171
172    x∷xs-⊂-to-∈ : {α : Set}  ⦃ DS : DeqSet α ⦄  (x : α)  (xs ys : List α)  (x ∷ xs) ⊂ ys ≡ true  x ∈ ys ≡ true
173    x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs []         x∷xs⊂ys = x∷xs⊂ys
174    x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊂ys with x ∈ xs' | inspect (λ x  x ∈ xs') $ x
175    ... | true  | 〈 p 〉 = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x'
176    ... | false | 〈 p 〉 = {!? $ MissingStandardLibrary.∨-cases ? ? p !}
177 
178  module Random where
179  -- Random stuff
180
181    [_holds-for_] : {α : Set}  (Expression α  Set)  Tag.Tag  Set
182    [ Q holds-for Tag.literal ] = (n : ℕ)  Q $ ↑ n
183    [ Q holds-for Tag.plus ]    = (x y : _)  Q $ x ⊕ y
184    [ Q holds-for Tag.times ]   = (x y : _)  Q $ x ⊗ y
185
186    holds-for-tag-specialise : {α : Set}  (Q : Expression α  Set)  (x : Expression α) 
187      [ Q holds-for (Tag.toTag x) ]  Q x
188    holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n
189    holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y
190    holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y
191
192    -- The following is ported from `variants.ma'.
193
194    _∈_ : {α : Set}  Expression α  List Tag.Tag  Bool
195    tag ∈ []        = false
196    tag ∈ (x ∷ xs) = (Tag._≈_ (Tag.toTag tag) x) ∨ (tag ∈ xs)
197
198    record Subexpression (α : Set) (l : List Tag.Tag) : Set where
199      field
200        element   : Expression α
201        ∈-element : MissingStandardLibrary.toSet $ element ∈ l
202
203    -- The following two functions are coercions in Matita.
204    subexpression : List Tag.Tag  Set  Set
205    subexpression l = λ α  Subexpression α l
206
207    mkSubexpression : {α : Set}  (l : List Tag.Tag)  (e : Expression α) 
208      MissingStandardLibrary.toSet $ e ∈ l  Subexpression α l
209    mkSubexpression l e p = record { element = e; ∈-element = p }
210
211    -- Missing from the Agda standard library, seemingly.
212    member : {α : Set}  (α  α  Bool)  α  List α  Bool
213    member p e []       = false
214    member p e (x ∷ xs) = (p e x) ∨ (member p e xs)
Note: See TracBrowser for help on using the repository browser.