All 與 Any#

satisfied : {A : Set} {P : A → Set} {xs : List A} → Any P xs → Σ[ x ∈ A ] P x
satisfied (here  px)  = _ , px
satisfied (there pxs) = satisfied pxs

All-map : {A : Set} {P Q : A → Set} {xs : List A} → ({x : A} → P x → Q x) → All P xs → All Q xs
All-map f []       = []
All-map f (p ∷ ps) = f p ∷ All-map f ps

Any-map : {A : Set} {P Q : A → Set} {xs : List A} → ({x : A} → P x → Q x) → Any P xs → Any Q xs
Any-map f (here  p) = here (f p)
Any-map f (there v) = there (Any-map f v)

tabulate : {A : Set} {P : A → Set} (xs : List A) → ({x : A} → x ∈ xs → P x) → All P xs
tabulate []       f = []
tabulate (x ∷ xs) f = f (here refl) ∷ tabulate xs (λ in-xs → f (there in-xs))

All-++-left : {A : Set} {P : A → Set} {ys : List A} (xs : List A) → All P (xs ++ ys) → All P xs
All-++-left []       _        = []
All-++-left (_ ∷ xs) (p ∷ ps) = p ∷ All-++-left xs ps

All-++-right : {A : Set} {P : A → Set} {ys : List A} (xs : List A) → All P (xs ++ ys) → All P ys
All-++-right []       ps       = ps
All-++-right (_ ∷ xs) (_ ∷ ps) = All-++-right xs ps

infixr 5 _++ᴬ_
_++ᴬ_ : {A : Set} {P : A → Set} {xs ys : List A} → All P xs → All P ys → All P (xs ++ ys)
[]       ++ᴬ ps' = ps'
(p ∷ ps) ++ᴬ ps' = p ∷ (ps ++ᴬ ps')

Any-++-left : {A : Set} {P : A → Set} {xs : List A} {ys : List A} → Any P xs → Any P (xs ++ ys)
Any-++-left (here  p) = here p
Any-++-left (there v) = there (Any-++-left v)

Any-++-right : {A : Set} {P : A → Set} {xs : List A} {ys : List A} → Any P ys → Any P (xs ++ ys)
Any-++-right {xs = []}     any = any
Any-++-right {xs = x ∷ xs} any = there (Any-++-right any)

∈-concat
  : {A : Set} {x : A} {xs : List A} {xss : List (List A)}
  → x ∈ xs → xs ∈ xss → x ∈ concat xss
∈-concat x∈xs (here  refl) = Any-++-left  x∈xs
∈-concat x∈xs (there xs∈)  = Any-++-right (∈-concat x∈xs xs∈)

de-morgan₁ : {A : Set} {P : A → Set} {xs : List A} → All (λ x → ¬ P x) xs → ¬ Any P xs
de-morgan₁ (¬p ∷ ¬ps) (here  p) = ¬p p
de-morgan₁ (¬p ∷ ¬ps) (there q) = de-morgan₁ ¬ps q

de-morgan₂ : {A : Set} {P : A → Set} {xs : List A} → ¬ Any P xs → All (λ x → ¬ P x) xs
de-morgan₂ {xs = []}     ¬any = []
de-morgan₂ {xs = x ∷ xs} ¬any = (λ p → ¬any (here p)) ∷ de-morgan₂ (λ v → ¬any (there v))

de-morgan₃ : {A : Set} {P : A → Set} {xs : List A} → Any (λ x → ¬ P x) xs → ¬ All P xs
de-morgan₃ (here  ¬p) (p ∷ ps) = ¬p p
de-morgan₃ (there v)  (p ∷ ps) = de-morgan₃ v ps

sum-zero' : (xs : List ℕ) → sum xs ≡ zero → All (_≡ zero) xs
sum-zero' []          p = []
sum-zero' (zero ∷ xs) p = refl ∷ sum-zero' xs p
-- 或者：
-- sum-zero' (x ∷ xs) p = fst (sum-zero x (sum xs) p) ∷ sum-zero' xs (snd (sum-zero x (sum xs) p))

sum-zero'' : (xs : List ℕ) → All (_≡ zero) xs → sum xs ≡ zero
sum-zero'' []          []         = refl
sum-zero'' (zero ∷ xs) (refl ∷ p) = sum-zero'' xs p

infix 4 _≟_
_≟_ : (a b : ℕ) → Dec (a ≡ b)
a ≟ b = ∨-elim yes no (eq? a b)

dec-→ : {A B : Set} → Dec A → Dec B → Dec (A → B)
dec-→ (yes a)  (yes b)  = yes (λ f → b)
dec-→ (yes a)  (no  ¬b) = no  (λ f → ¬b (f a))
dec-→ (no  ¬a) q        = yes (λ a → ⊥-elim (¬a a))

find : {A : Set} {P : A → Set} → ((x : A) → Dec (P x)) → (xs : List A) → Any P xs ⊎ All (λ x → ¬ (P x)) xs
find P? [] = right []
find P? (x ∷ xs) with P? x | find P? xs
... | yes px  | _       = left  (here px)
... | no ¬px  | left  q = left  (there q)
... | no ¬px  | right q = right (¬px ∷ q)

dec-All : {A : Set} {P : A → Set} → ((x : A) → Dec (P x)) → (xs : List A) → Dec (All P xs)
dec-All P? [] = yes []
dec-All P? (x ∷ xs) with P? x | dec-All P? xs
... | yes px  | yes pxs  = yes (px ∷ pxs)
... | yes px  | no  ¬pxs = no λ { (_  ∷ pxs) → ¬pxs pxs }
... | no  ¬px | _        = no λ { (px ∷ _)   → ¬px px   }

≗→≗* : {X Y : Set} {f g : X → Y} → f ≗ g → f ≗* g
≗→≗* p = [] , λ x → left (p x)

≗*-refl : {X Y : Set} {f : X → Y} → f ≗* f
≗*-refl = [] , λ x → left refl

≗*-sym : {X Y : Set} {f g : X → Y} → f ≗* g → g ≗* f
≗*-sym (xs , p) = xs , λ x → ∨-map sym (λ z → z) (p x)

≗*-trans : {X Y : Set} {f g h : X → Y} → f ≗* g → g ≗* h → f ≗* h
≗*-trans {X} {Y} {f} {g} {h} (xs , p) (xs' , p') = xs ++ xs' , go
  where
  go : (x : X) → f x ≡ h x ⊎ x ∈ xs ++ xs'
  go x with p x | p' x
  ... | left eq    | left eq'    = left (trans eq eq')
  ... | left _     | right x∈xs' = right (Any-++-right x∈xs')
  ... | right x∈xs | _           = right (Any-++-left  x∈xs)