Ignore:
Timestamp:
Dec 10, 2012, 4:44:33 PM (7 years ago)
Author:
mulligan
Message:

Not as straightforward as first imagined...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/Variants.agda

    r2546 r2549  
    55  open import Data.List
    66  open import Data.Nat hiding (_≟_)
    7   open import Data.Sum
     7  open import Data.Product hiding (map)
     8  open import Data.Sum hiding (map)
    89  open import Data.Unit hiding (_≟_)
    910
     
    4142    not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
    4243
    43     -- Properties of Boolean disjunction
     44    -- Properties of Boolean disjunction and conjunction
    4445    ∨-elim₂ : (b : Bool) → b ∨ true ≡ true
    4546    ∨-elim₂ true  = refl
    4647    ∨-elim₂ false = refl
    4748
    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
    5166
    5267    -- Boolean equality
     
    167182    _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs)
    168183
    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
    177234 
    178235  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.