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

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

Not as straightforward as first imagined...

File size: 10.5 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.Product hiding (map)
8  open import Data.Sum hiding (map)
9  open import Data.Unit hiding (_≟_)
10
11  open import Function
12
13  open import Relation.Nullary
14  open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉)
15
16  -- The following is ported from `test.ma'.
17
18  data Expression (α : Set) : Set where
19       : ℕ  Expression α
20    _⊕_ : Expression α  Expression α  Expression α
21    _⊗_ : Expression α  Expression α  Expression α
22
23  module MissingStandardLibrary where
24
25    -- Lifting Bool into Set
26    toSet : Bool  Set
27    toSet true  = ⊤
28    toSet false = ⊥
29
30    -- Properties of Boolean negation
31    not-not-elim : (b : Bool)  not (not b) ≡ b
32    not-not-elim true  = refl
33    not-not-elim false = refl
34
35    not-self-adjoint₁ : (b c : Bool)  not b ≡ c  b ≡ not c
36    not-self-adjoint₁ true  true  ()
37    not-self-adjoint₁ true  false not-b≡c = refl
38    not-self-adjoint₁ false true  not-b≡c = refl
39    not-self-adjoint₁ false false ()
40
41    not-self-adjoint₂ : (b c : Bool)  b ≡ not c  not b ≡ c
42    not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
43
44    -- Properties of Boolean disjunction and conjunction
45    ∨-elim₂ : (b : Bool)  b ∨ true ≡ true
46    ∨-elim₂ true  = refl
47    ∨-elim₂ false = refl
48
49    ∨-cases-true₁ : (b c : Bool)  b ∨ c ≡ true  b ≡ true ⊎ c ≡ true
50    ∨-cases-true₁ true  c b∨c-true = inj₁ refl
51    ∨-cases-true₁ false c b∨c-true = inj₂ b∨c-true
52
53    ∨-cases-true₂ : (b c : Bool)  b ≡ true ⊎ c ≡ true  b ∨ c ≡ true
54    ∨-cases-true₂ true  c b⊎c≡true = refl
55    ∨-cases-true₂ false c (inj₁ ())
56    ∨-cases-true₂ false c (inj₂ y) = y
57
58    ∧-cases-true₁ : (b c : Bool)  b ∧ c ≡ true  (b ≡ true) × (c ≡ true)
59    ∧-cases-true₁ true  c     b∧c≡true = refl , b∧c≡true
60    ∧-cases-true₁ false true  b∧c≡true = b∧c≡true , refl
61    ∧-cases-true₁ false false b∧c≡true = b∧c≡true , b∧c≡true
62
63    ∧-cases-true₂ : (b c : Bool)  (b ≡ true) × (c ≡ true)  (b ∧ c) ≡ true
64    ∧-cases-true₂ true  c b≡true×c≡true = proj₂ b≡true×c≡true
65    ∧-cases-true₂ false c b≡true×c≡true = proj₁ b≡true×c≡true
66
67    -- Boolean equality
68    _≈_ : Bool  Bool  Bool
69    true  ≈ c = c
70    false ≈ c = not c
71
72    ≈-reflexive : (b : Bool)  b ≈ b ≡ true
73    ≈-reflexive true  = refl
74    ≈-reflexive false = refl
75
76    ≈-true₁ : (b c : Bool)  b ≈ c ≡ true  b ≡ c
77    ≈-true₁ true  true  b≈c-true = refl
78    ≈-true₁ true  false ()
79    ≈-true₁ false true  b≈c-true = b≈c-true
80    ≈-true₁ false false b≈c-true = refl
81
82    ≈-true₂ : (b c : Bool)  b ≡ c  b ≈ c ≡ true
83    ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c
84
85  -- Tags, and their equality
86  module Tag where
87
88    data Tag : Set where
89      literal : Tag
90      plus    : Tag
91      times   : Tag
92
93    toTag : {α : Set}  Expression α  Tag
94    toTag (↑ _)   = literal
95    toTag (_ ⊕ _) = plus
96    toTag (_ ⊗ _) = times
97
98    _≈_ : Tag  Tag  Bool
99    literal ≈ literal = true
100    plus    ≈ plus    = true
101    times   ≈ times   = true
102    _       ≈ _       = false
103
104    _≉_ : Tag  Tag  Bool
105    l ≉ r = not $ l ≈ r
106
107    ≈-≉-dual : (l r : Tag)  l ≈ r ≡ not (l ≉ r)
108    ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl
109
110    ≈-reflexive : (l : Tag)  l ≈ l ≡ true
111    ≈-reflexive literal = refl
112    ≈-reflexive plus    = refl
113    ≈-reflexive times   = refl
114
115    ≈-true₁ : (l r : Tag)  l ≈ r ≡ true  l ≡ r
116    ≈-true₁ literal literal l≈r-true = refl
117    ≈-true₁ literal plus    ()
118    ≈-true₁ literal times   ()
119    ≈-true₁ plus    literal ()
120    ≈-true₁ plus    plus    l≈r-true = refl
121    ≈-true₁ plus    times   ()
122    ≈-true₁ times   literal ()
123    ≈-true₁ times   plus    ()
124    ≈-true₁ times   times   l≈r-true = refl
125
126    ≈-true₂ : (l r : Tag)  l ≡ r  l ≈ r ≡ true
127    ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r
128
129    ≉-true₁ : (l r : Tag)  l ≉ r ≡ true  l ≢ r
130    ≉-true₁ literal literal ()
131    ≉-true₁ literal plus    l≉r-true = λ ()
132    ≉-true₁ literal times   l≉r-true = λ ()
133    ≉-true₁ plus    literal l≉r-true = λ ()
134    ≉-true₁ plus    plus    ()
135    ≉-true₁ plus    times   l≉r-true = λ ()
136    ≉-true₁ times   literal l≉r-true = λ ()
137    ≉-true₁ times   plus    l≉r-true = λ ()
138    ≉-true₁ times   times   ()
139
140    ≉-true₂ : (l r : Tag)  l ≢ r  l ≉ r ≡ true
141    ≉-true₂ literal literal l≢r = ⊥-elim $ l≢r refl
142    ≉-true₂ literal plus    l≢r = refl
143    ≉-true₂ literal times   l≢r = refl
144    ≉-true₂ plus    literal l≢r = refl
145    ≉-true₂ plus    plus    l≢r = ⊥-elim $ l≢r refl
146    ≉-true₂ plus    times   l≢r = refl
147    ≉-true₂ times   literal l≢r = refl
148    ≉-true₂ times   plus    l≢r = refl
149    ≉-true₂ times   times   l≢r = ⊥-elim $ l≢r refl
150
151    ≈-≉-decidable : (l r : Tag)  l ≈ r ≡ true ⊎ l ≉ r ≡ true
152    ≈-≉-decidable literal literal = inj₁ refl
153    ≈-≉-decidable literal plus    = inj₂ refl
154    ≈-≉-decidable literal times   = inj₂ refl
155    ≈-≉-decidable plus    literal = inj₂ refl
156    ≈-≉-decidable plus    plus    = inj₁ refl
157    ≈-≉-decidable plus    times   = inj₂ refl
158    ≈-≉-decidable times   literal = inj₂ refl
159    ≈-≉-decidable times   plus    = inj₂ refl
160    ≈-≉-decidable times   times   = inj₁ refl
161
162  module DeqSet where
163
164    record DeqSet (α : Set) : Set where
165      constructor
166        mkDeqSet
167      field
168        _≈_           : α  α  Bool
169        _≉_           : α  α  Bool
170        ≈-≉-dual      : (l r : α)  l ≈ r ≡ not (l ≉ r)
171        ≈-true₁       : (l r : α)  l ≈ r ≡ true  l ≡ r
172        ≈-true₂       : (l r : α)  l ≡ r  l ≈ r ≡ true
173        ≉-true₁       : (l r : α)  l ≉ r ≡ true  l ≢ r
174        ≉-true₂       : (l r : α)  l ≢ r  l ≉ r ≡ true
175        ≈-≉-decidable : (l r : α)  l ≈ r ≡ true ⊎ l ≉ r ≡ true
176
177    Tag-DeqSet : DeqSet Tag.Tag
178    Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable
179
180    _∈_ : {α : Set}  ⦃ DS : DeqSet α ⦄  α  List α  Bool
181    _∈_ ⦃ DS ⦄ e []       = false
182    _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs)
183
184    _⊆_ : {α : Set}  ⦃ DS : DeqSet α ⦄  List α  List α  Bool
185    _⊆_ ⦃ DS ⦄ sub sup = all (λ x  x ∈ sup) sub
186
187    -- (DeqSet._≈_ DS x x ∨ x ∈ xs) ∧ foldr _∧_ true (map (λ x' → DeqSet._≈_ DS x' x ∨ x' ∈ xs) xs) ≡ true
188    ⊆-reflexive : {α : Set}  ⦃ DS : DeqSet α ⦄  (l : List α)  l ⊆ l ≡ true
189    ⊆-reflexive ⦃ DS ⦄ []       = refl
190    ⊆-reflexive ⦃ DS ⦄ (x ∷ xs)
191      rewrite
192        ⊆-reflexive xs = {!!} -- MissingStandardLibrary.∧-cases-true₂ (DeqSet._≈_ DS x x ∨ x ∈ xs) _ (x≈x-∨-x-∈-xs-≡-true , {!!})
193      where
194        x≈x-∨-x-∈-xs-≡-true : (DeqSet._≈_ DS x x) ∨ (x ∈ xs) ≡ true
195        x≈x-∨-x-∈-xs-≡-true = MissingStandardLibrary.∨-cases-true₂ _ _ (inj₁ $ DeqSet.≈-true₂ DS x x refl)
196
197        xs-⊆-xs-≡-true : xs ⊆ xs ≡ true
198        xs-⊆-xs-≡-true = ⊆-reflexive xs
199
200    x∷xs-⊆-ys-to-x-∈-ys : {α : Set}  ⦃ DS : DeqSet α ⦄  (x : α)  (xs ys : List α)  (x ∷ xs) ⊆ ys ≡ true  x ∈ ys ≡ true
201    x∷xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x xs []         x∷xs⊆ys = x∷xs⊆ys
202    x∷xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊆ys with x ∈ xs'
203    ... | true  = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x'
204    ... | false = MissingStandardLibrary.∨-cases-true₂ (DeqSet._≈_ DS x x') false $ inj₁ x≈x'≡true
205      where
206        x≈x'∨false≡true∧foldr≡true : (DeqSet._≈_ DS x x' ∨ false) ≡ true × foldr _∧_ true (Data.List.map (λ x0  DeqSet._≈_ DS x0 x' ∨ x0 ∈ xs') xs) ≡ true
207        x≈x'∨false≡true∧foldr≡true = MissingStandardLibrary.∧-cases-true₁ (DeqSet._≈_ DS x x' ∨ false) (foldr _∧_ true (map (λ x  DeqSet._≈_ DS x x' ∨ x ∈ xs') xs)) x∷xs⊆ys
208
209        x≈x'∨false≡true : DeqSet._≈_ DS x x' ∨ false ≡ true
210        x≈x'∨false≡true = proj₁ $ x≈x'∨false≡true∧foldr≡true
211
212        x≈x'≡true : DeqSet._≈_ DS x x' ≡ true
213        x≈x'≡true with MissingStandardLibrary.∨-cases-true₁ (DeqSet._≈_ DS x x') false x≈x'∨false≡true
214        ... | inj₁ p = p
215        ... | inj₂ ()
216
217    -- Oh `destruct' how I miss thee...
218    false≡true-to-α : {α : Set}  false ≡ true  α
219    false≡true-to-α ()
220
221    x∷xs-⊆-ys-to-xs-⊆-ys : {α : Set}  ⦃ DS : DeqSet α ⦄  (x : α)  (xs ys : List α)  (x ∷ xs) ⊆ ys ≡ true  xs ⊆ ys ≡ true
222    x∷xs-⊆-ys-to-xs-⊆-ys ⦃ DS ⦄ x xs ys x∷xs⊆ys with x ∈ ys
223    ... | true  = x∷xs⊆ys
224    ... | false = false≡true-to-α x∷xs⊆ys
225
226    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys : {α : Set}  ⦃ DS : DeqSet α ⦄  (x : α)  (xs ys : List α)  x ∈ xs ≡ true  xs ⊆ ys ≡ true  x ∈ ys ≡ true
227    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x []        ys x∈xs≡true xs⊆ys≡true = false≡true-to-α x∈xs≡true
228    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x (x' ∷ xs) ys x∈xs≡true xs⊆ys≡true with DeqSet._≈_ DS x x' | inspect (λ x''  DeqSet._≈_ DS x'' x') $ x
229    ... | true  | 〈 p 〉 = subst _ (sym $ DeqSet.≈-true₁ DS x x' p) (proj₁ $ MissingStandardLibrary.∧-cases-true₁ (x' ∈ ys) (foldr _∧_ true (map (λ x0  x0 ∈ ys) xs)) xs⊆ys≡true)
230    ... | false | 〈 p 〉 = x-∈-xs-to-xs-⊆-ys-to-x-∈-ys x xs ys x∈xs≡true foldr-∧-≡-true
231      where
232        foldr-∧-≡-true : foldr _∧_ true (map (λ x  x ∈ ys) xs) ≡ true
233        foldr-∧-≡-true = proj₂ $ MissingStandardLibrary.∧-cases-true₁ (x' ∈ ys) _ xs⊆ys≡true
234 
235  module Random where
236
237    `_ : List Tag.Tag  Set
238    ` [] = ?
239    ` (x ∷ xs) = ?
240
241    test₁ : ` [ Tag.literal ]  ℕ
242    test₁ = {!!}
Note: See TracBrowser for help on using the repository browser.