【发布时间】：2020-06-29 17:21:11
【问题描述】：
标准库的 AVL 树实现使用依赖对来存储键值对。我有两个这样的对，它们的键（k 和 k′）我已经证明是相等的（k≡k′）。它们还包含相同的值 (v)。我想证明这对是平等的。这是目标：
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′ = {!!}
我尝试使用k≡k′ 重写，这会将LHS 上的k 变成k′ 和RHS 上的k≡k′ 变成refl。这就是我卡住的地方。我觉得我遗漏了一些明显的东西，因为这似乎是一件非常基本的事情。
（作为练习，我试图证明标准库的 AVL 树插入是正确的。因此我最近对它的 AVL 树代码很着迷。）
更新
嗯。也许这并不像我想象的那么微不足道，至少在不了解V 的情况下。毕竟，我目前所知道的是：
-
有一种方法可以将
Val k类型的值转换为Val k′类型的值 - 通过V≈。 -
V≈ refl接受Val foo并返回Val foo。
目前我不知道V≈ refl 是身份函数，这似乎是我需要做的证明。
更新二
例如，如果我知道 V≈ 实际上是 subst Val，那么我的证明将是：
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
所以，我想我的问题最终是：
-
我可以用我现有的东西完成我的原始证明吗？
-
如果不是，那么我需要什么属性
V≈才能完成我的原始证明（即“将其限制为类似于subst的函数”）？
更新 III
我正在提供更多背景信息来回应 MrO 的评论。我将提供更简单的东西，而不是剥离我的实际证明。让我们证明一个 AVL 树插入的特殊情况，这会导致我在一般情况下面临的相同问题。
让我们证明，将键 k 的值 v 插入到空树中，然后查找键 k 的值会产生我们插入的值 v。
让我们开始吧：
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
现在，一个创建空树的函数：
make-empty : ∀ {l u} → l <⁺ u → Tree V l u 0
make-empty = leaf
还有证明：
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 = {!!}
我要填写的目标是just (V≈ refl v) ≡ just v。
【问题讨论】：
-
关于您的第二次更新：您的证明可以简单地使用
proof′ _ _ _ refl = refl，也可以不使用subst Val k≡k′ v，您不能简单地使用v吗？我对您的问题真正需要证明的内容感到困惑。 -
感谢您对此进行调查！让我试着改写一下。
V≈ : x ≡ y → Val x → Val y是一个类似于subst的函数，用于将Val x类型的值转换为Val y类型的值。它是 AVL 树模块的参数，所以我不知道它的定义，只知道它的类型。我想在从subst到V≈的第二次更新中概括证明。据我了解，我第二次更新中的证明使用了subst P refl是恒等函数这一事实，因此subst Val k≡k′ v ≡ v。我似乎无法将这个事实用于V≈，因为我不知道V≈ refl是身份函数。 -
所有这些来自哪里：给定一个 AVL 树，其值
v′ : Val k′位于键k′ : ℕ，使用键k : ℕ在树中查找k ≡ k′。查找在树中找到值v′ : Val k′。 AVL 代码现在使用V≈将v′从Val k′转换为Val k以返回。我们使用k而不是k′进行了查找，所以我们得到了Val k- 即使k ≡ k′。在我关于 AVL 树插入的证明中，我被困在V≈ refl v′ ≡ v′。在我看来，如果不了解更多关于V≈的信息，我将无法继续。所以我想知道我是否遗漏了什么。 -
能否将您刚才描述的关于查找的完整证明添加到您的帖子中？
-
谢谢！我还试图探索的另一件事（在我有限的理解范围内）是
Val k的某种唯一性或不相关属性，因此类型的相等意味着值的相等。如果我理解正确，那么我们不需要知道任何关于V≈ refl的信息，除了它需要一个Val k并产生一个Val k。
标签： agda