Rearrange a few functions

This commit is contained in:
Danila Fedorin 2023-07-30 13:49:38 -07:00
parent eaee73236f
commit af0066eaa7

View File

@ -152,22 +152,13 @@ private module ImplInsert (f : B → B → B) where
merge-preserves-Unique ((k₁ , v₁) xs₁) l₂ u₂ =
insert-preserves-Unique (merge-preserves-Unique xs₁ l₂ u₂)
insert-preserves-∈ : {k k' : A} {v v' : B} {l : List (A × B)}
¬ k k' (k , v) l (k , v) insert k' v' l
insert-preserves-∈ {k} {k'} {l = x xs} k≢k' (here k,v=x)
rewrite sym k,v=x with ≡-dec-A k' k
... | yes k'≡k = absurd (k≢k' (sym k'≡k))
... | no _ = here refl
insert-preserves-∈ {k} {k'} {l = (k'' , _) xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
insert-preserves-∈k : {k k' : A} {v' : B} {l : List (A × B)}
¬ k k' k ∈k l k ∈k insert k' v' l
insert-preserves-∈k k≢k' k∈kl =
let (v , k,v∈l) = locate k∈kl
in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
insert-fresh : {k : A} {v : B} {l : List (A × B)}
¬ k ∈k l (k , v) insert k v l
insert-fresh {l = []} k∉kl = here refl
insert-fresh {k} {l = (k' , v') xs} k∉kl
with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = there (insert-fresh (λ k∈kxs k∉kl (there k∈kxs)))
insert-preserves-∉k : {k k' : A} {v' : B} {l : List (A × B)}
¬ k k' ¬ k ∈k l ¬ k ∈k insert k' v' l
@ -191,23 +182,32 @@ private module ImplInsert (f : B → B → B) where
... | yes k≡k' = absurd (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉k k≢k' (merge-preserves-∉ (λ k∈kxs₁ k∉kl₁ (there k∈kxs₁)) k∉kl₂)
insert-preserves-∈ : {k k' : A} {v v' : B} {l : List (A × B)}
¬ k k' (k , v) l (k , v) insert k' v' l
insert-preserves-∈ {k} {k'} {l = x xs} k≢k' (here k,v=x)
rewrite sym k,v=x with ≡-dec-A k' k
... | yes k'≡k = absurd (k≢k' (sym k'≡k))
... | no _ = here refl
insert-preserves-∈ {k} {k'} {l = (k'' , _) xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
insert-preserves-∈k : {k k' : A} {v' : B} {l : List (A × B)}
¬ k k' k ∈k l k ∈k insert k' v' l
insert-preserves-∈k k≢k' k∈kl =
let (v , k,v∈l) = locate k∈kl
in ∈-cong proj₁ (insert-preserves-∈ k≢k' k,v∈l)
merge-preserves-∈₁ : {k : A} {v : B} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ (k , v) l₂ (k , v) merge l₁ l₂
¬ k ∈k l₁ (k , v) l₂ (k , v) merge l₁ l₂
merge-preserves-∈₁ {l₁ = []} _ k,v∈l₂ = k,v∈l₂
merge-preserves-∈₁ {l₁ = (k' , v') xs₁} k∉kl₁ k,v∈l₂ =
let recursion = merge-preserves-∈₁ (λ k∈xs₁ k∉kl₁ (there k∈xs₁)) k,v∈l₂
in insert-preserves-∈ (λ k≡k' k∉kl₁ (here k≡k')) recursion
insert-fresh : {k : A} {v : B} {l : List (A × B)}
¬ k ∈k l (k , v) insert k v l
insert-fresh {l = []} k∉kl = here refl
insert-fresh {k} {l = (k' , v') xs} k∉kl
with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = there (insert-fresh (λ k∈kxs k∉kl (there k∈kxs)))
merge-preserves-∈₂ : {k : A} {v : B} {l₁ l₂ : List (A × B)}
Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) merge l₁ l₂
Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) merge l₁ l₂
merge-preserves-∈₂ {k} {v} {(k' , v') xs₁} (push k'≢xs₁ uxs₁) (there k,v∈xs₁) k∉kl₂ =
insert-preserves-∈ k≢k' k,v∈mxs₁l
where