3 files changed, 338 insertions, 0 deletions
diff --git a/src/Data/List/Relation/Binary/Prefix.agda b/src/Data/List/Relation/Binary/Prefix.agda
new file mode 100644
index 0000000..84d8e03
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Prefix.agda
@@ -0,0 +1,118 @@
+module Data.List.Relation.Binary.Prefix where
+
+open import Data.Empty using (⊥-elim)
+open import Data.List.Base using (List; []; _∷_; _++_; length; inits; map)
+open import Data.List.Properties using (length-++)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_; setoid)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.Nat using (_≤_; z≤n; s≤s; _+_) renaming (_<_ to _<ⁿ_)
+open import Data.Nat.Properties using (<⇒≱; m<m+n; module ≤-Reasoning)
+open import Data.Product using (_,_; uncurry)
+open import Function.Equivalence using (_⇔_; equivalence)
+open import Level using (Level; _⊔_)
+open import Relation.Binary
+open import Relation.Nullary using (Dec; yes; no; ¬_)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    a ℓ : Level
+
+module _
+  {A : Set a} (P : Set) (_≈_ : Rel A ℓ)
+  where
+
+  data Prefix : Rel (List A) ℓ where
+    base : P                                    → Prefix [] []
+    halt : ∀ {y ys}                             → Prefix [] (y ∷ ys)
+    next : ∀ {x xs y ys}
+           (x≈y : x ≈ y) (xs<ys : Prefix xs ys) → Prefix (x ∷ xs) (y ∷ ys)
+
+module _
+  {A : Set a} {P : Set} {_≈_ : Rel A ℓ}
+  where
+
+  private
+    _≋_ = Pointwise _≈_
+    _<_ = Prefix P _≈_
+
+  initsPrefixes : P → Reflexive _≈_ → ∀ xs → All (_< xs) (inits xs)
+  initsPrefixes p refl []       = base p ∷ []
+  initsPrefixes p refl (x ∷ xs) = halt ∷ map′ (x ∷_ ) (next refl) (initsPrefixes p refl xs)
+    where
+    map′ : ∀ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} →
+           (f : A → B) → (∀ {x} → P x → Q (f x)) → ∀ {xs} → All P xs → All Q (map f xs)
+    map′ f pres []         = []
+    map′ f pres (px ∷ pxs) = pres px ∷ map′ f pres pxs
+
+  module _
+    (equivalence : IsEquivalence _≈_)
+    where
+
+    open IsEquivalence equivalence
+    open import Data.List.Membership.Setoid (setoid (record { isEquivalence = equivalence })) using (_∈_)
+    open import Data.List.Relation.Unary.Any using (Any; here; there)
+
+    prefix∈inits : ∀ {xs ys} → xs < ys → xs ∈ inits ys
+    prefix∈inits (base x)         = here []
+    prefix∈inits halt             = here []
+    prefix∈inits (next x≈y xs<ys) = there (map′ (_∷_ _) (x≈y ∷_) (prefix∈inits xs<ys))
+      where
+      map′ : ∀ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} →
+           (f : A → B) → (∀ {x} → P x → Q (f x)) → ∀ {xs} → Any P xs → Any Q (map f xs)
+      map′ f pres (here px) = here (pres px)
+      map′ f pres (there pxs) = there (map′ f pres pxs)
+
+  reflexive : P → Reflexive _≈_ → Reflexive _<_
+  reflexive p refl {[]}      = base p
+  reflexive p refl {x ∷ xs} = next refl (reflexive p refl)
+
+  irreflexive : ¬ P → Irreflexive _≋_ _<_
+  irreflexive ¬p []          (base p)       = ¬p p
+  irreflexive ¬p (_ ∷ xs≋ys) (next _ xs<ys) = irreflexive ¬p xs≋ys xs<ys
+
+  transitive : Transitive _≈_ → Transitive _<_
+  transitive trans (base _)         ys<zs            = ys<zs
+  transitive trans halt             (next _ _)       = halt
+  transitive trans (next x≈y xs<ys) (next y≈z ys<zs) =
+    next (trans x≈y y≈z) (transitive trans xs<ys ys<zs)
+
+  antisymmetric : Symmetric _≈_ → Antisymmetric _≋_ _<_
+  antisymmetric sym (base _)         (base _)         = []
+  antisymmetric sym (next x≈y xs<ys) (next y≈x ys<xs) =
+    x≈y ∷ antisymmetric sym xs<ys ys<xs
+
+  decidable : Dec P → Decidable _≈_ → Decidable _<_
+  decidable P? _≈?_ []       []       = Dec.map′ base (λ { (base p) → p }) P?
+  decidable P? _≈?_ []       (x ∷ ys) = yes halt
+  decidable P? _≈?_ (x ∷ xs) []       = no λ ()
+  decidable P? _≈?_ (x ∷ xs) (y ∷ ys) =
+    Dec.map′ (uncurry next)
+             (λ { (next x≈y xs<ys) → x≈y , xs<ys })
+             ((x ≈? y) ×-dec (decidable P? _≈?_ xs ys))
+
+  length≤ : ∀ {xs} {ys} → xs < ys → length xs ≤ length ys
+  length≤ (base x)         = z≤n
+  length≤ halt             = z≤n
+  length≤ (next x≈y xs<ys) = s≤s (length≤ xs<ys)
+
+  length< : ∀ {xs} {ys} → ¬ P → xs < ys → length xs <ⁿ length ys
+  length< ¬p (base p)         = ⊥-elim (¬p p)
+  length< ¬p halt             = s≤s z≤n
+  length< ¬p (next x≈y xs<ys) = s≤s (length< ¬p xs<ys)
+
+  minimum : P → Minimum _<_ []
+  minimum p []       = base p
+  minimum p (x ∷ xs) = halt
+
+  ¬maximum : A → ∀ xs → ¬ Maximum _<_ xs
+  ¬maximum a xs max =
+    <⇒≱
+      (begin-strict
+        length xs                   <⟨  m<m+n (length xs) (s≤s z≤n) ⟩
+        length xs + length (a ∷ []) ≡˘⟨ length-++ xs ⟩
+        length (xs ++ a ∷ [])       ∎)
+      (length≤ (max (xs ++ a ∷ [])))
+    where open ≤-Reasoning
diff --git a/src/Data/List/Relation/Binary/Suffix.agda b/src/Data/List/Relation/Binary/Suffix.agda
new file mode 100644
index 0000000..6b41a67
--- /dev/null
+++ b/src/Data/List/Relation/Binary/Suffix.agda
@@ -0,0 +1,73 @@
+module Data.List.Relation.Binary.Suffix where
+
+open import Data.Bool using (true; false; _∧_; _∨_)
+open import Data.Empty using (⊥-elim)
+open import Data.List using (List; []; _∷_; length)
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_; setoid)
+open import Data.Nat using (suc; _≤_; z≤n; s≤s)
+open import Data.Nat.Properties using (n<1+n; ≤-step; <⇒≱; module ≤-Reasoning)
+open import Data.Sum using (inj₁; inj₂; [_,_])
+open import Level using (Level; _⊔_)
+open import Relation.Binary
+open import Relation.Nullary using (yes; no; ¬_)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Sum using (_⊎-dec_)
+
+private
+  variable
+    a ℓ : Level
+
+module _
+  {A : Set a} (_≈_ : Rel A ℓ)
+  where
+
+  data Suffix : Rel (List A) (a ⊔ ℓ) where
+    base : ∀ {xs ys} → (xs≋ys : Pointwise _≈_ xs ys) → Suffix xs ys
+    next : ∀ y {xs ys} → Suffix xs ys → Suffix xs (y ∷ ys)
+
+module _
+  {A : Set a} {_≈_ : Rel A ℓ}
+  where
+
+  private
+    _≋_ = Pointwise _≈_
+    _<_ = Suffix _≈_
+
+  length≤ : ∀ {xs ys} → xs < ys → length xs ≤ length ys
+  length≤ (base [])            = z≤n
+  length≤ (base (x∼y ∷ xs≋ys)) = s≤s (length≤ (base xs≋ys))
+  length≤ (next y xs<ys)       = ≤-step (length≤ xs<ys)
+
+  refl : Reflexive _≈_ → Reflexive _<_
+  refl refl {xs} = base (Pointwise.refl refl)
+
+  transitive : Transitive _≈_ → Transitive _<_
+  transitive trans xs<ys          (next z ys<zs)       = next z (transitive trans xs<ys ys<zs)
+  transitive trans (base xs≋ys)   (base ys≋zs)         = base (Pointwise.transitive trans xs≋ys ys≋zs)
+  transitive trans (next y xs<ys) (base (y∼z ∷ ys≋zs)) = next _ (transitive trans xs<ys (base ys≋zs))
+
+  antisymmetric : Symmetric _≈_ → Antisymmetric _≋_ _<_
+  antisymmetric sym (base xs≋ys) _ = xs≋ys
+  antisymmetric sym (next _ _) (base ys≋xs) = Pointwise.symmetric sym ys≋xs
+  antisymmetric sym (next y {x ∷ xs} {ys} x∷xs<ys) (next x y∷ys<xs) =
+    ⊥-elim
+      (<⇒≱ (≤-step (n<1+n (length xs)))
+           (begin
+             suc (suc (length xs)) ≡⟨⟩
+             suc (length (x ∷ xs)) ≤⟨ s≤s (length≤ x∷xs<ys) ⟩
+             suc (length ys) ≡⟨⟩
+             length (y ∷ ys) ≤⟨ length≤ y∷ys<xs ⟩
+             length xs ∎))
+    where open ≤-Reasoning
+
+  minimum : Minimum _<_ []
+  minimum []       = base []
+  minimum (x ∷ xs) = next x (minimum xs)
+
+  decidable : Decidable _≈_ → Decidable _<_
+  decidable ≈? [] ys = yes (minimum ys)
+  decidable ≈? (x ∷ xs) [] = no (λ { (base ()) })
+  decidable ≈? (x ∷ xs) (y ∷ ys) =
+    Dec.map′ [ base , next y ]
+             (λ { (base xs≋ys) → inj₁ xs≋ys ; (next _ xs<ys) → inj₂ xs<ys })
+             (Pointwise.decidable ≈? (x ∷ xs) (y ∷ ys) ⊎-dec decidable ≈? (x ∷ xs) ys)
diff --git a/src/Motzkin.agda b/src/Motzkin.agda
new file mode 100644
index 0000000..d5aa67e
--- /dev/null
+++ b/src/Motzkin.agda
@@ -0,0 +1,147 @@
+
+module Motzkin where
+
+open import Data.Nat using (ℕ; zero; suc; _+_; _≤?_; z≤n)
+open import Data.Nat.Properties using (≤-totalOrder)
+
+open import Data.Empty using (⊥-elim)
+open import Data.Fin using (Fin; zero; suc; toℕ; raise)
+open import Data.List using (List; []; _∷_; length; filter; cartesianProductWith; allFin; map)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Suffix as Suffix using (base; next)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties as AllP using (all-filter)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties as AnyP using (lookup-result)
+open import Data.List.Relation.Unary.Linked using ([]; [-]; _∷_)
+open import Data.List.Relation.Unary.Sorted.TotalOrder ≤-totalOrder using (Sorted; sorted?)
+open import Data.Product using (_×_; _,_; ∃₂; proj₁; proj₂; map₁)
+open import Data.Product.Properties as Prod
+open import Data.Sum using (_⊎_; [_,_])
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; replicate; updateAt; toList)
+open import Data.Vec.Properties using (map-id)
+open import Function using (_∘_; case_of_; id)
+open import Function.Equivalence using (_⇔_; equivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; subst; setoid)
+open import Relation.Nullary using (Dec; yes; no; ¬_)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Implication using (_→-dec_)
+open import Relation.Unary using (Pred; Decidable)
+
+_≋_ : ∀ {n} → Rel (List (Fin n)) _
+_≋_ = Pointwise _≡_
+
+Suffix : ∀ {n} → Rel (List (Fin n)) _
+Suffix = Suffix.Suffix _≡_
+
+counts : ∀ {n} → (xs : List (Fin n)) → Vec ℕ n
+counts []       = replicate 0
+counts (x ∷ xs) = updateAt x suc (counts xs)
+
+sorted-0s : ∀ {n} → (Sorted ∘ toList {n = n} ∘ replicate) 0
+sorted-0s {zero}        = []
+sorted-0s {suc zero}    = [-]
+sorted-0s {suc (suc n)} = z≤n ∷ sorted-0s
+
+≋⇒≡ : ∀ {n} {xs ys : List (Fin n)} → xs ≋ ys → xs ≡ ys
+≋⇒≡ [] = refl
+≋⇒≡ (x≡y ∷ xs≋ys) = subst (λ _ → _ ≡ _ ∷ _) x≡y (cong (_ ∷_) (≋⇒≡ xs≋ys))
+
+P : ∀ {n} → Pred (List (Fin n)) _
+P xs = ∀ ys → Suffix ys xs → (Sorted ∘ toList ∘ counts) ys
+
+data Motzkin {n} : List (Fin n) → Set where
+  base : Motzkin []
+  next : ∀ {x xs} → (Sorted ∘ toList ∘ counts) (x ∷ xs) → Motzkin xs → Motzkin (x ∷ xs)
+
+P⇔Motzkin : ∀ {n} xs → P {n} xs ⇔ Motzkin xs
+P⇔Motzkin xs = equivalence (⇒ xs) ⇐
+  where
+  ⇒ : ∀ xs → P xs → Motzkin xs
+  ⇒ [] pxs = base
+  ⇒ (x ∷ xs) pxs = next (pxs (x ∷ xs) (Suffix.refl refl)) (⇒ xs (λ ys ys<xs → pxs ys (next x ys<xs)))
+
+  ⇐ : ∀ {xs} → Motzkin xs → P xs
+  ⇐ base [] (base []) = sorted-0s
+  ⇐ (next counts↗ pxs) ys (base xs≋ys) = subst (Sorted ∘ toList ∘ counts) (sym (≋⇒≡ xs≋ys)) counts↗
+  ⇐ (next counts↗ pxs) ys (next _ ys<xs) = ⇐ pxs ys ys<xs
+
+extendUpdate : ∀ {n m} → Fin n → Vec (Fin n) m × Vec ℕ n → Vec (Fin n) (suc m) × Vec ℕ n
+extendUpdate x (xs , counts) = x ∷ xs , updateAt x suc counts
+
+extendUpdateCount : ∀ {n m x xs-counts} →
+                    proj₂ xs-counts ≡ (counts ∘ toList ∘ proj₁) xs-counts →
+                    (proj₂ ∘ extendUpdate {n} {m} x) xs-counts ≡ (counts ∘ toList ∘ proj₁ ∘ extendUpdate x) xs-counts
+extendUpdateCount refl = refl
+
+generate : ∀ n m → List (Vec (Fin n) m × Vec ℕ n)
+generate n zero    = ([] , replicate 0) ∷ []
+generate n (suc m) =
+  filter (sorted? _≤?_ ∘ toList ∘ proj₂)
+         (cartesianProductWith extendUpdate
+                               (allFin n)
+                               (generate n m))
+
+generate⇒counts : ∀ n m → All (λ (xs , cs) → cs ≡ counts (toList xs)) (generate n m)
+generate⇒counts n zero = refl ∷ []
+generate⇒counts n (suc m) =
+  AllP.filter⁺
+    (sorted? _≤?_ ∘ toList ∘ proj₂)
+    (AllP.cartesianProductWith⁺
+      (setoid (Fin n))
+      (setoid (Vec (Fin n) m × Vec ℕ n))
+      extendUpdate
+      (allFin n)
+      (generate n m)
+      (λ {x} {y} px py → extendUpdateCount {n} {m} {x} {y} (All.lookup (generate⇒counts n m) py)))
+
+generate⇒counts↗ : ∀ n m → All (Sorted ∘ toList ∘ counts ∘ toList ∘ proj₁) (generate n m)
+generate⇒counts↗ n zero = sorted-0s ∷ []
+generate⇒counts↗ n (suc m) =
+  All.zipWith
+    (λ (p₂≡cs , p₂↗) → subst (Sorted ∘ toList) p₂≡cs p₂↗)
+    ( generate⇒counts n (suc m)
+    , all-filter (sorted? _≤?_ ∘ toList ∘ proj₂)
+                 (cartesianProductWith extendUpdate (allFin n) (generate n m)))
+
+generate⇒next : ∀ n m → All (λ pair → ∃₂ λ y ys → proj₁ pair ≡ y ∷ (proj₁ ys) × ys ∈ generate n m) (generate n (suc m))
+generate⇒next n m =
+  AllP.filter⁺
+    (sorted? _≤?_ ∘ toList ∘ proj₂)
+    (AllP.cartesianProductWith⁺
+      (setoid (Fin n))
+      (setoid (Vec (Fin n) m × Vec ℕ n))
+      extendUpdate
+      (allFin n)
+      (generate n m)
+      λ px py → _ , _ , refl , py)
+
+generate⇒Motzkin : ∀ n m → All (Motzkin ∘ toList ∘ proj₁) (generate n m)
+generate⇒Motzkin n zero    = base ∷ []
+generate⇒Motzkin n (suc m) =
+  All.zipWith
+    (λ (counts↗ , y , ys , xs≡y∷ys , pys) →
+      subst
+        (Motzkin ∘ toList)
+        (sym xs≡y∷ys)
+        (next
+          (subst (Sorted ∘ toList ∘ counts ∘ toList) xs≡y∷ys counts↗)
+          (All.lookup (generate⇒Motzkin n m) pys)))
+    (generate⇒counts↗ n (suc m) , generate⇒next n m)
+
+Motzkin⇒generate : ∀ {n xs} → Motzkin xs → (xs , counts xs) ∈ map (map₁ toList) (generate n (length xs))
+Motzkin⇒generate base = here refl
+Motzkin⇒generate (next {x} {xs} counts↗ pxs) =
+  AnyP.map⁺
+    ([ id
+     , (λ ¬counts↗ → ⊥-elim (¬counts↗ (subst (Sorted ∘ toList) (,-injectiveʳ (lookup-result cpw)) counts↗)))
+     ] (AnyP.filter⁺ (sorted? _≤?_ ∘ toList ∘ proj₂) cpw))
+  where
+  cpw =
+    AnyP.cartesianProductWith⁺
+      extendUpdate
+      (λ { refl eq → cong (λ (xs , cs) → x ∷ xs , updateAt x suc cs) eq})
+      (AnyP.tabulate⁺ {P = x ≡_} x refl)
+      (AnyP.map⁻ (Motzkin⇒generate pxs))