module Variants where open import Data.Bool open import Data.Empty open import Data.List open import Data.Nat hiding (_≟_) open import Data.Sum open import Data.Unit hiding (_≟_) open import Function open import Relation.Nullary open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉) -- The following is ported from `test.ma'. data Expression (α : Set) : Set where ↑ : ℕ → Expression α _⊕_ : Expression α → Expression α → Expression α _⊗_ : Expression α → Expression α → Expression α module MissingStandardLibrary where toSet : Bool → Set toSet true = ⊤ toSet false = ⊥ not-not-elim : (b : Bool) → not (not b) ≡ b not-not-elim true = refl not-not-elim false = refl not-self-adjoint₁ : (b c : Bool) → not b ≡ c → b ≡ not c not-self-adjoint₁ true true () not-self-adjoint₁ true false not-b≡c = refl not-self-adjoint₁ false true not-b≡c = refl not-self-adjoint₁ false false () not-self-adjoint₂ : (b c : Bool) → b ≡ not c → not b ≡ c not-self-adjoint₂ b c b≡not-c = sym \$ not-self-adjoint₁ c b \$ sym \$ b≡not-c _≈_ : Bool → Bool → Bool true ≈ c = c false ≈ c = not c ≈-reflexive : (b : Bool) → b ≈ b ≡ true ≈-reflexive true = refl ≈-reflexive false = refl ≈-true₁ : (b c : Bool) → b ≈ c ≡ true → b ≡ c ≈-true₁ true true b≈c-true = refl ≈-true₁ true false () ≈-true₁ false true b≈c-true = b≈c-true ≈-true₁ false false b≈c-true = refl ≈-true₂ : (b c : Bool) → b ≡ c → b ≈ c ≡ true ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c -- Tags, and their equality module Tag where data Tag : Set where literal : Tag plus : Tag times : Tag _≈_ : Tag → Tag → Bool literal ≈ literal = true plus ≈ plus = true times ≈ times = true _ ≈ _ = false _≉_ : Tag → Tag → Bool l ≉ r = not \$ l ≈ r ≈-≉-dual : (l r : Tag) → l ≈ r ≡ not (l ≉ r) ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl ≈-reflexive : (l : Tag) → l ≈ l ≡ true ≈-reflexive literal = refl ≈-reflexive plus = refl ≈-reflexive times = refl ≈-true₁ : (l r : Tag) → l ≈ r ≡ true → l ≡ r ≈-true₁ literal literal l≈r-true = refl ≈-true₁ literal plus () ≈-true₁ literal times () ≈-true₁ plus literal () ≈-true₁ plus plus l≈r-true = refl ≈-true₁ plus times () ≈-true₁ times literal () ≈-true₁ times plus () ≈-true₁ times times l≈r-true = refl ≈-true₂ : (l r : Tag) → l ≡ r → l ≈ r ≡ true ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r ≉-true₁ : (l r : Tag) → l ≉ r ≡ true → l ≢ r ≉-true₁ literal literal () ≉-true₁ literal plus l≉r-true = λ () ≉-true₁ literal times l≉r-true = λ () ≉-true₁ plus literal l≉r-true = λ () ≉-true₁ plus plus () ≉-true₁ plus times l≉r-true = λ () ≉-true₁ times literal l≉r-true = λ () ≉-true₁ times plus l≉r-true = λ () ≉-true₁ times times () ≉-true₂ : (l r : Tag) → l ≢ r → l ≉ r ≡ true ≉-true₂ literal literal l≢r = ⊥-elim \$ l≢r refl ≉-true₂ literal plus l≢r = refl ≉-true₂ literal times l≢r = refl ≉-true₂ plus literal l≢r = refl ≉-true₂ plus plus l≢r = ⊥-elim \$ l≢r refl ≉-true₂ plus times l≢r = refl ≉-true₂ times literal l≢r = refl ≉-true₂ times plus l≢r = refl ≉-true₂ times times l≢r = ⊥-elim \$ l≢r refl ≈-≉-decidable : (l r : Tag) → l ≈ r ≡ true ⊎ l ≉ r ≡ true ≈-≉-decidable literal literal = inj₁ refl ≈-≉-decidable literal plus = inj₂ refl ≈-≉-decidable literal times = inj₂ refl ≈-≉-decidable plus literal = inj₂ refl ≈-≉-decidable plus plus = inj₁ refl ≈-≉-decidable plus times = inj₂ refl ≈-≉-decidable times literal = inj₂ refl ≈-≉-decidable times plus = inj₂ refl ≈-≉-decidable times times = inj₁ refl module DeqSet where record DeqSet (α : Set) : Set where constructor mkDeqSet field _≈_ : α → α → Bool _≉_ : α → α → Bool ≈-≉-dual : (l r : α) → l ≈ r ≡ not (l ≉ r) ≈-true₁ : (l r : α) → l ≈ r ≡ true → l ≡ r ≈-true₂ : (l r : α) → l ≡ r → l ≈ r ≡ true ≉-true₁ : (l r : α) → l ≉ r ≡ true → l ≢ r ≉-true₂ : (l r : α) → l ≢ r → l ≉ r ≡ true ≈-≉-decidable : (l r : α) → l ≈ r ≡ true ⊎ l ≉ r ≡ true Tag-DeqSet : DeqSet Tag.Tag Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable 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 [ 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 (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._≈_ (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)