open import Relation.Nullary using (Dec) open import Relation.Binary.PropositionalEquality using (_≡_) module SetProperties {A : Set}(_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where -- Set Properties, with sets implemented by lists ------------------------------------------------------------------------ module PropEq where open import Relation.Nullary using (¬_) open import Relation.Binary.PropositionalEquality using (refl) open import Data.List using (List; _∷_) --------------------------------------- -- Propositional Equality Properties -- --------------------------------------- ------------------------------------------ sym≢ : ∀ {a b : A} → ¬ (a ≡ b) → ¬ (b ≡ a) sym≢ p refl = p refl -------------------- ----------------------------------------------------------------------- lem_x≡y→ax≡ay : ∀ {a : A} {x y : List A} → (x ≡ y) → (a ∷ x) ≡ (a ∷ y) lem_x≡y→ax≡ay {a} {x} {.x} refl = refl --------------------------------------- -- end of module PropEq ------------------------------------------------------------------------ module Delete where open import Relation.Nullary using (yes; no; ¬_) open import Relation.Binary.PropositionalEquality using (refl) open import Data.List using (List; []; [_]; _∷_) open import Data.List.Any using (here; there) open import Data.Empty using (⊥-elim) ----------------------------- delete : A → List A → List A delete _ [] = [] delete a (b ∷ x) with a ≟ b delete a (.a ∷ x) | yes refl = delete a x delete a (b ∷ x) | no _ = b ∷ delete a x ---------------------------------------------- ------------------------------------------------------------------------ -- Delete Properties ------------------------------------------------------------------------ ------------------------------------------------------------------------ del[] : ∀ {a : A} → delete a [] ≡ [] del[] = refl ------------------------------------------------------------------------ ------------------------------------------------------------------- lem_delaa : ∀ {a : A} {x : List A} → delete a (a ∷ x) ≡ delete a x lem_delaa {a} {x} with a ≟ a -- Pitty: have to test a ≟ a. lem_delaa {a} {x} | yes refl = refl lem_delaa {a} {x} | no a≢a = ⊥-elim (a≢a refl) ------------------------------------------------- ----------------------------------------------------------------------------------------- lem_delb≢a_ax : ∀ {a b : A} {x : List A} → ¬ (a ≡ b) → delete b (a ∷ x) ≡ a ∷ delete b x lem_delb≢a_ax {a} {b} {x} a≢b with b ≟ a -- Testing with a ≟ b instead of b ≟ a here does not succeed ... :-( lem_delb≢a_ax {a} {.a} {x} a≢b | yes refl = ⊥-elim (a≢b refl) lem_delb≢a_ax {a} {b} {x} a≢b | no ¬p = refl ---------------------------------------------- --------------------------------------------------------------------------------- lem_del_idempotent : ∀ (a : A) (x : List A) → delete a (delete a x) ≡ delete a x -- proof is a hack... lem_del_idempotent a [] = refl lem_del_idempotent a (b ∷ x) with a ≟ b lem_del_idempotent a (.a ∷ x) | yes refl rewrite (lem_delaa {a} {x}) with a ≡ a -- hack... lem_del_idempotent a (.a ∷ x) | yes refl | _ rewrite (lem_del_idempotent a x) = refl lem_del_idempotent a (b ∷ x) | no a≢b rewrite (lem_delb≢a_ax {b} {a} {x} (sym≢ a≢b)) with a ≟ b -- Pitty: have to write a ≟ b again lem_del_idempotent a (.a ∷ x) | no a≢b | yes refl = ⊥-elim (a≢b refl) lem_del_idempotent a (b ∷ x) | no a≢b | no _ rewrite (lem_del_idempotent a x) = refl ---------------------------------------------------------------------------------------- -- end of module Delete ------------------------------------------------------------------------ module Member where open import Relation.Nullary using (yes; no; ¬_) open import Relation.Binary.PropositionalEquality using (refl) open import Data.List using (List; []; [_]; _∷_) open import Data.List.Any using (here; there) open Data.List.Any.Membership-≡ using (_∈_) open import Data.Empty using (⊥-elim) open import Data.Sum using (_⊎_; inj₁; inj₂) --------------------------------------------------------- -- Membership Properties --------------------------------------------------------- ------------------------------------------------------------------------ lem_a∉[] : ∀ {A : Set} {a : A} → ¬ (a ∈ []) lem_a∉[] {A} {a} = λ () ------------------------------------------------------------------------ --------------------------------------------------------------------------------------- lem∉→∉∷ : ∀ {A : Set} {a b : A} {x : List A} → ¬ (a ≡ b) → ¬ (a ∈ x) → ¬ (a ∈ (b ∷ x)) lem∉→∉∷ {A} {a} {b} {x} a≢b a∉x (here a≡b) = ⊥-elim (a≢b a≡b) lem∉→∉∷ {A} {a} {b} {x} a≢b a∉x (there a∈bx) = ⊥-elim (a∉x a∈bx) ----------------------------------------------------------------- -------------------------------------------------------- lem∈Hd : ∀ {A : Set } {a : A} {x : List A} → a ∈ (a ∷ x) lem∈Hd {A} {a} {x} = here refl ------------------------------ -------------------------------- lema∈[a] : ∀ {a : A} → a ∈ [ a ] lema∈[a] {a} = here refl ------------------------- ----------------------------------------------------------- lem∈[b]→≡b : ∀ {A : Set} {a b : A} → (a ∈ [ b ]) → (a ≡ b) lem∈[b]→≡b {A} {a} {b} (here a≡b) = a≡b lem∈[b]→≡b {A} {a} {b} (there a∈[]) = ⊥-elim (lem_a∉[] {A} {a} a∈[]) -------------------------------------------------------------------- ----------------------------------------------------------------------- lem≡b→∈bx : ∀ {A : Set} {a b : A} {x : List A} → (a ≡ b) → a ∈ (b ∷ x) lem≡b→∈bx a≡b = here a≡b ------------------------- ------------------------------------------------- lem≢b→∉[b] : ∀ {a b} → ¬ (a ≡ b) → ¬ (a ∈ [ b ]) lem≢b→∉[b] {a} {b} a≢b with a ≟ b lem≢b→∉[b] {a} {.a} a≢b | yes refl = λ _ → a≢b refl lem≢b→∉[b] {a} {b} a≢b | no p = λ a∈[b] → a≢b (lem∈[b]→≡b a∈[b]) ---------------------------------------------------------------- ------------------------------------------------------------------- lem∈→∈∷ : ∀ {A : Set} {a b : A} {x : List A} → a ∈ x → a ∈ (b ∷ x) lem∈→∈∷ a∈x = there a∈x ------------------------ ---------------------------------------------------------- {- lem∈Or∉ : ∀ {a : 𝕍ar} {x : 𝕍ars} → (a ∈ x) ⊎ (¬ (a ∈ x)) lem∈Or∉ {a} {[]} = inj₂ (lem_a∉[] {𝕍ar} {a}) lem∈Or∉ {a} {b ∷ x} with a ≟ b lem∈Or∉ {a} {.a ∷ x} | yes refl = inj₁ (here refl) lem∈Or∉ {a} {b ∷ x} | no a≢b with lem∈Or∉ {a} {x} lem∈Or∉ {a} {b ∷ x} | no a≢b | inj₁ a∈x = inj₁ (lem∈→∈∷ {𝕍ar} {a} {b} {x} a∈x) lem∈Or∉ {a} {b ∷ x} | no a≢b | inj₂ a∉x = inj₂ (lem∉→∉∷ {𝕍ar} {a} {b} {x} a≢b a∉x) -} -------------------------------------------------------------------------------------- -------------------------------------------------------------------------- lem∈bx→≢b→∈x : ∀ {a b : A} {x : List A} → a ∈ (b ∷ x) → ¬ (a ≡ b) → a ∈ x lem∈bx→≢b→∈x {a} {b} {x} (here a≡b) a≢b = ⊥-elim (a≢b a≡b) lem∈bx→≢b→∈x {a} {b} {x} (there a∈x) a≢b = a∈x ----------------------------------------------- ------------------------------------------------------------- lem∉∷→∉ : ∀ {A : Set} {a b : A} {x : List A} → ¬ (a ∈ b ∷ x) → ¬ (a ∈ x) lem∉∷→∉ {A} {a} {b} {x} a≢bx a∈x = a≢bx (there a∈x) ---------------------------------------------------- ------------------------------------------------------------------------ -- List Membership and Propositional Equality Properties ------------------------------------------------------------------------ ----------------------------------------------------------------------------- lem_∈bx→≢b→∈x : ∀ {a b : A} {x : List A} → ¬ (a ≡ b) → (a ∈ b ∷ x) → (a ∈ x) lem_∈bx→≢b→∈x {a} {.a} {x} a≢b (here refl) = ⊥-elim (a≢b refl) lem_∈bx→≢b→∈x {a} {b} {x} a≢b (there a∈x) = a∈x ------------------------------------------------- ------------------------------------------------------------------ lem≡→∈ : ∀ {A : Set} {a b : A} {x : List A} → a ≡ b → a ∈ (b ∷ x) lem≡→∈ {a} {b} {x} a≡b = here a≡b ---------------------------------- ------------------------------------------------------- lem∈→≡ : ∀ {A : Set} {a b : A} → (a ∈ [ b ]) → (a ≡ b) lem∈→≡ {A} {a} {.a} (here refl) = refl lem∈→≡ {A} {a} {b} (there a∈[]) = ⊥-elim (lem_a∉[] {A} {a} a∈[]) ----------------------------------------------------------------- ----------------------------------------------------------- lem∉→≢ : ∀ {A : Set} {a b : A} → ¬ (a ∈ [ b ]) → ¬ (a ≡ b) lem∉→≢ {A} {a} {b} a∉[b] k∈[a] = a∉[b] (here k∈[a]) ---------------------------------------------------- ----------------------------------------------------------- lem≢→∉ : ∀ {A : Set} {a b : A} → ¬ (a ≡ b) → ¬ (a ∈ [ b ]) lem≢→∉ {A} {a} {b} a≢b (here a∈[b]) = a≢b a∈[b] lem≢→∉ {A} {a} {b} a≢b (there a∈[b]) = ⊥-elim (lem_a∉[] a∈[b]) --------------------------------------------------------------- -------------------------------------------------------------------------------------- lem∈x→∈HdTlx : ∀ { A : Set } {a b : A} {x : List A} → a ∈ (b ∷ x) → (a ≡ b) ⊎ (a ∈ x) lem∈x→∈HdTlx (here a∈b∷x) = inj₁ a∈b∷x lem∈x→∈HdTlx (there a∈b∷x) = inj₂ a∈b∷x ---------------------------------------- ----------------------------------------------------------------------------------------- lem∉→∉∷ : ∀ {A : Set} (a b : A) (x : List A) → ¬ (a ∈ x) → ¬ (a ≡ b) → ¬ (a ∈ (b ∷ x)) lem∉→∉∷ a b x a∉x a≢b a∈bx with lem∈x→∈HdTlx a∈bx ... | (inj₁ a≡b) = a≢b a≡b ... | (inj₂ a∈x) = a∉x a∈x ---------------------------------- -------------------------------------------------------------------- lem_≡→≡∷ : ∀ {a : A} {x y : List A} → (x ≡ y) → ((a ∷ x) ≡ (a ∷ y)) lem_≡→≡∷ {a} {x} {.x} refl = refl ---------------------------------- ----------------------------------------------------------- lemOcc2 : ∀ {A : Set} {v v' : A} → (v ∈ [ v' ]) → (v ≡ v') lemOcc2 {A} {v} {v'} (here v≡v') = v≡v' lemOcc2 {A} {v} {v'} (there v∈[]) = ⊥-elim (lem_a∉[] {A} {v} v∈[]) ------------------------------------------------------------------- ------------------------------------------------------------------------- lemOcc0' : ∀ {A : Set} {v v' : A} {x : List A} → (v ≡ v') → v ∈ (v' ∷ x) lemOcc0' v≡v' = here v≡v' -------------------------- --------------------------------------------------------------------------- lem_a∉→b∈→a≢b : ∀ {a b : A} {x : List A} → ¬ (a ∈ x) → (b ∈ x) → ¬ (a ≡ b) lem_a∉→b∈→a≢b {a} {b} {x} a∉x b∈x with a ≟ b lem_a∉→b∈→a≢b {a} {.a} {x} a∉x b∈x | yes refl = ⊥-elim (a∉x b∈x) lem_a∉→b∈→a≢b {a} {b} {x} a∉x b∈x | no a≢b = a≢b ---------------------------------------------------- ------------------------------------------------------------------------------- lem_a∉bx→a∉x : ∀ {A : Set} {a b : A} {x : List A} → ¬ a ∈ (b ∷ x) → ¬ (a ∈ x) lem_a∉bx→a∉x {A} {a} {b} {x} a∉bx = λ z → a∉bx (there z) --------------------------------------------------------- -- end of module Member ------------------------------------------------------------------------ module MemberDelete where -- Lemmas involving ∈ and delete open import Relation.Nullary using (yes; no; ¬_) open import Relation.Binary.PropositionalEquality using (cong; refl; sym) open import Data.List using (List; []; [_]; _∷_) open import Data.List.Any using (here; there) open Data.List.Any.Membership-≡ using (_∈_) open import Data.Empty using (⊥-elim) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_; _≡⟨_⟩_; _∎) -- The open imports below cause an error. No need to use qualified names to refer to the imported names. Weird. -- open import SetProperties.Delete using (delete; lem_delaa; lem_delb≢a_ax) -- open import SetProperties.Member using (lem∉→∉∷; lem∉∷→∉; lem∈→∈∷; lem∈bx→≢b→∈x; lem_a∉[]; lem≡→∈; lem∈Hd) -- Definitions inside Delete and Member, which are inside SetProperties, are not parameterised by _≟_. Weird. ------------------------------------------------------------------------ -- Membership with Delete Properties ------------------------------------------------------------------------ -- Abbreviations -- (were used to avoid _≟_ as argument, but argument _≟_ was avoided by placing modules -- (that contain the names to abbreviate) inside module SetProperty). x≡y→ax≡ay : ∀ {a : A} {x y : List A} → (x ≡ y) → (a ∷ x) ≡ (a ∷ y) x≡y→ax≡ay = lem_x≡y→ax≡ay del : A → List A → List A del = delete delaa : ∀ {a : A} {x : List A} → del a (a ∷ x) ≡ del a x delaa = lem_delaa delb≢a_ax : ∀ {a b : A} {x : List A} → ¬ (a ≡ b) → del b (a ∷ x) ≡ a ∷ del b x delb≢a_ax = lem_delb≢a_ax ∉→∉∷ : ∀ {A : Set} {a b : A} {x : List A} → ¬ (a ≡ b) → ¬ (a ∈ x) → ¬ (a ∈ (b ∷ x)) ∉→∉∷ = lem∉→∉∷ ∉∷→∉ : ∀ {A : Set} {a b : A} {x : List A} → ¬ (a ∈ b ∷ x) → ¬ (a ∈ x) ∉∷→∉ = lem∉∷→∉ ∈→∈∷ : ∀ {A : Set} {a b : A} {x : List A} → a ∈ x → a ∈ (b ∷ x) ∈→∈∷ = lem∈→∈∷ ∈bx→≢b→∈x : ∀ {a b : A} {x : List A} → a ∈ (b ∷ x) → ¬ (a ≡ b) → a ∈ x ∈bx→≢b→∈x = lem∈bx→≢b→∈x a∉[] : ∀ {A : Set} {a : A} → ¬ (a ∈ []) a∉[] = lem_a∉[] ≡→∈ : ∀ {A : Set} {a b : A} {x : List A} → a ≡ b → a ∈ (b ∷ x) ≡→∈ = lem≡→∈ ∈Hd : ∀ {A : Set } {a : A} {x : List A} → a ∈ (a ∷ x) ∈Hd = lem∈Hd -- End of Abbreviations ----- -------------------------------------------------------- lem∉del : ∀ {a : A} {x : List A} → ¬ (a ∈ (del a x)) lem∉del {a} {[]} = λ () lem∉del {a} {b ∷ x'} with b ≟ a lem∉del {a} {.a ∷ x'} | yes refl rewrite (delaa {a} {x'}) = lem∉del {a} {x'} lem∉del {a} {b ∷ x'} | no a≢b rewrite (delb≢a_ax {b} {a} {x'} a≢b) = ∉→∉∷ {A} {a} {b} {del a x'} (sym≢ a≢b) (lem∉del {a} {x'}) -------------------------------------------------------------------- ------------------------------------------------------------------------------------ lem_∈delaa→∈dela : ∀ {a b : A} {x : List A} → a ∈ del b (b ∷ x) → a ∈ del b x lem_∈delaa→∈dela {a} {b} {x} a∈delbbx rewrite (delaa {b} {x}) = a∈delbbx ----------------------------------------------------------------------------- --------------------------------------------------------------------------------------- lemdel : ∀ {a : A} {x : List A} → ¬ (a ∈ x) → del a x ≡ x lemdel {a} {[]} _ = refl lemdel {a} {b ∷ x} a∉bx with a ≟ b lemdel {a} {.a ∷ x} a∉bx | yes refl = ⊥-elim (a∉bx (here refl)) lemdel {a} {b ∷ x} a∉bx | no a≢b = x≡y→ax≡ay (lemdel {a} {x} (∉∷→∉ {A} {a} {b} {x} a∉bx)) -------------------------------------------------------------------------------------------------------- -------------------------------------------------------------- lem∈del : ∀ {a b : A} {x : List A} → a ∈ (del b x) → a ∈ x lem∈del {a} {b} {[]} () lem∈del {a} {b} {c ∷ x'} a∈delb_cx' with a ≟ c lem∈del {a} {b} {.a ∷ x'} a∈delb_cx' | yes refl = here refl lem∈del {a} {b} {c ∷ x'} a∈delb_cx' | no a≢c with b ≟ c lem∈del {a} {b} {.b ∷ x'} a∈delb_cx' | no a≢c | yes refl rewrite (sym (delaa {b} {x'})) = ∈→∈∷ {A} {a} {b} {x'} (lem∈del {a} {b} {x'} (lem_∈delaa→∈dela {a} {b} {x'} a∈delb_cx')) lem∈del {a} {b} {c ∷ x'} a∈delb_cx' | no a≢c | no b≢c = ∈→∈∷ {A} {a} {c} {x'} (lem∈del {a} {b} {x'} (∈bx→≢b→∈x {a} {c} {del b x'} a∈delb_cx' a≢c)) ----------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------- lem∈x→≢b→∈x_b : ∀ {a b : A} {x : List A} → a ∈ x → ¬ (a ≡ b) → a ∈ del b x lem∈x→≢b→∈x_b {a} {b} {[]} a∈[] a≢b = ⊥-elim (a∉[] a∈[]) lem∈x→≢b→∈x_b {a} {b} {c ∷ x} a∈x a≢b with a ≟ c lem∈x→≢b→∈x_b {a} {b} {.a ∷ x} (here refl) a≢b | yes refl rewrite (delb≢a_ax {a} {b} {x} a≢b) = ≡→∈ refl lem∈x→≢b→∈x_b {a} {b} {.a ∷ x} (here refl) a≢b | no a≢c = ⊥-elim (a≢c refl) lem∈x→≢b→∈x_b {a} {b} {c ∷ x} (there a∈x) a≢b | no a≢c with b ≟ c lem∈x→≢b→∈x_b {a} {b} {.b ∷ x} (there a∈x) a≢b | no a≢c | yes refl = lem∈x→≢b→∈x_b {a} {b} {x} a∈x a≢b lem∈x→≢b→∈x_b {a} {b} {c ∷ x} (there a∈x) a≢b | no a≢c | no _ = ∈→∈∷ {A} {a} {c} {del b x} (lem∈x→≢b→∈x_b {a} {b} {x} a∈x a≢b) lem∈x→≢b→∈x_b {a} {b} {.a ∷ x} (there a∈x) a≢b | yes refl rewrite (delb≢a_ax {a} {b} {x} a≢b) = ∈→∈∷ {A} {a} {a} {del b x} (lem∈x→≢b→∈x_b {a} {b} {x} a∈x a≢b) ----------------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------------------------- lema∈a∷delbx : ∀ {a b : A} {x : List A} → (a ∈ (a ∷ del b x)) -- agda should deduce this, but it doesn't... lema∈a∷delbx {a} {b} {x} = ∈Hd {A} {a} {del b x} --------------------------------------------------------- ---------------------------------------------------------------------------------- lem_a≢b→a∈delbx : ∀ {a b : A} {x : List A} → ¬ (a ≡ b) → a ∈ del b (a ∷ x) lem_a≢b→a∈delbx {a} {b} {x} a≢b rewrite (delb≢a_ax {a} {b} {x} a≢b) = lema∈a∷delbx {a} {b} {x} ------------------------------------------------------------------------------------------------------- ------------------------------------------------------------------------------------------ lem≢b∉x→∉delbx : ∀ {a b : A} {x : List A} → ¬ (a ≡ b) → ¬ (a ∈ x) → ¬ (a ∈ del b x) lem≢b∉x→∉delbx {a} {b} {[]} _ a∉[] = lem_a∉[] {A} {a} lem≢b∉x→∉delbx {a} {b} {c ∷ x} a≢b a∉cx with a ≟ c lem≢b∉x→∉delbx {a} {b} {.a ∷ x} a≢b a∉cx | yes refl = ⊥-elim (a∉cx (here refl)) lem≢b∉x→∉delbx {a} {b} {c ∷ x} a≢b a∉cx | no a≢c with b ≟ c lem≢b∉x→∉delbx {a} {b} {.b ∷ x} a≢b a∉cx | no a≢c | yes refl = lem≢b∉x→∉delbx {a} {b} {x} a≢b (∉∷→∉ {A} {a} {b} {x} a∉cx) lem≢b∉x→∉delbx {a} {b} {c ∷ x} a≢b a∉cx | no a≢c | no b≢c = ∉→∉∷ {A} {a} {c} {del b x} a≢c (lem≢b∉x→∉delbx {a} {b} {x} a≢b (∉∷→∉ {A} {a} {c} {x} a∉cx)) -------------------------------------------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------- lem_∉x→∉delbx : ∀ (a b : A) (x : List A) → ¬ (a ∈ x) → ¬ (a ∈ del b x) lem_∉x→∉delbx a b [] a∉[] = a∉[] lem_∉x→∉delbx a b (c ∷ x) a∉cx with a ≟ c lem_∉x→∉delbx a b (.a ∷ x) a∉cx | yes refl = ⊥-elim (a∉cx (here refl)) lem_∉x→∉delbx a b (c ∷ x) a∉cx | no a≢c with b ≟ c lem_∉x→∉delbx a b (.b ∷ x) a∉bx | no a≢c | yes refl = lem_∉x→∉delbx a b x (∉∷→∉ {A} {a} {b} {x} a∉bx) lem_∉x→∉delbx a b (c ∷ x) a∉cx | no a≢c | no b≢c rewrite (delb≢a_ax {c} {b} {x} (sym≢ b≢c)) = ∉→∉∷ {A} {a} {c} {del b x} a≢c (lem_∉x→∉delbx a b x (∉∷→∉ {A} {a} {c} {x} a∉cx)) ------------------------------------ ------------------------------------------------------------------------------- lem_com_del : ∀ {a b : A} {x : List A} → (del a (del b x)) ≡ (del b (del a x)) lem_com_del {a} {b} {[]} = refl lem_com_del {a} {b} {c ∷ x} with a ≟ b lem_com_del {a} {.a} {c ∷ x} | yes refl = refl lem_com_del {a} {b} {c ∷ x} | no a≢b with c ≟ b -- b ≟ c (instead of c ≟ b) here causes a distressing error message :-( lem_com_del {a} {b} {.b ∷ x} | no a≢b | yes refl = begin del a (del b (b ∷ x)) ≡⟨ cong (λ x → del a x) (delaa {b} {x}) ⟩ del a (del b x) ≡⟨ lem_com_del {a} {b} {x} ⟩ del b (del a x) ≡⟨ sym (delaa {b} {del a x}) ⟩ del b (b ∷ del a x) ≡⟨ cong (λ x → del b x) (sym (delb≢a_ax {b} {a} {x} (sym≢ a≢b))) ⟩ del b (del a (b ∷ x)) ∎ lem_com_del {a} {b} {c ∷ x} | no a≢b | no c≢b with c ≟ a lem_com_del {a} {b} {.a ∷ x} | no a≢b | no c≢b | yes refl = begin del a (del b (a ∷ x)) ≡⟨ cong (λ x → del a x) (delb≢a_ax {a} {b} {x} a≢b) ⟩ del a (a ∷ del b x) ≡⟨ delaa {a} {del b x} ⟩ del a (del b x) ≡⟨ lem_com_del {a} {b} {x} ⟩ del b (del a x) ≡⟨ cong (λ x → del b x) (sym (delaa {a} {x})) ⟩ del b (del a (a ∷ x)) ∎ lem_com_del {a} {b} {c ∷ x} | no a≢b | no c≢b | no c≢a = begin del a (del b (c ∷ x)) ≡⟨ cong (λ x → del a x) (delb≢a_ax {c} {b} {x} c≢b) ⟩ del a (c ∷ del b x) ≡⟨ delb≢a_ax {c} {a} {del b x} c≢a ⟩ c ∷ del a (del b x) ≡⟨ cong (λ x → c ∷ x) (lem_com_del {a} {b} {x}) ⟩ c ∷ del b (del a x) ≡⟨ sym (delb≢a_ax {c} {b} {del a x} c≢b) ⟩ del b (c ∷ del a x) ≡⟨ cong (λ x → del b x) (sym (delb≢a_ax {c} {a} {x} c≢a)) ⟩ del b (del a (c ∷ x)) ∎ --- -- end of module MemberDelete ------------------------------------------------------------------------ module Union where open import Relation.Binary.PropositionalEquality using (refl) open import Data.List using (List; []; [_]; _∷_) open import Data.List.Any using (any) open import Data.List.Any using (here; there) -- compiles without this open import: weird... _∪_ : List A → List A → List A [] ∪ y = y (a ∷ x) ∪ y = a ∷ (x ∪ delete a y) ----------------------------------------- lem_x≡x∪[] : ∀ {x : List A} → x ≡ x ∪ [] lem_x≡x∪[] {[]} = refl lem_x≡x∪[] {a ∷ x'} with any (_≟_ a) [] lem_x≡x∪[] {a ∷ x'} | yes a∈[] = ⊥-elim ((lem_a∉[] {A} {a}) a∈[]) -- pitty to have to tell this lem_x≡x∪[] {a ∷ x'} | no a∉[] = lem_≡→≡∷ {a} {x'} {x' ∪ []} (lem_x≡x∪[] {x'}) ------------------------------------------------------------------------------ ----------------------------------------- lem_x∪[]≡x : ∀ {x : List A} → x ∪ [] ≡ x lem_x∪[]≡x = sym lem_x≡x∪[] --------------------------- ------------------------------------------------ lema∪[]→[a] : ∀ {a : A} → [ a ] ∪ [] ≡ a ∷ [] lema∪[]→[a] {a} = refl ----------------------- -- end of module Union ------------------------------------------------------------------------ module UnionDelete where ------------------------------------------------------------------------ -- List Union with Delete Properties ------------------------------------------------------------------------ ------------------------------------------------------------------------- lem∪del : ∀ {a : A} {x y : List A} → (a ∷ x) ∪ y ≡ a ∷ (x ∪ (delete a y)) lem∪del {a} {x} {y} = refl --------------------------- ----------------------------------------------------------------------------- lem∈x∪del₁ : ∀ (a b : A) (x y : List A) → a ∈ (x ∪ delete b y) → a ∈ (x ∪ y) -- these are mutually recursive lem∈∪ : ∀ {a b : A} {x y : List A} → a ∈ (x ∪ y) → ¬ (a ≡ b) → a ∈ (x ∪ delete b y) -------------------------------------------------------------------------------- -- lem∈x∪del₁ : ∀ (a b : A) (x y : List A) → a ∈ (x ∪ delete b y) → a ∈ (x ∪ y) lem∈x∪del₁ a b [] y a∈delby = lem∈del {a} {b} {y} a∈delby lem∈x∪del₁ a b (.a ∷ x) y (here refl) = here refl lem∈x∪del₁ a b (c ∷ x) y (there a∈x∪delcby) with a ≟ c lem∈x∪del₁ a b (.a ∷ x) y (there a∈x∪delcby) | yes refl = here refl lem∈x∪del₁ a b (c ∷ x) y (there a∈x∪delcby) | no a≢c = lem∈→∈∷ {A} {a} {c} {x ∪ delete c y} -- results in a ∈ (c ∷ (x ∪ del c y)) ≡ ((c ∷ x) ∪ y) ! (lem∈∪ {a} {c} {x} {y} -- results in a∈x∪delcy (lem∈x∪del₁ a b x y -- results in a∈x∪y (lem∈x∪del₁ a c x (delete b y) a∈x∪delcby) -- results in a∈x∪delby ) a≢c) --------------------------------------------------------------------------------------- -- lem∈∪ : ∀ {a b : A} {x y : List A} → a ∈ (x ∪ y) → ¬ (a ≡ b) → a ∈ (x ∪ delete b y) lem∈∪ {a} {b} {[]} {y} a∈y a≢b = lem∈x→≢b→∈x_b {a} {b} {y} a∈y a≢b lem∈∪ {a} {b} {.a ∷ x} {y} (here refl) a≢b = here refl lem∈∪ {a} {b} {c ∷ x} {y} (there a∈x∪delcy) a≢b with a ≟ c lem∈∪ {a} {b} {.a ∷ x} {y} (there a∈x∪delcy) a≢b | yes refl = here refl -- silly: if a≡c, 'there' should be 'here'... lem∈∪ {a} {b} {c ∷ x} {y} (there a∈x∪delcy) a≢b | no a≢c = lem∈→∈∷ {A} {a} {c} {x ∪ delete c (delete b y)} (lem∈∪ {a} {c} {x} {delete b y} (lem∈∪ {a} {b} {x} {y} (lem∈x∪del₁ a c x y a∈x∪delcy) a≢b) a≢c) ------------------------------------------------- -- end of module UnionDelete ------------------------------------------------------------------------ module MemberUnion where open import Relation.Binary.PropositionalEquality using (refl) open import Data.List using (List; [_]; _∷_) open import Data.List.Any open Data.List.Any.Membership-≡ using (_∈_) open import Data.Product using (_×_; _,_) ------------------------------------------------------------------------ -- List Membership with Union Properties ------------------------------------------------------------------------ ------------------------------------------------------- lem_a∈[a]∪x : ∀ {a : A} {x : List A} → a ∈ ([ a ] ∪ x) lem_a∈[a]∪x {a} {x} = lem∈Hd {A} {a} {delete a x} ------------------------------------------------- --------------------------------------------------------------- lem_a∈ax∪y : ∀ {a : A} {x y : List A} → a ∈ ((a ∷ x) ∪ y) lem_a∈ax∪y {a} {x} {y} = here refl ----------------------------------- ------------------------------------------------------------ lem∈x→∈x∪y : ∀ {a : A} {x y : List A} → a ∈ x → a ∈ (x ∪ y) lem∈x→∈x∪y {a} {[]} {y} () lem∈x→∈x∪y {a} {.a ∷ x'} {y} (here refl) = here refl lem∈x→∈x∪y {a} {b ∷ x'} {y} (there a∈x') = there (lem∈x→∈x∪y {a} {x'} {delete b y} a∈x') ------------------------------------------------------------------------------------------ -------------------------------------------------------------------------------- lem∈b∪x→≢b→∈x : ∀ {a b : A} {x : List A} → a ∈ ([ b ] ∪ x) → ¬ (a ≡ b) → a ∈ x lem∈b∪x→≢b→∈x {a} {b} {[]} a∈b∪[] a≢b = ⊥-elim (a≢b (lem∈→≡ a∈b∪[])) lem∈b∪x→≢b→∈x {a} {.a} {c ∷ x} (here refl) a≢b = ⊥-elim (a≢b refl) lem∈b∪x→≢b→∈x {a} {b} {c ∷ x} (there a∈cx) a≢b with a ≟ c lem∈b∪x→≢b→∈x {a} {b} {.a ∷ x} (there a∈cx) a≢b | yes refl = here refl lem∈b∪x→≢b→∈x {a} {b} {c ∷ x} (there a∈cx) a≢b | no a≢c = lem∈del {a} {b} a∈cx ------------------------------------------------------------------------------------ ---------------------------------------------------------------- lem∈x→∈b∪x : ∀ {a b : A} {x : List A} → a ∈ x → a ∈ ([ b ] ∪ x) lem∈x→∈b∪x {a} {b} {x} a∈x with (a ≟ b) lem∈x→∈b∪x {a} {.a} {x} a∈x | yes refl = here refl lem∈x→∈b∪x {a} {b} {x} a∈x | no a≢b = lem∈→∈∷ {A} {a} {b} (lem∈x→≢b→∈x_b {a} {b} {x} a∈x a≢b) --------------------------------------------------------------------------------------------------- -------------------------------------------------------------------------- lem∈ax→≢a→∈x : ∀ {a b : A} {x : List A} → (a ∈ b ∷ x) → ¬ (a ≡ b) → a ∈ x lem∈ax→≢a→∈x {a} {b} {x} (here a≡b) a≢b = ⊥-elim (a≢b a≡b) lem∈ax→≢a→∈x {a} {b} {x} (there a∈x) a≢b = a∈x ----------------------------------------------- ----------------------------------------------------------------------------- lem∈x∪y→∈bx∪y : ∀ (a b : A) (x y : List A) → a ∈ (x ∪ y) → a ∈ ((b ∷ x) ∪ y) lem∈x∪y→∈bx∪y a b x [] a∈x∪[] rewrite (sym (lem_x≡x∪[] {x})) with a ≡ a lem∈x∪y→∈bx∪y a b x [] a∈x∪[] | _ rewrite (sym (lem_x≡x∪[] {b ∷ x})) = lem∈→∈∷ {A} {a} {b} a∈x∪[] lem∈x∪y→∈bx∪y a b [] (.a ∷ y₁) (here refl) = lem∈x→∈b∪x {a} {b} (here refl) lem∈x∪y→∈bx∪y a b (.a ∷ x₁) (c ∷ y₁) (here refl) = there (here refl) lem∈x∪y→∈bx∪y a b [] (d ∷ y₁) (there a∈y₁) = lem∈x→∈b∪x {a} {b} (there a∈y₁) lem∈x∪y→∈bx∪y a b (c ∷ x₁) y (there a∈x₁∪delcy) with a ≟ b lem∈x∪y→∈bx∪y a .a (c ∷ x₁) y (there a∈x₁∪delcy) | yes refl = here refl lem∈x∪y→∈bx∪y a b (c ∷ x₁) y (there a∈x₁∪delcy) | no a≢b with any (_≟_ a) x₁ lem∈x∪y→∈bx∪y a b (c ∷ x₁) y (there a∈x₁∪delcy) | no a≢b | yes a∈x₁ = -- ∈ (b ∷ c ∷ x₁) → ∈ ((b ∷ c ∷ x₁) ∪ y) lem∈x→∈x∪y {a} {b ∷ c ∷ x₁} {y} -- ∈ x₁ → ∈ (b ∷ c ∷ x₁) (lem∈→∈∷ {A} {a} {b} {c ∷ x₁} (lem∈→∈∷ {A} {a} {c} {x₁} a∈x₁)) lem∈x∪y→∈bx∪y a b (c ∷ x₁) y (there a∈x₁∪delcy) | no a≢b | no a∉x₁ with a ≟ c lem∈x∪y→∈bx∪y a b (.a ∷ x₁) y (there a∈x₁∪delcy) | no a≢b | no a∉x₁ | yes refl = there (here refl) lem∈x∪y→∈bx∪y a b (c ∷ x₁) y (there a∈x₁∪delcy) | no a≢b | no a∉x₁ | no a≢c = lem∈→∈∷ {A} {a} {b} {(c ∷ x₁) ∪ delete b y} -- a ∈ (b ∷ ((c∷x₁) ∪ del b y)) ≡ (b∷c∷x₁ ∪ y) (lem∈∪ {a} {b} {c ∷ x₁} {y} -- a ∈ (c∷x₁) ∪ del b y |from a ∈ ((c∷x₁) ∪ y), a≢b -- Using: (c ∷ (x₁ ∪ del c y)) ≡ ((c∷x₁) ∪ y) (lem∈→∈∷ {A} {a} {c} {x₁ ∪ delete c y} -- a ∈ (c ∷ (x₁ ∪ del c y)) |from a ∈ (x₁ ∪ del c y) a∈x₁∪delcy) a≢b) -------------------------- ----------------------------------------------------------------------------- lem∈x∪y→∈x∪by : ∀ {a b : A} {x y : List A} → a ∈ (x ∪ y) → a ∈ (x ∪ (b ∷ y)) lem∈x∪y→∈x∪by {a} {b} {[]} {y} a∈y = lem∈→∈∷ {A} {a} {b} {y} a∈y lem∈x∪y→∈x∪by {a} {b} {.a ∷ x} {y} (here refl) = here refl lem∈x∪y→∈x∪by {a} {b} {c ∷ x} {y} (there a∈x∪delcy) = lem∈x∪y→∈bx∪y a c x (b ∷ y) (lem∈x∪y→∈x∪by {a} {b} {x} {y} (lem∈x∪del₁ a c x y a∈x∪delcy)) --------------------------------------- ------------------------------------------------------------------------------ lem∉x→∈x∪y→∈y : ∀ (a : A) (x y : List A) → ¬ (a ∈ x) → a ∈ (x ∪ y) → a ∈ y lem∉x→∈x∪y→∈y a [] y a∉x a∈y = a∈y lem∉x→∈x∪y→∈y a (.a ∷ x) y a∉ax (here refl) = ⊥-elim (a∉ax (lem∈Hd {A} {a} {x})) lem∉x→∈x∪y→∈y a (b ∷ x) y a∉bx (there a∈x∪delby) = lem∉x→∈x∪y→∈y a x y (lem∉∷→∉ a∉bx) (lem∈x∪del₁ a b x y a∈x∪delby) ---------------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------------------------- these are mutually recursive lem∈y→∈x∪y : ∀ {a : A} {x y : List A} → a ∈ y → a ∈ (x ∪ y) lem∈∪₁ : ∀ {a b : A} {x y : List A} → a ∈ (b ∷ (x ∪ y)) → a ∈ ((b ∷ x) ∪ y) ------------------------------------------------------------------------------- -- lem∈∪₁ : ∀ {a b : A} {x y : List A} → a ∈ (b ∷ (x ∪ y)) → a ∈ ((b ∷ x) ∪ y) lem∈∪₁ {a} {b} {x} {y} a∈b∷_x∪y with a ≟ b lem∈∪₁ {a} {.a} {x} {y} _ | yes refl with any (_≟_ a) (a ∷ x) lem∈∪₁ {a} {.a} {x} {y} _ | yes refl | yes a∈ax = lem∈x→∈x∪y {a} {a ∷ x} {y} a∈ax lem∈∪₁ {a} {.a} {x} {y} _ | yes refl | no a∉ax = ⊥-elim (a∉ax (here refl)) lem∈∪₁ {a} {b} {x} {y} (here a≡b) | no a≢b = ⊥-elim (a≢b a≡b) lem∈∪₁ {a} {b} {x} {y} (there a∈x∪y) | no a≢b with any (_≟_ a) x lem∈∪₁ {a} {b} {x} {y} (there a∈x∪y) | no a≢b | yes a∈x = lem∈x→∈x∪y {a} {b ∷ x} {y} (lem∈→∈∷ {A} {a} {b} {x} a∈x) lem∈∪₁ {a} {b} {x} {y} (there a∈x∪y) | no a≢b | no a∉x = lem∈x∪y→∈bx∪y a b x y (lem∈y→∈x∪y {a} {x} {y} (lem∉x→∈x∪y→∈y a x y a∉x a∈x∪y)) --------------------------------------------------------------- -- lem∈y→∈x∪y : ∀ {a : A} {x y : List A} → a ∈ y → a ∈ (x ∪ y) lem∈y→∈x∪y {a} {x} {[]} () lem∈y→∈x∪y {a} {[]} {.a ∷ y'} (here refl) = here refl lem∈y→∈x∪y {a} {b ∷ x'} {.a ∷ y'} (here refl) with a ≟ b lem∈y→∈x∪y {a} {.a ∷ x'} {.a ∷ y'} (here refl) | yes refl = lem_a∈ax∪y {a} {x'} {a ∷ y'} lem∈y→∈x∪y {a} {b ∷ x'} {.a ∷ y'} (here refl) | no a≢b = lem∈∪₁ {a} {b} {x'} {a ∷ y'} (lem∈→∈∷ {A} {a} {b} {x' ∪ (a ∷ y')} (lem∈y→∈x∪y {a} {x'} {a ∷ y'} (here refl))) lem∈y→∈x∪y {a} {x} {b ∷ y'} (there a∈y') = lem∈x∪y→∈x∪by {a} {b} {x} {y'} (lem∈y→∈x∪y {a} {x} {y'} a∈y') ---------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------- lem_a∈x∪ay : ∀ {a : A} {x y : List A} → a ∈ (x ∪ (a ∷ y)) lem_a∈x∪ay {a} {[]} {y} = here refl lem_a∈x∪ay {a} {b ∷ x} {y} with a ≟ b lem_a∈x∪ay {a} {.a ∷ x} {y} | yes refl = here refl lem_a∈x∪ay {a} {b ∷ x} {y} | no a≢b = lem∈x∪y→∈bx∪y a b x (a ∷ y) (lem_a∈x∪ay {a} {x} {y}) ---------------------------------------------------------------------------------------------- ------------------------------------------------------------------------------- lem_a∉x→a∈y→a∈x∪y : ∀ (a : A) (x y : List A) → ¬ (a ∈ x) → a ∈ y → a ∈ (x ∪ y) lem_a∉x→a∈y→a∈x∪y a [] y a∉x a∈y = a∈y lem_a∉x→a∈y→a∈x∪y a (b ∷ x) [] a∉bx () lem_a∉x→a∈y→a∈x∪y a (b ∷ x) (.a ∷ y) a∉bx (here refl) = lem_a∈x∪ay {a} {b ∷ x} {y} lem_a∉x→a∈y→a∈x∪y a (b ∷ x) (c ∷ y) a∉bx (there a∈y) = lem∈x∪y→∈x∪by {a} {c} {b ∷ x} {y} (lem_a∉x→a∈y→a∈x∪y a (b ∷ x) y a∉bx a∈y) ----------------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------------------------------------------------- lem∈bx∪y→≢b→∈x∪y : ∀ {a b : A} {x y : List A} → a ∈ ((b ∷ x) ∪ y) → ¬ (a ≡ b) → a ∈ (x ∪ y) lem∈bx∪y→≢b→∈x∪y {a} {b} {x} {y} (here a≡b) a≢b = ⊥-elim (a≢b a≡b) lem∈bx∪y→≢b→∈x∪y {a} {b} {x} {y} (there a∈x∪y) a≢b = lem∈x∪del₁ a b x y a∈x∪y ------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------- lem∉x→≢b→∉[b]∪x : ∀ {a b : A} {x : List A} → ¬ (a ∈ x) → ¬ (a ≡ b) → ¬ (a ∈ ([ b ] ∪ x)) lem∉x→≢b→∉[b]∪x {a} {b} {x} a∉x a≢b rewrite (lem_delb≢a_ax {a} {b} {x} a≢b) = lem∉→∉∷ {A} {a} {b} {delete b x} a≢b (lem≢b∉x→∉delbx {a} {b} {x} a≢b a∉x) --------------------------------------------------------------------------------------------------------------------- -------------------------------------------------------------------------------------- lem∉x∉y→∉x∪y : ∀ {a : A} {x y : List A} → (¬ (a ∈ x)) × (¬ (a ∈ y)) → ¬ (a ∈ (x ∪ y)) lem∉x∉y→∉x∪y {a} {[]} {y} (a∉[] , a∉y) a∈x∪y = ⊥-elim (a∉y a∈x∪y) lem∉x∉y→∉x∪y {a} {b ∷ x'} {y} (a∉bx' , a∉y) a∈bx'∪y with a ≟ b lem∉x∉y→∉x∪y {a} {.a ∷ x'} {y} (a∉bx' , a∉y) a∈bx'∪y | yes refl = ⊥-elim (a∉bx' (here refl)) lem∉x∉y→∉x∪y {a} {b ∷ x'} {y} (a∉bx' , a∉y) a∈bx'∪y | no a≢b = lem∉x∉y→∉x∪y {a} {x'} {y} (a∉x' , a∉y) a∈x'∪y where a∉x' = λ z → a∉bx' (there z) a∈x'∪y = lem∈bx∪y→≢b→∈x∪y {a} {b} {x'} {y} a∈bx'∪y a≢b ---------------------------------------------------------------- ----------------------------------------------------------------------------- lem∉∪→∉ : ∀ {a : A} {x y : List A} → ¬ (a ∈ x ∪ y) → (¬ (a ∈ x) × ¬ (a ∈ y)) lem∉∪→∉ {a} {x} {y} a∈xy = (λ a∈x → a∈xy (lem∈x→∈x∪y a∈x)) , (λ a∈y → a∈xy (lem∈y→∈x∪y {a} {x} {y} a∈y)) --------------------------------------------------------------------------------------------------------- ---------------------------------------------------------------------------- lem∈x∪y→∈xOr∈y : ∀ (a : A) (x y : List A) → a ∈ (x ∪ y) → (a ∈ x) ⊎ (a ∈ y) lem∈x∪y→∈xOr∈y a [] (b ∷ y') (here a∈y) = inj₂ (here a∈y) lem∈x∪y→∈xOr∈y a [] (b ∷ y') (there a∈y) = inj₂ (there a∈y) lem∈x∪y→∈xOr∈y a (b ∷ x') [] (here a∈x) = inj₁ (here a∈x) lem∈x∪y→∈xOr∈y a (b ∷ x') [] (there a∈bx') with lem∈x∪y→∈xOr∈y a x' [] a∈bx' lem∈x∪y→∈xOr∈y a (b ∷ x') [] (there a∈bx') | (inj₁ a∈x') = inj₁ (there a∈x') lem∈x∪y→∈xOr∈y a (b ∷ x') [] (there a∈bx') | (inj₂ a∈[]) = ⊥-elim (lem_a∉[] a∈[]) lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p with any (_≟_ a) (b ∷ x') lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p | yes a∈bx' with a ≟ b lem∈x∪y→∈xOr∈y a (.a ∷ x') (c ∷ y') p | yes a∈bx' | yes refl = inj₁ (here refl) lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p | yes a∈bx' | no a≢b = inj₁ a∈bx' lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p | no a∉bx' with any (_≟_ a) (c ∷ y') lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p | no a∉bx' | (yes a∈cy') with a ≟ c lem∈x∪y→∈xOr∈y a (b ∷ x') (.a ∷ y') p | no a∉bx' | (yes a∈cy') | yes refl = inj₂ (here refl) lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p | no a∉bx' | (yes a∈cy') | no a≢c = inj₂ a∈cy' lem∈x∪y→∈xOr∈y a (b ∷ x') (c ∷ y') p | no a∉bx' | (no a∉cy') = ⊥-elim ((lem∉x∉y→∉x∪y {a} {b ∷ x'} {c ∷ y'} (a∉bx' , a∉cy')) p) lem∈x∪y→∈xOr∈y a [] [] () --------------------------- ------------------------------------------------------------------------------------- lem∉both→∉∪ : ∀ {a : A} {x y : List A} → (¬ (a ∈ x)) × (¬ (a ∈ y)) → ¬ (a ∈ (x ∪ y)) lem∉both→∉∪ {a} {x} {y} (a∉x , a∉y) a∈xy with lem∈x∪y→∈xOr∈y a x y a∈xy ... | (inj₁ inx) = a∉x inx ... | (inj₂ iny) = a∉y iny -------------------------------------------------------- -------------------------------------------------------------------------------------------------- lem∈x∪y→≢b→∈x∪delby : ∀ {a b : A} {x y : List A} → a ∈ (x ∪ y) → ¬ (a ≡ b) → a ∈ (x ∪ delete b y) lem∈x∪y→≢b→∈x∪delby {a} {b} {[]} {y} a∈y a≢b = lem∈x→≢b→∈x_b {a} {b} {y} a∈y a≢b lem∈x∪y→≢b→∈x∪delby {a} {b} {.a ∷ x} {y} (here refl) a≢b = here refl lem∈x∪y→≢b→∈x∪delby {a} {b} {c ∷ x} {y} (there a∈x∪delcy) a≢b = lem∈x∪y→∈bx∪y a c x (delete b y) (lem∈x∪y→≢b→∈x∪delby {a} {b} {x} {y} (lem∈x∪del₁ a c x y a∈x∪delcy) a≢b) ------------------------------------------- ---------------------------------------------------------------------------- lem∈x∪del : ∀ {a b : A} {x y : List A} → a ∈ (x ∪ delete b y) → a ∈ (x ∪ y) lem∈x∪del {a} {b} {x} {y} a∈x∪delby with lem∈x∪y→∈xOr∈y a x (delete b y) a∈x∪delby lem∈x∪del {a} {b} {x} {y} a∈x∪delby | inj₁ a∈x = lem∈x→∈x∪y {a} {x} {y} a∈x lem∈x∪del {a} {b} {x} {y} a∈x∪delby | inj₂ a∈delby = lem∈y→∈x∪y {a} {x} {y} (lem∈del {a} {b} {y} a∈delby) ---------------------------------------------------------------------------------------------------------- -- end module MemberUnion ------------------------------------------------------------------------ module Subset where open import Data.List.Any open Data.List.Any.Membership-≡ using (_∈_; _⊆_) ------------------------------------------------------------------------ -- List Subset Properties ------------------------------------------------------------------------ ----------------------------------------- []⊆x : ∀ {A : Set} {x : List A} → [] ⊆ x []⊆x {A} {x} = λ () -------------------- --------------------------------------- x⊆x : ∀ {A : Set} {x : List A} → x ⊆ x x⊆x {A} {x} = λ x → x ---------------------- ------------------------------------------------------ x⊆ax : ∀ {A : Set} {a : A} {x : List A} → x ⊆ (a ∷ x) x⊆ax {a} {x} = there --------------------- ----------------------------------------- ⊆[]→≡[] : ∀ {x : List A} → x ⊆ [] → x ≡ [] ⊆[]→≡[] {[]} []⊆[] = refl ⊆[]→≡[] {b ∷ x} bx⊆[] = ⊥-elim (lem_a∉[] {A} {b} (bx⊆[] (lem∈Hd {A} {b} {x}))) -------------------------------------------------------------------------------- ----------------------------------------------------------------------- elem⊆ : ∀ {A : Set} {a : A} {x y : List A} → x ⊆ y → (a ∈ x) → (a ∈ y) elem⊆ {A} {a} {x} {y} x⊆y a∈x = x⊆y a∈x ---------------------------------------- ------------------------------------------------------------------------------ notElem⊆ : ∀ {A : Set} (a : A) (x y : List A) → x ⊆ y → ¬ (a ∈ y) → ¬ (a ∈ x) notElem⊆ a x y x⊆y a∉y = λ a∈x → a∉y (x⊆y a∈x) ------------------------------------------------ ---------------------------------------------------------------- lem_⊆⊆→⊆ : ∀ {A : Set} {x y z : List A} → x ⊆ y → z ⊆ x → z ⊆ y lem_⊆⊆→⊆ {A} {x} {y} {z} x⊆y z⊆x a∈z = x⊆y (z⊆x a∈z) ---------------------------------------------------- -------------------------------------------------------------- ⊆trans : ∀ {A : Set} {x y z : List A} → x ⊆ y → y ⊆ z → x ⊆ z ⊆trans {A} {x} {y} {z} x⊆y y⊆z a∈x = y⊆z (x⊆y a∈x) --------------------------------------------------- -- end of module Subset ------------------------------------------------------------------------ module SubsetUnion where open import Data.List.Any open Data.List.Any.Membership-≡ using (_∈_; _⊆_) ------------------------------------------------------------------------ -- List Subset Union Properties ------------------------------------------------------------------------ --------------------------------------- x⊆x∪y : ∀ {x y : List A} → x ⊆ (x ∪ y) x⊆x∪y {x} {y} a∈x = lem∈x→∈x∪y {_} {x} {y} a∈x y⊆x∪y : ∀ {x y : List A} → y ⊆ (x ∪ y) y⊆x∪y {x} {y} a∈y = lem∈y→∈x∪y {_} {x} {y} a∈y ----------------------------------------------- ----------------------------------------------- lem⊆→⊆∪ : ∀ {x y z : List A} → x ⊆ y → x ⊆ z ∪ y lem⊆→⊆∪ {x} {y} {z} x⊆y a∈x = lem∈y→∈x∪y {_} {z} {y} (x⊆y a∈x) --------------------------------------------------------------- ---------------------------------------------------------------------------- lem⊆→∪⊆∪ : ∀ {x₁ y₁ x₂ y₂ : List A} → x₁ ⊆ y₁ → x₂ ⊆ y₂ → x₁ ∪ x₂ ⊆ y₁ ∪ y₂ lem⊆→∪⊆∪ {x₁} {y₁} {x₂} {y₂} x₁⊆y₁ x₂⊆y₂ a∈x₁∪x₂ with lem∈x∪y→∈xOr∈y _ x₁ x₂ a∈x₁∪x₂ lem⊆→∪⊆∪ {x₁} {y₁} {x₂} {y₂} x₁⊆y₁ x₂⊆y₂ a∈x₁∪x₂ | inj₁ a∈x₁ = lem∈x→∈x∪y {_} {y₁} {y₂} (x₁⊆y₁ a∈x₁) lem⊆→∪⊆∪ {x₁} {y₁} {x₂} {y₂} x₁⊆y₁ x₂⊆y₂ a∈x₁∪x₂ | inj₂ a∈x₂ = lem∈y→∈x∪y {_} {y₁} {y₂} (x₂⊆y₂ a∈x₂) ---------------------------------------------------------------------------------------------------- --------------------------------------------------------------- lem⊆→∪⊆ : ∀ {x₁ x₂ y : List A} → x₁ ⊆ y → x₂ ⊆ y → x₁ ∪ x₂ ⊆ y lem⊆→∪⊆ {x₁} {x₂} {y} x₁⊆y x₂⊆y a∈x₁∪x₂ with lem∈x∪y→∈xOr∈y _ x₁ x₂ a∈x₁∪x₂ lem⊆→∪⊆ {x₁} {x₂} {y} x₁⊆y x₂⊆y a∈x₁∪x₂ | inj₁ a∈x₁ = x₁⊆y a∈x₁ lem⊆→∪⊆ {x₁} {x₂} {y} x₁⊆y x₂⊆y a∈x₁∪x₂ | inj₂ a∈x₂ = x₂⊆y a∈x₂ ---------------------------------------------------------------- ---------------------------------------------------------------------------------- lem∈x∪y→x⊆z→∈z∪y : ∀ {a : A} {x y z : List A} → x ⊆ z → a ∈ (x ∪ y) → a ∈ (z ∪ y) lem∈x∪y→x⊆z→∈z∪y {a} {x} {[]} {z} x⊆z a∈x rewrite (lem_x∪[]≡x {z}) with a ≡ a -- bug: replacing dummy 'a ≡ a' with 'x ⊆ z' causes error lem∈x∪y→x⊆z→∈z∪y {a} {x} {[]} {z} x⊆z a∈x | _ rewrite (lem_x∪[]≡x {x}) = x⊆z a∈x lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {[]} x⊆z a∈x∪y rewrite (⊆[]→≡[] {x} x⊆z) = a∈x∪y lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y with any (_≟_ a) x lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | yes a∈x = lem∈x→∈x∪y {a} {c ∷ z} {b ∷ y} (x⊆z a∈x) lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x with a ≟ b lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x | yes a≡b with any (_≟_ a) (c ∷ z) lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x | yes a≡b | yes a∈cz = lem∈x→∈x∪y {a} {c ∷ z} {b ∷ y} a∈cz lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x | yes a≡b | no a∉cz rewrite a≡b = lem_a∉x→a∈y→a∈x∪y b (c ∷ z) (b ∷ y) a∉cz (lem∈Hd {A} {b} {y}) lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x | no a≢b with any (_≟_ a) (c ∷ z) lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x | no a≢b | yes a∈cz = lem∈x→∈x∪y {a} {c ∷ z} {b ∷ y} a∈cz lem∈x∪y→x⊆z→∈z∪y {a} {x} {b ∷ y} {c ∷ z} x⊆z a∈x∪y | no a∉x | no a≢b | no a∉cz = lem_a∉x→a∈y→a∈x∪y a (c ∷ z) (b ∷ y) a∉cz (lem∉x→∈x∪y→∈y a x (b ∷ y) a∉x a∈x∪y) ------------------------------------------ ----------------------------------------------------------- ∪_preserves_⊆ : ∀ {x y z : List A} → x ⊆ y → x ∪ z ⊆ y ∪ z ∪_preserves_⊆ {x} {y} {z} x⊆y a∈x∪z with lem∈x∪y→∈xOr∈y _ x z a∈x∪z ∪_preserves_⊆ {x} {y} {z} x⊆y a∈x∪z | inj₁ a∈x = x⊆x∪y {y} {z} (x⊆y a∈x) ∪_preserves_⊆ {x} {y} {z} x⊆y a∈x∪z | inj₂ a∈z = y⊆x∪y {y} {z} a∈z ------------------------------------------------------------------- ------------------------------------------------------------------ lem_⊆→⊆∪ : ∀ {x y z w : List A} → x ⊆ (y ∪ z) → y ⊆ w → x ⊆ w ∪ z lem_⊆→⊆∪ {x} {y} {z} {w} x⊆y∪z y⊆w a∈x with lem∈x∪y→∈xOr∈y _ y z (x⊆y∪z a∈x) lem_⊆→⊆∪ {x} {y} {z} {w} x⊆y∪z y⊆w a∈x | inj₁ a∈y = x⊆x∪y {w} {z} (y⊆w a∈y) lem_⊆→⊆∪ {x} {y} {z} {w} x⊆y∪z y⊆w a∈x | inj₂ a∈z = y⊆x∪y {w} {z} a∈z ---------------------------------------------------------------------- --------------------------------------------------------------- lem_⊆x∪y→⊆y∪x : ∀ {x y z : List A} → x ⊆ (y ∪ z) → x ⊆ (z ∪ y) lem_⊆x∪y→⊆y∪x {x} {y} {z} x⊆y∪z a∈x with lem∈x∪y→∈xOr∈y _ y z (x⊆y∪z a∈x) lem_⊆x∪y→⊆y∪x {x} {y} {z} x⊆y∪z a∈x | inj₁ a∈y = y⊆x∪y {z} {y} a∈y lem_⊆x∪y→⊆y∪x {x} {y} {z} x⊆y∪z a∈x | inj₂ a∈z = x⊆x∪y {z} {y} a∈z ------------------------------------------------------------------- -- end of module SubsetUnion module SetDifference where ------------------------------------------------------------------------ -- List Set Difference Properties ------------------------------------------------------------------------ -------------------------- _⊖_ : List A → List A → List A x ⊖ [] = x x ⊖ (a ∷ y) = delete a x ⊖ y ----------------------------- ----------------------------------------- lem_[]⊖x≡[] : ∀ {x : List A} → [] ⊖ x ≡ [] lem_[]⊖x≡[] {[]} = refl lem_[]⊖x≡[] {a ∷ x} = begin [] ⊖ (a ∷ x) ≡⟨ refl ⟩ delete a [] ⊖ x ≡⟨ cong (λ y → y ⊖ x) (del[] {a}) ⟩ [] ⊖ x ≡⟨ lem_[]⊖x≡[] {x} ⟩ [] ∎ --- ----------------------------------------------------- lem∉[]⊖x : ∀ {a : A} {x : List A} → ¬ (a ∈ ([] ⊖ x)) lem∉[]⊖x {a} {x} rewrite (lem_[]⊖x≡[] {x}) = lem_a∉[] {A} {a} ---------------------------------------------------------------- -- end of module SetDifference module DifferenceDelete where -------------------------------------------------------------------- lem_⊖ : ∀ {a : A} {x y : List A} → (delete a x ⊖ y) ≡ (x ⊖ (a ∷ y)) lem_⊖ {a} {x} {y} = refl ------------------------- --------------------------------------------------------------------------------- lem_del⊖[] : ∀ {a : A} {x : List A} → delete a x ≡ (x ⊖ (a ∷ [])) lem_del⊖[] {a} {x} = refl -------------------------- ---------------------------------------------------------------------------- these are mutually recursive lem_del⊖ : ∀ {a : A} {x y : List A} → (delete a x ⊖ y) ≡ (delete a (x ⊖ y)) lem_del⊖₁ : ∀ {a : A} {x y : List A} → delete a (x ⊖ y) ≡ delete a (x ⊖ (a ∷ y)) lem_del⊖₁ {a} {x} {[]} = begin delete a (x ⊖ []) ≡⟨ sym (lem_del_idempotent a (x ⊖ [])) ⟩ delete a (delete a (x ⊖ [])) ≡⟨ cong (λ x → delete a x) (lem_del⊖[] {a} {x}) ⟩ -- lem_del⊖ is proved just with refl, but putting refl instead of lem_del⊖[] causes code to become yellow. :-( delete a (x ⊖ (a ∷ [])) ∎ lem_del⊖₁ {a} {[]} {y} = begin delete a ([] ⊖ y) ≡⟨ cong (λ x → delete a x) (lem_[]⊖x≡[] {y}) ⟩ delete a [] ≡⟨ cong (λ x → delete a x) (sym (lem_[]⊖x≡[] {a ∷ y})) ⟩ delete a ([] ⊖ (a ∷ y)) ∎ lem_del⊖₁ {a} {x} {c ∷ y} = begin delete a (x ⊖ (c ∷ y)) ≡⟨ cong (λ x → delete a x) (sym (lem_⊖ {c} {x} {y})) ⟩ delete a (delete c x ⊖ y) ≡⟨ sym (lem_del_idempotent a (delete c x ⊖ y)) ⟩ delete a (delete a (delete c x ⊖ y)) ≡⟨ cong (λ x → delete a x) (sym (lem_del⊖ {a} {delete c x} {y})) ⟩ delete a (delete a (delete c x) ⊖ y) ≡⟨ cong (λ x → delete a x) ((cong (λ x → x ⊖ y) (lem_com_del {a} {c} {x}))) ⟩ delete a (delete c (delete a x) ⊖ y) ≡⟨ cong (λ x → delete a x) (sym (lem_⊖ {c} {delete a x} {y})) ⟩ delete a (delete a x ⊖ (c ∷ y)) ≡⟨ cong (λ x → delete a x) (sym (lem_⊖ {a} {x} {c ∷ y})) ⟩ delete a (x ⊖ (a ∷ c ∷ y)) ∎ --- ------------------------------------------------------------------------------- -- lem_del⊖ : ∀ {a : A} {x y : List A} → (delete a x ⊖ y) ≡ (delete a (x ⊖ y)) lem_del⊖ {a} {x} {[]} = refl lem_del⊖ {a} {x} {b ∷ y} with a ≟ b lem_del⊖ {a} {x} {.a ∷ y} | yes refl = begin delete a x ⊖ (a ∷ y) ≡⟨ refl ⟩ delete a (delete a x) ⊖ y ≡⟨ cong (λ x → x ⊖ y) (lem_del_idempotent a x) ⟩ delete a x ⊖ y ≡⟨ lem_del⊖ {a} {x} {y} ⟩ delete a (x ⊖ y) ≡⟨ lem_del⊖₁ {a} {x} {y} ⟩ delete a (x ⊖ (a ∷ y)) ∎ lem_del⊖ {a} {x} {b ∷ y} | no a≢b = begin delete a x ⊖ (b ∷ y) ≡⟨ refl ⟩ delete b (delete a x) ⊖ y ≡⟨ cong (λ x → x ⊖ y) (lem_com_del {b} {a} {x}) ⟩ delete a (delete b x) ⊖ y ≡⟨ lem_del⊖ {a} {delete b x} {y} ⟩ delete a (delete b x ⊖ y) ≡⟨ refl ⟩ delete a (x ⊖ (b ∷ y)) ∎ --- ------------------------------------------------------------------------------ lema_x⊖y≡x⊖ay : ∀ {a : A} {x y : List A} → (x ⊖ (a ∷ y)) ≡ (delete a (x ⊖ y)) lema_x⊖y≡x⊖ay {a} {x} {y} = lem_del⊖ {a} {x} {y} ------------------------------------------------- ------------------------------------------------------------- lem∈x⊖y→∈x : ∀ {a : A} {x y : List A} → a ∈ (x ⊖ y) → a ∈ x lem∈x⊖y→∈x {a} {x} {[]} a∈x = a∈x lem∈x⊖y→∈x {a} {x} {b ∷ y} a∈x⊖by rewrite (lema_x⊖y≡x⊖ay {b} {x} {y}) = lem∈x⊖y→∈x {a} {x} {y} (lem∈del {a} {b} {x ⊖ y} a∈x⊖by) ------------------------------------- ---------------------------------------------------------------------------- lem∈x⊖by→∈x⊖y : ∀ {a b : A} {x y : List A} → a ∈ (x ⊖ (b ∷ y)) → a ∈ (x ⊖ y) lem∈x⊖by→∈x⊖y {a} {b} {x} {y} a∈x⊖by rewrite (lema_x⊖y≡x⊖ay {b} {x} {y}) = lem∈del {a} {b} {x ⊖ y} a∈x⊖by ---------------------------------------------------------------------------------------------------------- ---------------------------------------------------------------- lem∈x⊖y→∉y : ∀ {a : A} {x y : List A} → a ∈ (x ⊖ y) → ¬ (a ∈ y) lem∈x⊖y→∉y {a} {x} {[]} a∈x a∈[] = ⊥-elim (lem_a∉[] {A} {a} a∈[]) lem∈x⊖y→∉y {a} {x} {.a ∷ y} a∈x⊖ay (here refl) = ⊥-elim (lem∉del {a} {x} (lem∈x⊖y→∈x {a} {delete a x} {y} a∈x⊖ay)) lem∈x⊖y→∉y {a} {x} {b ∷ y} a∈x⊖by (there a∈y) = ⊥-elim (lem∈x⊖y→∉y {a} {x} {y} (lem∈x⊖by→∈x⊖y {a} {b} {x} {y} a∈x⊖by) a∈y) ---------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------------------------------------------------- lem∈x⊖y→≢b→∈x⊖by : ∀ {a b : A} {x y : List A} → a ∈ (x ⊖ y) → ¬ (a ≡ b) → a ∈ (x ⊖ (b ∷ y)) lem∈x⊖y→≢b→∈x⊖by {a} {b} {x} {y} a∈x⊖y a≢b with any (_≟_ a) y lem∈x⊖y→≢b→∈x⊖by {a} {b} {x} {y} a∈x⊖y a≢b | yes a∈y = ⊥-elim (lem∈x⊖y→∉y {a} {x} {y} a∈x⊖y a∈y) lem∈x⊖y→≢b→∈x⊖by {a} {b} {x} {y} a∈x⊖y a≢b | no _ rewrite (lem_del⊖ {b} {x} {y}) = lem∈x→≢b→∈x_b {a} {b} {x ⊖ y} a∈x⊖y a≢b ------------------------------------------ --------------------------------------------------------------------------- lem∈x→∉y→∈x⊖y : ∀ {a : A} {x y : List A} → a ∈ x → ¬ (a ∈ y) → a ∈ (x ⊖ y) lem∈x→∉y→∈x⊖y {a} {x} {[]} a∈x _ = a∈x lem∈x→∉y→∈x⊖y {a} {x} {c ∷ y} a∈x a∉cy with a ≟ c lem∈x→∉y→∈x⊖y {a} {x} {.a ∷ y} a∈x a∉ay | yes refl = ⊥-elim (a∉ay (here refl)) lem∈x→∉y→∈x⊖y {a} {x} {c ∷ y} a∈x a∉cy | no a≢c = lem∈x⊖y→≢b→∈x⊖by {a} {c} {x} {y} (lem∈x→∉y→∈x⊖y {a} {x} {y} a∈x (lem∉∷→∉ {A} {a} {c} {y} a∉cy)) -- a ∈ (x ⊖ y) a≢c -------- ----------------------------------------------------------------------------- lem∈x⊖y→∈bx⊖y : ∀ {a b : A} {x y : List A} → a ∈ (x ⊖ y) → a ∈ ((b ∷ x) ⊖ y) lem∈x⊖y→∈bx⊖y {a} {b} {[]} {y} a∈[]⊖y rewrite (lem_[]⊖x≡[] {y}) = ⊥-elim (lem_a∉[] {A} {a} a∈[]⊖y) lem∈x⊖y→∈bx⊖y {a} {b} {x} {y} a∈x⊖y with any (_≟_ a) y lem∈x⊖y→∈bx⊖y {a} {b} {x} {y} a∈x⊖y | yes a∈y = ⊥-elim (lem∈x⊖y→∉y {a} {x} {y} a∈x⊖y a∈y) lem∈x⊖y→∈bx⊖y {a} {b} {x} {y} a∈x⊖y | no a∉y = lem∈x→∉y→∈x⊖y {a} {b ∷ x} {y} (lem∈→∈∷ {A} {a} {b} -- a∈bx from a∈x (lem∈x⊖y→∈x {a} {x} {y} a∈x⊖y)) -- a∈x from a∈x⊖y a∉y -------- -------------------------------------------------------------------- lem∉x→∉x⊖y : ∀ {a : A} {x y : List A} → ¬ (a ∈ x) → ¬ (a ∈ (x ⊖ y)) lem∉x→∉x⊖y {a} {x} {y} a∉x a∈x⊖y = ⊥-elim (a∉x (lem∈x⊖y→∈x {a} {x} {y} a∈x⊖y)) ------------------------------------------------------------------------------- -- end of module DifferenceDelete module DifferenceSubset where --------------------------------------- lem⊆→⊖⊆ : ∀ (x y : List A) → (x ⊖ y) ⊆ x lem⊆→⊖⊆ x y a∈x⊖y = lem∈x⊖y→∈x {_} {x} {y} a∈x⊖y ------------------------------------------------- -- end of module DifferenceSubset module Disjoint where ------------------------------------------------------------------------ -- List Set Disjointness Properties ------------------------------------------------------------------------ ------------------------------------- _∩̸_ : {A : Set} (x y : List A) → Set x ∩̸ y = ∀ {a} → a ∈ x → (¬ (a ∈ y)) ------------------------------------ -------------------------------------------------- com∩̸ : ∀ {A : Set} {x y : List A} → x ∩̸ y → y ∩̸ x com∩̸ {A} {x} {y} x∩̸y = λ x y → x∩̸y y x --------------------------------------- ---------------------------------------- ∩̸[] : ∀ {A : Set} {x : List A} → x ∩̸ [] ∩̸[] = λ _ → lem_a∉[] --------------------- ---------------------------------------- []∩̸ : ∀ {A : Set} {x : List A} → [] ∩̸ x []∩̸ = λ () ----------- -------------------------------------------------------------------------- ∩̸∷ : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ y) → x ∩̸ y → (a ∷ x) ∩̸ y ∩̸∷ a∉y x∩̸y (here refl) = λ a∈y → a∉y a∈y ∩̸∷ a∉y x∩̸y (there a₁∈x) = x∩̸y a₁∈x ----------------------------------- --------------------------------------------------------------------------- ∩̸∷' : ∀ {A : Set} {a : A} {x y : List A} → ¬ (a ∈ x) → x ∩̸ y → x ∩̸ (a ∷ y) ∩̸∷' a∉x x∩̸y a∈x (here refl) = a∉x a∈x ∩̸∷' a∉x x∩̸y a∈x (there a₁∈a:x) = x∩̸y a∈x a₁∈a:x ------------------------------------------------ ------------------------------------------------------------------------ lem∩̸→∉ : ∀ {A : Set} {a : A} {x y : List A} → x ∩̸ y → a ∈ x → ¬ (a ∈ y) lem∩̸→∉ {a} {x} {y} x∩̸y a∈x = x∩̸y a∈x ------------------------------------- ------------------------------------------------------------------- ∩̸→∉ : ∀ {A : Set} {a : A} {x y : List A} → x ∩̸ (a ∷ y) → ¬ (a ∈ x) ∩̸→∉ {A} {a} {x} {y} x∩̸ay a∈x = x∩̸ay a∈x (here refl) ---------------------------------------------------- ------------------------------------------------------------------- ∩̸→∉' : ∀ {A : Set} {a : A} {x y : List A} → (a ∷ y) ∩̸ x → ¬ (a ∈ x) ∩̸→∉' {A} {a} {x} {y} ay∩̸x a∈x = ay∩̸x (here refl) a∈x ---------------------------------------------------- ----------------------------------------------------------------- ∩̸Tail : ∀ {A : Set} {a : A} {x y : List A} → (a ∷ x) ∩̸ y → x ∩̸ y ∩̸Tail ax∩̸y (here p) = ax∩̸y (there (here p)) ∩̸Tail ax∩̸y (there p) = ∩̸Tail (λ z → ax∩̸y (there z)) p ------------------------------------------------------ ------------------------------------------------------------------ ∩̸Tail' : ∀ {A : Set} {a : A} {x y : List A} → x ∩̸ (a ∷ y) → x ∩̸ y ∩̸Tail' x∩̸ay (here p) = λ z → x∩̸ay (here p) (there z) ∩̸Tail' x∩̸ay (there p) = ∩̸Tail' (λ z → x∩̸ay (there z)) p -------------------------------------------------------- -------------------------------------------------------- lem∉→∩̸ : ∀ {a : A} {x : List A} → ¬ (a ∈ x) → [ a ] ∩̸ x lem∉→∩̸ {a} {[]} _ _ () lem∉→∩̸ {a} {b ∷ y} a∉by a∈[a] (here a∈by) with a ≟ b lem∉→∩̸ {a} {.a ∷ y} a∉by a∈[a] (here a∈by) | yes refl = a∉by (here refl) lem∉→∩̸ {a} {b ∷ y} a∉by (here px) (here a∈by) | no p rewrite px = p a∈by lem∉→∩̸ {a} {b ∷ y} a∉by (there ()) (here a∈by) | no p lem∉→∩̸ {a} {b ∷ y} a∉by a∈[a] (there a∈by) = lem∉→∩̸ (λ z → a∉by (there z)) a∈[a] a∈by --------------------------------------------------------------------------------------- -- end of module Disjoint module DisjointSubset where ------------------------------------------------------------ ⊆→∩̸ : ∀ {A : Set} {x y z : List A} → x ⊆ y → y ∩̸ z → x ∩̸ z ⊆→∩̸ x⊆y y∩̸z a∈x = y∩̸z (x⊆y a∈x) -------------------------------- ------------------------------------------------------------------------- ⊆→∩̸₁ : ∀ {A : Set} {y z x x' : List A} → y ⊆ z → x ∩̸ z → x' ⊆ x → y ∩̸ x' ⊆→∩̸₁ y⊆z x∩̸z x'⊆x a∈y a∈x' = x∩̸z (x'⊆x a∈x') (y⊆z a∈y) ------------------------------------------------------- -- end of module DisjointSubset module DisjointUnion where ------------------------------------------------------------ ∩̸∪ : ∀ {x₁ x₂ y : List A} → x₁ ∩̸ y → x₂ ∩̸ y → (x₁ ∪ x₂) ∩̸ y ∩̸∪ {x₁} {x₂} x₁∩̸y x₂∩̸y a∈x₁∪x₂ y with lem∈x∪y→∈xOr∈y _ x₁ x₂ a∈x₁∪x₂ ∩̸∪ {x₁} {x₂} x₁∩̸y x₂∩̸y a∈x₁∪x₂ y | (inj₁ inx₁) = x₁∩̸y inx₁ y ∩̸∪ {x₁} {x₂} x₁∩̸y x₂∩̸y a∈x₁∪x₂ y | (inj₂ inx₂) = x₂∩̸y inx₂ y ------------------------------------------------------------- ---------------------------------------------------------------------------------------------- lem∪→∩̸' : ∀ {d₁ d₂ r₁ r₂ : List A} → d₁ ∩̸ r₁ → d₂ ∩̸ r₂ → ((d₁ ∪ d₂) ∩̸ ((r₂ ⊖ d₁) ∪ (r₁ ⊖ d₂))) lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ with lem∈x∪y→∈xOr∈y _ d₁ d₂ a∈d₁∪d₂ lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ | inj₁ a∈d₁ with lem∈x∪y→∈xOr∈y _ (r₂ ⊖ d₁) (r₁ ⊖ d₂) a∈r₂⊖d₁∪r₁⊖d₂ lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ | inj₁ a∈d₁ | inj₁ a∈r₂⊖d₁ = ⊥-elim ((lem∈x⊖y→∉y {_} {r₂} {d₁} a∈r₂⊖d₁) a∈d₁) lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ | inj₁ a∈d₁ | inj₂ a∈r₁⊖d₂ = ⊥-elim (d₁∩̸r₁ a∈d₁ (lem∈x⊖y→∈x {_} {r₁} {d₂} a∈r₁⊖d₂)) lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ | inj₂ a∈d₂ with lem∈x∪y→∈xOr∈y _ (r₂ ⊖ d₁) (r₁ ⊖ d₂) a∈r₂⊖d₁∪r₁⊖d₂ lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ | inj₂ a∈d₂ | inj₁ a∈r₂⊖d₁ = ⊥-elim (d₂∩̸r₂ a∈d₂ (lem∈x⊖y→∈x {_} {r₂} {d₁} a∈r₂⊖d₁)) lem∪→∩̸' {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ a∈d₁∪d₂ a∈r₂⊖d₁∪r₁⊖d₂ | inj₂ a∈d₂ | inj₂ a∈r₁⊖d₂ = ⊥-elim ((lem∈x⊖y→∉y {_} {r₁} {d₂} a∈r₁⊖d₂) a∈d₂) ------------------------------------------------------------------------------------------------------------------------------------------- ------------------------------------------------------------------------------------------------ lem∪→∩̸ : ∀ {d₁ d₂ r₁ r₂ : List A} → d₁ ∩̸ r₁ → d₂ ∩̸ r₂ → d₁ ∩̸ r₂ → ((d₁ ∪ d₂) ∩̸ (r₂ ∪ (r₁ ⊖ d₂))) lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ with lem∈x∪y→∈xOr∈y _ d₁ d₂ a∈d₁∪d₂ lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ | inj₁ a∈d₁ with lem∈x∪y→∈xOr∈y _ r₂ (r₁ ⊖ d₂) a∈r₂∪r₁⊖d₂ lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ | inj₁ a∈d₁ | inj₁ a∈r₂ = ⊥-elim (d₁∩̸r₂ a∈d₁ a∈r₂) lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ | inj₁ a∈d₁ | inj₂ a∈r₁⊖d₂ = ⊥-elim (d₁∩̸r₁ a∈d₁ (lem∈x⊖y→∈x {_} {r₁} {d₂} a∈r₁⊖d₂)) lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ | inj₂ a∈d₂ with lem∈x∪y→∈xOr∈y _ r₂ (r₁ ⊖ d₂) a∈r₂∪r₁⊖d₂ lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ | inj₂ a∈d₂ | inj₁ a∈r₂ = ⊥-elim (d₂∩̸r₂ a∈d₂ a∈r₂) lem∪→∩̸ {d₁} {d₂} {r₁} {r₂} d₁∩̸r₁ d₂∩̸r₂ d₁∩̸r₂ a∈d₁∪d₂ a∈r₂∪r₁⊖d₂ | inj₂ a∈d₂ | inj₂ a∈r₁⊖d₂ = ⊥-elim ((lem∈x⊖y→∉y {_} {r₁} {d₂} a∈r₁⊖d₂) a∈d₂) ------------------------------------------------------------------------------------------------------------------------------------------- ------------------------------------------------------------------- lem∪⊖⊆∪ : ∀ (d₁ d₂ x y : List A) → ((x ⊖ d₁) ∪ (y ⊖ d₂)) ⊆ (x ∪ y) lem∪⊖⊆∪ d₁ d₂ x y = lem⊆→∪⊆∪ (lem⊆→⊖⊆ x d₁) (lem⊆→⊖⊆ y d₂) ---------------------------------------------------------- ------------------------------------------------------------------- lem∩̸x→x⊆→x⊆⊖ : ∀ (d x y : List A) → d ∩̸ x → (x ⊆ y) → (x ⊆ (y ⊖ d)) lem∩̸x→x⊆→x⊆⊖ d x y d∩̸x x⊆y a∈x = lem∈x→∉y→∈x⊖y {_} {y} (x⊆y a∈x) (com∩̸ d∩̸x a∈x) -------------------------------------------------------------------------------- ------------------------------------------------------------------------------------------------------- lem∩̸x→x⊆∪→x⊆∪⊖ : ∀ (d₁ d₂ x y z : List A) → x ∩̸ d₁ → x ∩̸ d₂ → (x ⊆ y ∪ z) → (x ⊆ ((y ⊖ d₁) ∪ (z ⊖ d₂))) lem∩̸x→x⊆∪→x⊆∪⊖ d₁ d₂ x y z x∩̸d₁ x∩̸d₂ x⊆y∪z a∈x with lem∈x∪y→∈xOr∈y _ y z (x⊆y∪z a∈x) lem∩̸x→x⊆∪→x⊆∪⊖ d₁ d₂ x y z x∩̸d₁ x∩̸d₂ x⊆y∪z a∈x | inj₁ a∈y = lem∈x→∈x∪y {_} {y ⊖ d₁} {z ⊖ d₂} -- a ∈ ((y ⊖ d₁) ∪ (z ⊖ d₂))), from a ∈ (y ⊖ d₁) (lem∈x→∉y→∈x⊖y {_} {y} {d₁} a∈y -- a ∈ (y ⊖ d₁), from a ∈ y, a ∉ d₁ (lem∩̸→∉ {A} {_} {x} {d₁} x∩̸d₁ a∈x)) -- a ∉ d₁, from x∩̸d₁, a ∈ x lem∩̸x→x⊆∪→x⊆∪⊖ d₁ d₂ x y z x∩̸d₁ x∩̸d₂ x⊆y∪z a∈x | inj₂ a∈z = lem∈y→∈x∪y {_} {y ⊖ d₁} {z ⊖ d₂} -- a ∈ ((y ⊖ d₁) ∪ (z ⊖ d₂))), from a ∈ (z ⊖ d₂) (lem∈x→∉y→∈x⊖y {_} {z} {d₂} a∈z -- a ∈ (z ⊖ d₂), from a ∈ z, a ∉ d₂ (lem∩̸→∉ {A} {_} {x} {d₂} x∩̸d₂ a∈x)) -- a ∉ d₂, from x∩̸d₂, a ∈ x ---------------------------------------------