Proving two dependent (AVL tree key-value) pairs equal

Question

The standard library's AVL tree implementation uses dependent pairs to store key-value pairs. I have two such pairs whose keys (k and k′) I have shown to be equal (k≡k′). They also contain the same value (v). I'd like to prove that the pairs are equal. Here's the goal:

open import Agda.Primitive

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Data.AVL.Indexed <-strictTotalOrder

module Repro (ℓ : Level) (V : Value ℓ) where

Val = Value.family V
V≈ = Value.respects V

proof : (k k′ : ℕ) → (v : Val k) → (k≡k′ : k ≡ k′) → (k , v) ≡ (k′ , V≈ k≡k′ v)
proof k k′ v k≡k′ = {!!}

I tried rewriting with k≡k′, which turns k on the LHS into k′ and k≡k′ on the RHS into refl. That's where I get stuck. I feel like I'm missing something obvious, as this seems a pretty basic thing to do.

(As an exercise, I'm trying to prove the standard library's AVL tree insertion correct. Hence my recent obsession with its AVL tree code.)

Update

Hmm. Maybe this isn't as trivial as I thought, at least without knowing more about V. After all, what I currently know is that:

There's a way to turn a value of type Val k into a value of type Val k′ - by way of V≈.
That V≈ refl takes a Val foo and returns a Val foo.

What I don't know at this point is that V≈ refl is the identity function, which seems to be what I'd need to do my proof.

Update II

If, for example, I knew that V≈ was actually subst Val, then my proof would be:

proof′ : (k k′ : ℕ) → (v : Val k) → (k≡k′ : k ≡ k′) → (k , v) ≡ (k′ , subst Val k≡k′ v)
proof′ k k′ v k≡k′ rewrite k≡k′ = cong (k′ ,_) refl

So, I guess my question ultimately is:

Can I complete my original proof with what I have?
If not, then what property do I need V≈ to have to complete my original proof (i.e., to "restrict it to functions that are like subst")?

Update III

I am providing more context in response to MrO's comment. Instead of stripping down my actual proof, I'll provide something even simpler. Let's prove a special case of AVL tree insertion, which leads to the same problem that I'm facing in the general case.

Let's prove that inserting a value v for key k into an empty tree and then looking up the value for key k yields the value v that we inserted.

Let's get set up:

open import Agda.Primitive using (Level)
open import Data.Maybe using (just)
open import Data.Nat using (ℕ)
open import Data.Nat.Properties using (<-strictTotalOrder ; <-cmp)
open import Data.Product using (proj₂)
open import Function using () renaming (const to constᶠ)
open import Relation.Binary using (tri< ; tri≈ ; tri>)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl )
open import Relation.Nullary.Negation using (contradiction)

open import Data.AVL.Indexed <-strictTotalOrder

module Simple {ℓ : Level} (V : Value ℓ) where

private
  Val = Value.family V
  V≈  = Value.respects V

Now, a function to create an empty tree:

make-empty : ∀ {l u} → l <⁺ u → Tree V l u 0
make-empty = leaf

And the proof:

proof : ∀ {l u} (k : ℕ) (v : Val k) (l<u : l <⁺ u) (l<k<u : l < k < u) →
  lookup k (proj₂ (insertWith k (constᶠ v) (make-empty l<u) l<k<u)) l<k<u ≡ just v

proof k v l<u l<k<u with <-cmp k k
... | tri< _ p _ = contradiction refl p
... | tri> _ p _ = contradiction refl p
... | tri≈ _ p _ rewrite p = {!!}

The goal that I'm trying to fill in is just (V≈ refl v) ≡ just v.

About your second update: your proof can simply be proof′ _ _ _ refl = refl and also instead of using subst Val k≡k′ v couldn't you simply use v ? I'm confused as to what really needs to be proved in your question. — MrO
Thank you for looking into this! Let me try to rephrase. V≈ : x ≡ y → Val x → Val y is a subst-like function for turning a value of type Val x into a value of type Val y. It is a parameter to the AVL tree module, so I don't know its definition, only its type. I'd like to generalize the proof in my second update from subst to V≈. As I understand it, the proof in my second update uses the fact that subst P refl is the identity function, so that subst Val k≡k′ v ≡ v. I can't seem to use this fact for V≈, as I don't know that V≈ refl is the identity function. — 123omnomnom
Where all of this comes from: Given an AVL tree with a value v′ : Val k′ at key k′ : ℕ, do a lookup in the tree with a key k : ℕ where k ≡ k′. The lookup finds the value v′ : Val k′ in the tree. The AVL code now uses V≈ to turn v′ from a Val k′ into a Val k to return. We did the lookup with k and not k′, so we get back a Val k - even though k ≡ k′. In my proof about AVL tree insertion I am stuck at V≈ refl v′ ≡ v′. It seems to me that I cannot proceed without knowing more about V≈. And so I wonder whether I am missing anything. — 123omnomnom
Could you please add the englobing proof about lookup which you just described to your post ? — MrO
Thanks! One other thing that I tried to also explore (within the limits of my limited understanding) was some kind of uniqueness or irrelevance property for Val k, so that equality of types would imply equality of values. If I understand things correctly, then we wouldn't need to know anything about V≈ refl other than the fact that it takes a Val k and produces a Val k. — 123omnomnom

MrO MrO · Accepted Answer · 2020-07-01T19:09:44

You could postulate, or take as a module parameter, the fact that V≈ leaves the value unchanged, as follows:

postulate lemma : ∀ {k k′} {v : Val k} → (k≡k′ : k ≡ k′) → v ≡ subst _ (sym k≡k′) (V≈ k≡k′ v)

After that, your proof becomes:

proof : (k k′ : ℕ) → (v : Val k) → (k≡k′ : k ≡ k′) → (k , v) ≡ (k′ , V≈ k≡k′ v) 
proof k ._ _ refl = cong (k ,_) (lemma refl)

Proving two dependent (AVL tree key-value) pairs equal

1 Answers