module 4-Membership where -- In this practical we emphasize more on the idea that -- a proof is a program/term. open import 3-Logic -- Define lists again. data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A infixr 5 _∷_ infix 4 _∈_ -- What does it mean if we say `x is a member of xs`? -- 1. x is a member of x ∷ xs. -- 2. If x is a member of xs, x is a member of y ∷ xs. -- The two axioms above are expressed as a datatype. data _∈_ {A : Set} : A → List A → Set where here : ∀ {x xs} → x ∈ (x ∷ xs) there : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs) infixr 5 _++_ -- Recall (++). _++_ : ∀ {A} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) -- Try proving the following properties. ∈-++-pos : ∀ {A : Set} {x : A} xs ys → x ∈ xs ++ ys → (x ∈ xs) ∨ (x ∈ ys) ∈-++-pos = {! !} ∈-++-r : ∀ {A : Set} {x : A} xs {ys} → x ∈ ys → x ∈ (xs ++ ys) ∈-++-r = {! !} ∈-++-l : ∀ {A : Set} {x : A} {xs} ys → x ∈ xs → x ∈ (xs ++ ys) ∈-++-l = {! !} ∈-++-weaken : ∀ {A : Set} {x : A} xs ys zs → x ∈ (xs ++ zs) → x ∈ (xs ++ ys ++ zs) ∈-++-weaken = {! !} infix 4 _∉_ _∉_ : ∀ {A} → A → List A → Set x ∉ xs = ¬ (x ∈ xs) ∉-++-l : {A : Set} {x : A} (xs ys : List A) → x ∉ xs ++ ys → x ∉ xs ∉-++-l = {! !} ∉-++-r : {A : Set} {x : A} (xs ys : List A) → x ∉ xs ++ ys → x ∉ ys ∉-++-r = {! !} ∉-++-join : ∀ {A : Set} {x : A} → ∀ xs ys → x ∉ xs → x ∉ ys → x ∉ xs ++ ys ∉-++-join = {! !} ∉-++-weaken : ∀ {A : Set} {x : A} xs ys zs → x ∉ (xs ++ ys ++ zs) → x ∉ (xs ++ zs) ∉-++-weaken = {! !}