Changeset 2549 for Papers/polymorphic-variants-2012/Variants.agda

Timestamp:

Dec 10, 2012, 4:44:33 PM (7 years ago)

Author:

mulligan

Message:

Not as straightforward as first imagined...

File:

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

Papers/polymorphic-variants-2012/Variants.agda

@@ -5 +5 @@
   open import Data.List
   open import Data.Nat hiding (_≟_)
-  open import Data.Sum
+  open import Data.Product hiding (map)
+  open import Data.Sum hiding (map)
   open import Data.Unit hiding (_≟_)
 
@@ -41 +42 @@
     not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
 
-    -- Properties of Boolean disjunction
+    -- Properties of Boolean disjunction and conjunction
     ∨-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
+    ∨-cases-true₁ : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true
+    ∨-cases-true₁ true  c b∨c-true = inj₁ refl
+    ∨-cases-true₁ false c b∨c-true = inj₂ b∨c-true
+
+    ∨-cases-true₂ : (b c : Bool) → b ≡ true ⊎ c ≡ true → b ∨ c ≡ true
+    ∨-cases-true₂ true  c b⊎c≡true = refl
+    ∨-cases-true₂ false c (inj₁ ())
+    ∨-cases-true₂ false c (inj₂ y) = y
+
+    ∧-cases-true₁ : (b c : Bool) → b ∧ c ≡ true → (b ≡ true) × (c ≡ true)
+    ∧-cases-true₁ true  c     b∧c≡true = refl , b∧c≡true
+    ∧-cases-true₁ false true  b∧c≡true = b∧c≡true , refl
+    ∧-cases-true₁ false false b∧c≡true = b∧c≡true , b∧c≡true
+
+    ∧-cases-true₂ : (b c : Bool) → (b ≡ true) × (c ≡ true) → (b ∧ c) ≡ true
+    ∧-cases-true₂ true  c b≡true×c≡true = proj₂ b≡true×c≡true
+    ∧-cases-true₂ false c b≡true×c≡true = proj₁ b≡true×c≡true
 
     -- Boolean equality
@@ -167 +182 @@
     _∈_ ⦃ 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 !}
+    _⊆_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → List α → List α → Bool
+    _⊆_ ⦃ DS ⦄ sub sup = all (λ x → x ∈ sup) sub
+
+    -- (DeqSet._≈_ DS x x ∨ x ∈ xs) ∧ foldr _∧_ true (map (λ x' → DeqSet._≈_ DS x' x ∨ x' ∈ xs) xs) ≡ true
+    ⊆-reflexive : {α : Set} → ⦃ DS : DeqSet α ⦄ → (l : List α) → l ⊆ l ≡ true
+    ⊆-reflexive ⦃ DS ⦄ []       = refl
+    ⊆-reflexive ⦃ DS ⦄ (x ∷ xs)
+      rewrite
+        ⊆-reflexive xs = {!!} -- MissingStandardLibrary.∧-cases-true₂ (DeqSet._≈_ DS x x ∨ x ∈ xs) _ (x≈x-∨-x-∈-xs-≡-true , {!!})
+      where
+        x≈x-∨-x-∈-xs-≡-true : (DeqSet._≈_ DS x x) ∨ (x ∈ xs) ≡ true
+        x≈x-∨-x-∈-xs-≡-true = MissingStandardLibrary.∨-cases-true₂ _ _ (inj₁ $ DeqSet.≈-true₂ DS x x refl)
+
+        xs-⊆-xs-≡-true : xs ⊆ xs ≡ true
+        xs-⊆-xs-≡-true = ⊆-reflexive xs
+
+    x∷xs-⊆-ys-to-x-∈-ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊆ ys ≡ true → x ∈ ys ≡ true
+    x∷xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x xs []         x∷xs⊆ys = x∷xs⊆ys
+    x∷xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊆ys with x ∈ xs'
+    ... | true  = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x'
+    ... | false = MissingStandardLibrary.∨-cases-true₂ (DeqSet._≈_ DS x x') false $ inj₁ x≈x'≡true
+      where
+        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
+        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
+
+        x≈x'∨false≡true : DeqSet._≈_ DS x x' ∨ false ≡ true
+        x≈x'∨false≡true = proj₁ $ x≈x'∨false≡true∧foldr≡true
+
+        x≈x'≡true : DeqSet._≈_ DS x x' ≡ true
+        x≈x'≡true with MissingStandardLibrary.∨-cases-true₁ (DeqSet._≈_ DS x x') false x≈x'∨false≡true
+        ... | inj₁ p = p
+        ... | inj₂ ()
+
+    -- Oh `destruct' how I miss thee...
+    false≡true-to-α : {α : Set} → false ≡ true → α
+    false≡true-to-α ()
+
+    x∷xs-⊆-ys-to-xs-⊆-ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊆ ys ≡ true → xs ⊆ ys ≡ true
+    x∷xs-⊆-ys-to-xs-⊆-ys ⦃ DS ⦄ x xs ys x∷xs⊆ys with x ∈ ys
+    ... | true  = x∷xs⊆ys
+    ... | false = false≡true-to-α x∷xs⊆ys
+
+    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → x ∈ xs ≡ true → xs ⊆ ys ≡ true → x ∈ ys ≡ true
+    x-∈-xs-to-xs-⊆-ys-to-x-∈-ys ⦃ DS ⦄ x []        ys x∈xs≡true xs⊆ys≡true = false≡true-to-α x∈xs≡true
+    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
+    ... | 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)
+    ... | false | 〈 p 〉 = x-∈-xs-to-xs-⊆-ys-to-x-∈-ys x xs ys x∈xs≡true foldr-∧-≡-true
+      where
+        foldr-∧-≡-true : foldr _∧_ true (map (λ x → x ∈ ys) xs) ≡ true
+        foldr-∧-≡-true = proj₂ $ MissingStandardLibrary.∧-cases-true₁ (x' ∈ ys) _ xs⊆ys≡true
   
   module Random where
-  -- Random stuff
-
-    [_holds-for_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set
-    [ Q holds-for Tag.literal ] = (n : ℕ) → Q $ ↑ n
-    [ Q holds-for Tag.plus ]    = (x y : _) → Q $ x ⊕ y
-    [ Q holds-for Tag.times ]   = (x y : _) → Q $ x ⊗ y
-
-    holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) →
-      [ 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
-    holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y
-
-    -- The following is ported from `variants.ma'.
-
-    _∈_ : {α : Set} → Expression α → List Tag.Tag → Bool
-    tag ∈ []        = false
-    tag ∈ (x ∷ xs) = (Tag._≈_ (Tag.toTag tag) x) ∨ (tag ∈ xs)
-
-    record Subexpression (α : Set) (l : List Tag.Tag) : Set where
-      field
-        element   : Expression α
-        ∈-element : MissingStandardLibrary.toSet $ element ∈ l
-
-    -- The following two functions are coercions in Matita.
-    subexpression : List Tag.Tag → Set → Set
-    subexpression l = λ α → Subexpression α l
-
-    mkSubexpression : {α : Set} → (l : List Tag.Tag) → (e : Expression α) →
-      MissingStandardLibrary.toSet $ e ∈ l → Subexpression α l
-    mkSubexpression l e p = record { element = e; ∈-element = p }
-
-    -- Missing from the Agda standard library, seemingly.
-    member : {α : Set} → (α → α → Bool) → α → List α → Bool
-    member p e []       = false
-    member p e (x ∷ xs) = (p e x) ∨ (member p e xs)
+
+    `_ : List Tag.Tag → Set
+    ` [] = ?
+    ` (x ∷ xs) = ?
+
+    test₁ : ` [ Tag.literal ] → ℕ
+    test₁ = {!!}