[ refactor ] downstream improvements following #2961 / #2968#2970
[ refactor ] downstream improvements following #2961 / #2968#2970jamesmckinna wants to merge 13 commits intoagda:masterfrom
Conversation
…vel parameterisation; fix ref. to `lookup`
jamesmckinna
added
status: blocked-by-issue
| Please use insertWith-nothing instead." | ||
| #-} | ||
| Any-insertWith-just = insertWith-just | ||
| {-# WARNING_ON_USAGE Any-insertWith-just |
There was a problem hiding this comment.
It seems like Any-insertWith-just isn't general enough, which might be related to deprecating with name changes. Not sure if there's a standard practice for how to chose new names when the old lemma isn't general enough, but I thought I'd mention it here.
The problem with Any-insertWith-just is (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))). See that v is not constrained to be the preexisting v in the old tree. So this is good enough to prove Any-insert-just, which ignores the v anyway, but doesn't seem useful when insertWith is used with a non-trivial function.
One possible fix is:
Any-insertWith-just-strong :
(∀ k′ v → (eq : k ≈ k′) → Q (k′ , v) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
(q : Any Q t) → k ≈ lookupKey q →
Any P (proj₂ (insertWith k f t seg))
The proof of this happens to be almost exactly a copy and paste of the existing Any-insertWith-just.
There was a problem hiding this comment.
Nice! Thanks very much.
The thing to do in such circumstances would be to fix the type of the 'new' functions, and deprecate the old, but noting that the type has improved. At least if I recall previous episodes of this character... will look properly in the morning soon!
There was a problem hiding this comment.
So... I've been thinking about your comment a bit more (but not really doing any proof), and your generalisation, while it seems stronger, perhaps may also be refactored via the existing proof and Properties.Lookup.lookup-rebuild?
|
|
||
| ∈ₖᵥ-singleton⁺ : (k , x) ∈ₖᵥ singleton k x | ||
| ∈ₖᵥ-singleton⁺ = tree (IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl)) | ||
| ∈ₖᵥ-singleton⁺ = tree {!IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl)!} |
There was a problem hiding this comment.
Not the end of the world as this is 'Draft', but it's still bad to leave in holes (here and in next function).
|
|
||
| open import Data.Nat.Base | ||
| open import Data.Fin.Base using (Fin; zero; suc) | ||
| open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) |
There was a problem hiding this comment.
Hmm, should Height be defined in this file, and its properties in a .Properties file?
| import Function.Base as F | ||
| open Setoid S renaming (Carrier to Key) | ||
| open import Level using (Level; suc; _⊔_) | ||
| import Function.Base as Function |
There was a problem hiding this comment.
Can't const and id just be imported directly?
3 participants
DRAFT: for rebasing against #2968 in due course. If #2968 does indeed get merged, then this PR revolves entirely around the properties of
Map.Membership, and we may wish to revisit/refactorthat separately (under the usualSetoid/Propositionaldistinction?)Notes to self (and others):
Data.Tree.AVL.Map.Membership.Propositionalto do with liftingrespectsfields fromKtoK × Vfor the case whereVequality isPropositional... but real sense of why these arise, when they don't seem to under Add properties that characterizeData.Tree.AVL.Indexed.delete. #2961 or [ refactor ] Infrastructure forData.Tree.AVL.Indexed.*#2968... advice welcome!? UPDATED they seem to disappear under the latest version of [ refactor ] Infrastructure forData.Tree.AVL.Indexed.*#2968 !?