Changeset 2549 for Papers/polymorphic-variants-2012/Variants.agda
- Timestamp:
- Dec 10, 2012, 4:44:33 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/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 not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c 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∨c-true = inj₁ refl 50 ∨-cases false c b∨c-true = inj₂ b∨c-true 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 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.∧-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 177 234 178 235 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) 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.