Add intermediate state for insertion proofs

This commit is contained in:
Danila Fedorin 2023-07-25 22:58:42 -07:00
parent 6b51cd4050
commit 489b0532df

View File

@ -12,15 +12,14 @@ import Data.List.Membership.Propositional as MemProp
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
open import Data.Nat using () open import Data.Nat using ()
open import Data.List using (List; []; _∷_; _++_) open import Data.List using (List; map; []; _∷_; _++_)
open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Data.Empty using () open import Data.Empty using ()
keys : List (A × B) List A keys : List (A × B) List A
keys [] = [] keys = map proj₁
keys ((k , v) xs) = k keys xs
data Unique {c} {C : Set c} : List C Set c where data Unique {c} {C : Set c} : List C Set c where
empty : Unique [] empty : Unique []
@ -63,6 +62,7 @@ private module ImplRelation (_≈_ : B → B → Set b) where
subset m₁ m₂ = (k : A) (v : B) (k , v) m₁ Σ B (λ v' v v' × ((k , v') m₂)) subset m₁ m₂ = (k : A) (v : B) (k , v) m₁ Σ B (λ v' v v' × ((k , v') m₂))
private module ImplInsert (f : B B B) where private module ImplInsert (f : B B B) where
open import Data.List using (map)
open MemProp using (_∈_) open MemProp using (_∈_)
private private
@ -117,6 +117,52 @@ private module ImplInsert (f : B → B → B) where
merge-preserves-Unique [] l₂ u₂ = u₂ merge-preserves-Unique [] l₂ u₂ = u₂
merge-preserves-Unique ((k₁ , v₁) xs₁) l₂ u₂ = insert-preserves-Unique k₁ v₁ (merge xs₁ l₂) (merge-preserves-Unique xs₁ l₂ u₂) merge-preserves-Unique ((k₁ , v₁) xs₁) l₂ u₂ = insert-preserves-Unique k₁ v₁ (merge xs₁ l₂) (merge-preserves-Unique xs₁ l₂ u₂)
insert-preserves-other-keys : (k k' : A) (v v' : B) (l : List (A × B)) ¬ k k' (k , v) l (k , v) insert k' v' l
insert-preserves-other-keys k k' v v' (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-other-keys k k' v v' ((k'' , _) xs) k≢k' (there k,v∈xs) with ≡-dec-A k' k''
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-other-keys k k' v v' xs k≢k' k,v∈xs)
merge-preserves-keys₁ : (k : A) (v : B) (l₁ l₂ : List (A × B)) ¬ k ∈k l₁ (k , v) l₂ (k , v) merge l₁ l₂
merge-preserves-keys₁ k v [] l₂ _ k,v∈l₂ = k,v∈l₂
merge-preserves-keys₁ k v ((k' , v') xs₁) l₂ k∉kl₁ k,v∈l₂ =
let recursion = merge-preserves-keys₁ k v xs₁ l₂ (λ k∈xs₁ k∉kl₁ (there k∈xs₁)) k,v∈l₂
in insert-preserves-other-keys k k' v v' _ (λ k≡k' k∉kl₁ (here k≡k')) recursion
insert-preserves-other-key : (k : A) (v : B) (l : List (A × B)) ¬ k ∈k l (k , v) insert k v l
insert-preserves-other-key k v [] k∉kl = here refl
insert-preserves-other-key k v ((k' , v') xs) k∉kl with ≡-dec-A k k'
... | yes k≡k' = absurd (k∉kl (here k≡k'))
... | no _ = there (insert-preserves-other-key k v xs (λ k∈kxs k∉kl (there k∈kxs)))
∈-cong : {c d} {C : Set c} {D : Set d} {c : C} {l : List C} (f : C D) c l f c map f l
∈-cong f (here c≡c') = here (cong f c≡c')
∈-cong f (there c∈xs) = there (∈-cong f c∈xs)
-- prove that ¬ k ∈k m → (k , v) ∈ insert k v m
merge-preserves-keys₂ : (k : A) (v : B) (l₁ l₂ : List (A × B)) Unique (keys l₁) (k , v) l₁ ¬ k ∈k l₂ (k , v) merge l₁ l₂
merge-preserves-keys₂ k v ((k' , v') xs₁) l₂ (push k'≢xs₁ uxs₁) (here _) k∉kl₂ = {!!} -- hard!
-- where
-- rest : ∀ (l l' : List (A × B)) → All (λ k'' → ¬ k ≡ k'') (keys l) → ¬ k ∈k l' → ¬ k ∈k merge l l'
-- rest [] l' _ k∉kl' = k∉kl'
-- rest l [] (k≢l) _ = help
-- where
-- help : ∀ (l : List (A × B)) → All (λ k'' → ¬ k ≡ k'') (keys l) → ¬ k ∈k l
-- help [] _ ()
-- help ((k'' , _) ∷ xs) (k≢k'' ∷ k≢xs) (here k≡k'') = k≢k'' k≡k''
-- help ((k'' , _) ∷ xs) (k≢k'' ∷ k≢xs) (there k∈kxs) = help xs k≢xs k∈kxs
-- -- rest (x@(k'' , _) ∷ xs) l' (k≢k'' ∷ k≢xs) k∉kl' with (≡-dec-A k'' = (rest xs l' k≢xs k∉kl')
-- -- where
-- -- help : ¬ k ∈k (merge (x ∷ xs) l') -- insert x (merge xs l')
-- -- help (here k≡k'') = {!!}
-- -- help (there k∈) = {!!}
-- -- let nested = (rest xs l' k≢xs k∉kl')
Map : Set (a b) Map : Set (a b)
Map = Σ (List (A × B)) (λ l Unique (keys l)) Map = Σ (List (A × B)) (λ l Unique (keys l))
@ -154,6 +200,27 @@ module _ (f : B → B → B) where
merge-provenance : (m₁ m₂ : Map) (k : A) k ∈k merge m₁ m₂ Σ (Provenance k m₁ m₂) MergeResult merge-provenance : (m₁ m₂ : Map) (k : A) k ∈k merge m₁ m₂ Σ (Provenance k m₁ m₂) MergeResult
merge-provenance = {!!} merge-provenance = {!!}
-- ------------------------------------------------------------------------
--
-- The following can be proven using plain properties of insert:
--
-- prove that ¬ k ∈k m₁ → (k , v) ∈ m₂ → (k , v) ∈ merge m₁ m₂ (done)
-- prove that k ≢ k' → (k , v) ∈ m → (k , v) ∈ insert k' v' m (done)
-- prove that (k , v) ∈ m₁ → ¬ k ∈k m₂ → (k , v) ∈ merge m₁ m₂ (stuck)
-- prove that ¬ k ∈k m → (k , v) ∈ insert k v m
--
-- ------------------------------------------------------------------------
--
-- The following relies on uniqueness, since inserts stops after the first encounter.
--
-- prove that (k , v) ∈ m₁ → (k , v') ∈ m₂ → (k, f v v') ∈ merge m₁ m₂
--
-- ------------------------------------------------------------------------
--
-- The following can probably be proven via keys.
--
-- prove that k ∉k m₁ → k ∉k m₂ → k ∉k merge m₁ m₂
module _ (_≈_ : B B Set b) where module _ (_≈_ : B B Set b) where
open ImplRelation _≈_ renaming (subset to subset-impl) open ImplRelation _≈_ renaming (subset to subset-impl)