Changeset 2546

Timestamp:

Dec 7, 2012, 6:49:40 PM (7 years ago)

Author:

mulligan

Message:

Some more progress.

File:

• Papers/polymorphic-variants-2012/Variants.agda (modified) (7 diffs)

Papers/polymorphic-variants-2012/Variants.agda

@@ -22 +22 @@
   module MissingStandardLibrary where
 
+    -- Lifting Bool into Set
     toSet : Bool → Set
     toSet true  = ⊤
     toSet false = ⊥
 
+    -- Properties of Boolean negation
     not-not-elim : (b : Bool) → not (not b) ≡ b
     not-not-elim true  = refl
@@ -39 +41 @@
     not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
 
+    -- Properties of Boolean disjunction
+    ∨-elim₂ : (b : Bool) → b ∨ true ≡ true
+    ∨-elim₂ true  = refl
+    ∨-elim₂ false = refl
+
+    ∨-cases : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true
+    ∨-cases true  c b∨c-true = inj₁ refl
+    ∨-cases false c b∨c-true = inj₂ b∨c-true
+
+    -- Boolean equality
     _≈_ : Bool → Bool → Bool
     true  ≈ c = c
@@ -63 +75 @@
       plus    : Tag
       times   : Tag
+
+    toTag : {α : Set} → Expression α → Tag
+    toTag (↑ _)   = literal
+    toTag (_ ⊕ _) = plus
+    toTag (_ ⊗ _) = times
 
     _≈_ : Tag → Tag → Bool
@@ -136 +153 @@
         _≈_           : α → α → Bool
         _≉_           : α → α → Bool
-
         ≈-≉-dual      : (l r : α) → l ≈ r ≡ not (l ≉ r)
         ≈-true₁       : (l r : α) → l ≈ r ≡ true → l ≡ r
@@ -146 +162 @@
     Tag-DeqSet : DeqSet Tag.Tag
     Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable
+
+    _∈_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → α → List α → Bool
+    _∈_ ⦃ DS ⦄ e []       = false
+    _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs)
+
+    _⊂_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → List α → List α → Bool
+    _⊂_ ⦃ DS ⦄ sub sup = all (λ x → x ∈ sup) sub
+
+    x∷xs-⊂-to-∈ : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊂ ys ≡ true → x ∈ ys ≡ true
+    x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs []         x∷xs⊂ys = x∷xs⊂ys
+    x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊂ys with x ∈ xs' | inspect (λ x → x ∈ xs') $ x
+    ... | true  | 〈 p 〉 = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x'
+    ... | false | 〈 p 〉 = {!? $ MissingStandardLibrary.∨-cases ? ? p !}
   
   module Random where
   -- Random stuff
-
-    Tag-DeqSet : DeqSet.DeqSet Tag.Tag
-    Tag-DeqSet = {!!}
-
-    toTag : {α : Set} → Expression α → Tag.Tag
-    toTag (↑ _)   = Tag.literal
-    toTag (_ ⊕ _) = Tag.plus
-    toTag (_ ⊗ _) = Tag.times
 
     [_holds-for_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set
@@ -164 +185 @@
 
     holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) →
-      [ Q holds-for (toTag x) ] → Q x
+      [ Q holds-for (Tag.toTag x) ] → Q x
     holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n
     holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y
@@ -173 +194 @@
     _∈_ : {α : Set} → Expression α → List Tag.Tag → Bool
     tag ∈ []        = false
-    tag ∈ (x ∷ xs) = (Tag._≈_ (toTag tag) x) ∨ (tag ∈ xs)
+    tag ∈ (x ∷ xs) = (Tag._≈_ (Tag.toTag tag) x) ∨ (tag ∈ xs)
 
     record Subexpression (α : Set) (l : List Tag.Tag) : Set where