DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Tweak signature of 'forget' to simplify proofs

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-07 20:04:33 -08:00
parent 34203840c8
commit 7905d106e2
2 changed files with 20 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Lattice/FiniteValueMap.agda
View File

@ -185,7 +185,7 @@ module IterProdIsomorphism where
narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = ... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁)) ⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁))
... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) = ... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
(v'' , (v'≈v'' , k',v'∈fm'₂)) (v'' , (v'≈v'' , k',v'∈fm'₂))
@ -196,7 +196,7 @@ module IterProdIsomorphism where
k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
(k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm)) (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm = k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
( (λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) }) ( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) })
, there k',v∈fm , there k',v∈fm
) )
@ -215,11 +215,11 @@ module IterProdIsomorphism where
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂ Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂ with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
... | in₁ (single k,v∈m₁) k∉km₂ ... | in₁ (single k,v∈m₁) k∉km₂
with k∈km₁ ← (forget {m = m₁} k,v∈m₁) with k∈km₁ ← (forget k,v∈m₁)
rewrite trans ks₁≡ks (sym ks₂≡ks) = rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₂ k∈km₁) ⊥-elim (k∉km₂ k∈km₁)
... | in₂ k∉km₁ (single k,v∈m₂) ... | in₂ k∉km₁ (single k,v∈m₂)
with k∈km₂ ← (forget {m = m₂} k,v∈m₂) with k∈km₂ ← (forget k,v∈m₂)
rewrite trans ks₁≡ks (sym ks₂≡ks) = rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₁ k∈km₂) ⊥-elim (k∉km₁ k∈km₂)
... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) = ... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
@ -324,11 +324,9 @@ module IterProdIsomorphism where
| from-first-value (fm₁ ⊔ᵐ fm₂) | from-first-value (fm₁ ⊔ᵐ fm₂)
| from-first-value fm₁ | from-first-value fm₂ | from-first-value fm₁ | from-first-value fm₂
... | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl ... | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂) with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂)
... | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂} ... | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂))
k,v₂∈fm₂)) ... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁))
... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁}
k,v₁∈fm₁))
... | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂)) ... | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁ rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂ rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
@ -387,10 +385,10 @@ module IterProdIsomorphism where
(v , (IsLattice.≈-refl lB , here refl)) (v , (IsLattice.≈-refl lB , here refl))
... | here refl | there k',v₂∈fm₂' = ... | here refl | there k',v₂∈fm₂' =
⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂') ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
(forget {m = proj₁ fm₂'} k',v₂∈fm₂'))) (forget k',v₂∈fm₂')))
... | there k',v₁∈fm₁' | here refl = ... | there k',v₁∈fm₁' | here refl =
⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁') ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
(forget {m = proj₁ fm₁'} k',v₁∈fm₁'))) (forget k',v₁∈fm₁')))
... | there k',v₁∈fm₁' | there k',v₂∈fm₂' = ... | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
let let
k',v₁v₂∈fm₁'fm₂' = k',v₁v₂∈fm₁'fm₂' =

20
Lattice/Map.agda
View File

@ -488,7 +488,9 @@ _∈k_ k m = MemProp._∈_ k (keys m)
locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m) locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m)
locate k∈km = locate-impl k∈km locate k∈km = locate-impl k∈km
forget : ∀ {k : A} {v : B} {m : Map} → (k , v) ∈ m → k ∈k m -- defined this way because ∈ for maps uses projection, so the full map can't be guessed.
-- On the other hand, list can be guessed.
forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l)
forget = ∈-cong proj₁ forget = ∈-cong proj₁
Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v' Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
@ -594,7 +596,7 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
Expr-Provenance-≡ : ∀ {k : A} {v : B} (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e Expr-Provenance-≡ : ∀ {k : A} {v : B} (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
Expr-Provenance-≡ {k} {v} e k,v∈e Expr-Provenance-≡ {k} {v} e k,v∈e
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget {m = ⟦ e ⟧} k,v∈e) with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
module _ (≈₂-dec : IsDecidable _≈₂_) where module _ (≈₂-dec : IsDecidable _≈₂_) where
@ -609,7 +611,7 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
let (v , k,v∈m₁) = locate-impl k∈km₁ let (v , k,v∈m₁) = locate-impl k∈km₁
in no (λ m₁⊆m₂ → in no (λ m₁⊆m₂ →
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁ let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
in k∉km₂ (∈-cong proj₁ k,v'∈m₂)) in k∉km₂ (forget k,v'∈m₂))
SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) = SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
no (λ m₁⊆m₂ → no (λ m₁⊆m₂ →
let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁ let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
@ -979,7 +981,7 @@ updating-via-k∈ks-forward m {ks} f k∈ks k∈km rewrite transform-keys-≡ (p
updating-via-k∈ks-≡ : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} → updating-via-k∈ks-≡ : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
k ∈ˡ ks → (k , v) ∈ (m updating ks via f)→ v ≡ f k k ∈ˡ ks → (k , v) ∈ (m updating ks via f)→ v ≡ f k
updating-via-k∈ks-≡ m {ks} f k∈ks k,v∈um updating-via-k∈ks-≡ m {ks} f k∈ks k,v∈um
with updating-via-k∈ks m f k∈ks (forget {m = (m updating ks via f)} k,v∈um) with updating-via-k∈ks m f k∈ks (forget k,v∈um)
... | k,fk∈um = Map-functional {m = (m updating ks via f)} k,v∈um k,fk∈um ... | k,fk∈um = Map-functional {m = (m updating ks via f)} k,v∈um k,fk∈um
updating-via-k∉ks-forward : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} → updating-via-k∉ks-forward : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
@ -1017,11 +1019,11 @@ module _ {l} {L : Set l}
with Expr-Provenance-≡ ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂ with Expr-Provenance-≡ ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
... | in₁ (single k,v∈f'l₁) k∉kf'l₂ = ... | in₁ (single k,v∈f'l₁) k∉kf'l₂ =
let let
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget {m = f' l₁} k,v∈f'l₁) k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget k,v∈f'l₁)
k∈kfl₁fl₂ = union-preserves-∈k₁ {l₁ = proj₁ (f l₁)} {l₂ = proj₁ (f l₂)} k∈kfl₁ k∈kfl₁fl₂ = union-preserves-∈k₁ {l₁ = proj₁ (f l₁)} {l₂ = proj₁ (f l₂)} k∈kfl₁
(v' , k,v'∈fl₁l₂) = locate {m = (f l₁ ⊔ f l₂)} k∈kfl₁fl₂ (v' , k,v'∈fl₁l₂) = locate {m = (f l₁ ⊔ f l₂)} k∈kfl₁fl₂
(v'' , (v'≈v'' , k,v''∈fl₂)) = fl₁fl₂⊆fl₂ k v' k,v'∈fl₁l₂ (v'' , (v'≈v'' , k,v''∈fl₂)) = fl₁fl₂⊆fl₂ k v' k,v'∈fl₁l₂
k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget {m = f l₂} k,v''∈fl₂) k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget k,v''∈fl₂)
in in
⊥-elim (k∉kf'l₂ k∈kf'l₂) ⊥-elim (k∉kf'l₂ k∈kf'l₂)
... | in₂ k∉kf'l₁ (single k,v'∈f'l₂) = ... | in₂ k∉kf'l₁ (single k,v'∈f'l₂) =
@ -1044,7 +1046,7 @@ module _ {l} {L : Set l}
f'l₂⊆f'l₁f'l₂ : f' l₂ ⊆ ((f' l₁) ⊔ (f' l₂)) f'l₂⊆f'l₁f'l₂ : f' l₂ ⊆ ((f' l₁) ⊔ (f' l₂))
f'l₂⊆f'l₁f'l₂ k v k,v∈f'l₂ f'l₂⊆f'l₁f'l₂ k v k,v∈f'l₂
with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget {m = f' l₂} k,v∈f'l₂) with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget k,v∈f'l₂)
with (v' , k,v'∈fl₂) ← locate {m = f l₂} k∈kfl₂ with (v' , k,v'∈fl₂) ← locate {m = f l₂} k∈kfl₂
with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) ← fl₂⊆fl₁fl₂ k v' k,v'∈fl₂ with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) ← fl₂⊆fl₁fl₂ k v' k,v'∈fl₂
with Expr-Provenance-≡ ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂ with Expr-Provenance-≡ ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
@ -1058,8 +1060,8 @@ module _ {l} {L : Set l}
with k∈-dec k ks with k∈-dec k ks
... | yes k∈ks with refl ← updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v∈f'l₂ = ... | yes k∈ks with refl ← updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v∈f'l₂ =
let let
k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget {m = f l₁} k,v₁∈fl₁) k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget k,v₁∈fl₁)
k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget {m = f l₂} k,v₂∈fl₂) k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget k,v₂∈fl₂)
k,uv₁uv₂∈f'l₁f'l₂ = ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,uv₁∈f'l₁ k,uv₂∈f'l₂ k,uv₁uv₂∈f'l₁f'l₂ = ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,uv₁∈f'l₁ k,uv₂∈f'l₂
in in
(updater l₁ k ⊔₂ updater l₂ k , (IsLattice.≈-sym lB (g-Monotonicʳ k l₁≼l₂) , k,uv₁uv₂∈f'l₁f'l₂)) (updater l₁ k ⊔₂ updater l₂ k , (IsLattice.≈-sym lB (g-Monotonicʳ k l₁≼l₂) , k,uv₁uv₂∈f'l₁f'l₂))