diff options
Diffstat (limited to 'src/Motzkin.agda')
| -rw-r--r-- | src/Motzkin.agda | 147 |
1 files changed, 147 insertions, 0 deletions
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)) |