Changeset 2549 for Papers/polymorphicvariants2012/Variants.agda
 Timestamp:
 Dec 10, 2012, 4:44:33 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/Variants.agda
r2546 r2549 5 5 open import Data.List 6 6 open import Data.Nat hiding (_≟_) 7 open import Data.Sum 7 open import Data.Product hiding (map) 8 open import Data.Sum hiding (map) 8 9 open import Data.Unit hiding (_≟_) 9 10 … … 41 42 notselfadjoint₂ b c b≡notc = sym $ notselfadjoint₁ c b $ sym $ b≡notc 42 43 43  Properties of Boolean disjunction 44  Properties of Boolean disjunction and conjunction 44 45 ∨elim₂ : (b : Bool) → b ∨ true ≡ true 45 46 ∨elim₂ true = refl 46 47 ∨elim₂ false = refl 47 48 48 ∨cases : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true 49 ∨cases true c b∨ctrue = inj₁ refl 50 ∨cases false c b∨ctrue = inj₂ b∨ctrue 49 ∨casestrue₁ : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true 50 ∨casestrue₁ true c b∨ctrue = inj₁ refl 51 ∨casestrue₁ false c b∨ctrue = inj₂ b∨ctrue 52 53 ∨casestrue₂ : (b c : Bool) → b ≡ true ⊎ c ≡ true → b ∨ c ≡ true 54 ∨casestrue₂ true c b⊎c≡true = refl 55 ∨casestrue₂ false c (inj₁ ()) 56 ∨casestrue₂ false c (inj₂ y) = y 57 58 ∧casestrue₁ : (b c : Bool) → b ∧ c ≡ true → (b ≡ true) × (c ≡ true) 59 ∧casestrue₁ true c b∧c≡true = refl , b∧c≡true 60 ∧casestrue₁ false true b∧c≡true = b∧c≡true , refl 61 ∧casestrue₁ false false b∧c≡true = b∧c≡true , b∧c≡true 62 63 ∧casestrue₂ : (b c : Bool) → (b ≡ true) × (c ≡ true) → (b ∧ c) ≡ true 64 ∧casestrue₂ true c b≡true×c≡true = proj₂ b≡true×c≡true 65 ∧casestrue₂ false c b≡true×c≡true = proj₁ b≡true×c≡true 51 66 52 67  Boolean equality … … 167 182 _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs) 168 183 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 !} 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.∧casestrue₂ (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.∨casestrue₂ _ _ (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⊆ystox∈ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊆ ys ≡ true → x ∈ ys ≡ true 201 x∷xs⊆ystox∈ys ⦃ DS ⦄ x xs [] x∷xs⊆ys = x∷xs⊆ys 202 x∷xs⊆ystox∈ys ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊆ys with x ∈ xs' 203 ...  true = MissingStandardLibrary.∨elim₂ $ DeqSet._≈_ DS x x' 204 ...  false = MissingStandardLibrary.∨casestrue₂ (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.∧casestrue₁ (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.∨casestrue₁ (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≡truetoα : {α : Set} → false ≡ true → α 219 false≡truetoα () 220 221 x∷xs⊆ystoxs⊆ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊆ ys ≡ true → xs ⊆ ys ≡ true 222 x∷xs⊆ystoxs⊆ys ⦃ DS ⦄ x xs ys x∷xs⊆ys with x ∈ ys 223 ...  true = x∷xs⊆ys 224 ...  false = false≡truetoα x∷xs⊆ys 225 226 x∈xstoxs⊆ystox∈ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → x ∈ xs ≡ true → xs ⊆ ys ≡ true → x ∈ ys ≡ true 227 x∈xstoxs⊆ystox∈ys ⦃ DS ⦄ x [] ys x∈xs≡true xs⊆ys≡true = false≡truetoα x∈xs≡true 228 x∈xstoxs⊆ystox∈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.∧casestrue₁ (x' ∈ ys) (foldr _∧_ true (map (λ x0 → x0 ∈ ys) xs)) xs⊆ys≡true) 230 ...  false  〈 p 〉 = x∈xstoxs⊆ystox∈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.∧casestrue₁ (x' ∈ ys) _ xs⊆ys≡true 177 234 178 235 module Random where 179  Random stuff 180 181 [_holdsfor_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set 182 [ Q holdsfor Tag.literal ] = (n : ℕ) → Q $ ↑ n 183 [ Q holdsfor Tag.plus ] = (x y : _) → Q $ x ⊕ y 184 [ Q holdsfor Tag.times ] = (x y : _) → Q $ x ⊗ y 185 186 holdsfortagspecialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) → 187 [ Q holdsfor (Tag.toTag x) ] → Q x 188 holdsfortagspecialise Q (↑ n) QholdsfortoTag = QholdsfortoTag n 189 holdsfortagspecialise Q (x ⊕ y) QholdsfortoTag = QholdsfortoTag x y 190 holdsfortagspecialise Q (x ⊗ y) QholdsfortoTag = QholdsfortoTag 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) 236 237 `_ : List Tag.Tag → Set 238 ` [] = ? 239 ` (x ∷ xs) = ? 240 241 test₁ : ` [ Tag.literal ] → ℕ 242 test₁ = {!!}
Note: See TracChangeset
for help on using the changeset viewer.