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

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

Some new ideas that lead to non-termination...

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