1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
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))
|
