1 | module 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) |
---|