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

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

Not as straightforward as first imagined...

File:
1 edited

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

 r2546 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 (_≟_) 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 _∈_ ⦃ 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₁ = {!!}
Note: See TracChangeset for help on using the changeset viewer.