Agda实例搜索遇多等价解失败问题求助

问题描述 #

Agda的实例搜索要求找到的候选解唯一，官方文档提到若所有候选解等价则可正常使用，但实际场景中遇到了问题：

• 定义了布尔玫瑰树Rose，以及见证所有节点为真/假的Trues/Falses类型
• 实现了翻转玫瑰树布尔值的Opp函数，以及从Trues x推导Falses (Opp x)的OppTF实例
• 对于Falses (B [])，存在两个候选解：直接使用Falses的构造器TFalses ⦃ VFalses' ⦄，或通过OppTF推导得到
• 已通过uniq函数证明这两个解等价，但Agda未自动识别，导致实例搜索失败
• 后续需要使用该证明，因此无法将实例标记为证明无关性（.{{ _ : Falses x }}）

期望实现以下任一目标：

• 让Agda完全归一化候选解，自动识别等价性
• 利用已有的等价性证明uniq说服Agda候选解等价
• 让Agda忽略重复候选且不将证明设为无关性

代码示例 #

module Example where

open import Data.List
open import Data.Bool
open import Relation.Binary.PropositionalEquality

data Rose : Set where
    V : Bool → Rose
    B : List Rose → Rose

Opp : Rose → Rose
Opp' : List Rose → List Rose

Opp (V x) = V (not x)
Opp (B xs) = B (Opp' xs)

Opp' [] = []
Opp' (x ∷ xs) = Opp x ∷ Opp' xs

data Trues : Rose → Set
data Trues' : List Rose → Set

data Trues where
    instance VTrues : Trues (V true)
    instance TTrues : ∀ {ts} ⦃ _ : Trues' ts ⦄ → Trues (B ts)
    
data Trues' where
    instance VTrues' : Trues' []
    instance TTrues' : ∀ {t ts} ⦃ _ : Trues t ⦄ ⦃ _ : Trues' ts ⦄ → Trues' (t ∷ ts)

data Falses : Rose → Set
data Falses' : List Rose → Set

data Falses where
    instance VFalses : Falses (V false)
    instance TFalses : ∀ {ts} ⦃ _ : Falses' ts ⦄ → Falses (B ts)
    
data Falses' where
    instance VFalses' : Falses' []
    instance TFalses' : ∀ {t ts} ⦃ _ : Falses t ⦄ ⦃ _ : Falses' ts ⦄ → Falses' (t ∷ ts)

instance
    OppTF : ∀ {x} ⦃ _ : Trues x ⦄ → Falses (Opp x)
    OppTF' : ∀ {xs} ⦃ _ : Trues' xs ⦄ → Falses' (Opp' xs)

    OppTF {x} ⦃ VTrues ⦄ = VFalses
    OppTF {x} ⦃ TTrues ⦃ xs ⦄ ⦄ = TFalses ⦃ OppTF' ⦃ xs ⦄ ⦄

    OppTF' {[]} ⦃ VTrues' ⦄ = VFalses'
    OppTF' {x ∷ xs} ⦃ TTrues' ⦃ p ⦄ ⦃ ps ⦄ ⦄ = TFalses' ⦃ OppTF ⦃ p ⦄ ⦄ ⦃ OppTF' ⦃ ps ⦄ ⦄

data Str : Rose → Set where
    Tor : ∀ {x : Rose} → Str x

dummy : ∀ {x : Rose} ⦃ _ : Falses x ⦄ → Rose
dummy {x} = x

test : Rose
test = dummy {B []}

uniq : ∀ {p : Falses (B [])} → p ≡ TFalses ⦃ VFalses' ⦄
uniq {TFalses {_} ⦃ VFalses' ⦄} = refl

错误信息 #

Failed to solve the following constraints:
  Resolve instance argument _70 : Falses (B [])
  Candidates
    TFalses : {ts : List Rose} ⦃ _ : Falses' ts ⦄ → Falses (B ts)
    OppTF : {x : Rose} ⦃ _ : Trues x ⦄ → Falses (Opp x)
    (stuck)

解决方案 #

方法1：调整实例优先级（最直接有效） #

Agda支持给实例设置优先级，优先级数值越高，实例搜索时越优先被选中。我们可以给Falses和Falses'的直接构造器设置更高优先级，让Agda优先选择它们，避免与OppTF类实例产生冲突：

修改Falses和Falses'的构造器定义，添加instance-priority注解：

data Falses where
    instance-priority 10
    instance VFalses : Falses (V false)
    instance-priority 10
    instance TFalses : ∀ {ts} ⦃ _ : Falses' ts ⦄ → Falses (B ts)
    
data Falses' where
    instance-priority 10
    instance VFalses' : Falses' []
    instance-priority 10
    instance TFalses' : ∀ {t ts} ⦃ _ : Falses t ⦄ ⦃ _ : Falses' ts ⦄ → Falses' (t ∷ ts)

同时给OppTF和OppTF'设置更低的优先级（比如默认的0），确保它们不会抢占直接构造器的优先级：

instance
    instance-priority 0
    OppTF : ∀ {x} ⦃ _ : Trues x ⦄ → Falses (Opp x)
    instance-priority 0
    OppTF' : ∀ {xs} ⦃ _ : Trues' xs ⦄ → Falses' (Opp' xs)

    -- 原OppTF和OppTF'的定义保持不变
    OppTF {x} ⦃ VTrues ⦄ = VFalses
    OppTF {x} ⦃ TTrues ⦃ xs ⦄ ⦄ = TFalses ⦃ OppTF' ⦃ xs ⦄ ⦄

    OppTF' {[]} ⦃ VTrues' ⦄ = VFalses'
    OppTF' {x ∷ xs} ⦃ TTrues' ⦃ p ⦄ ⦃ ps ⦄ ⦄ = TFalses' ⦃ OppTF ⦃ p ⦄ ⦄ ⦃ OppTF' ⦃ ps ⦄ ⦄

这样Agda在搜索Falses (B [])的实例时，会优先选择TFalses ⦃ VFalses' ⦄，不会触发OppTF的候选，解决解析失败问题。

方法2：限制OppTF的适用范围 #

通过模式匹配或显式条件，让OppTF仅在无法通过直接构造器生成实例的场景下生效。比如给OppTF添加额外参数，确保x对应的Opp x无法直接匹配Falses的构造器，但这种方法需要修改类型定义，复杂度较高，不如优先级调整直接。

关于自动识别等价性的说明 #

Agda的实例搜索是基于语法匹配的，不会自动归一化候选解并检查语义等价性——即使你已经用uniq证明了两个候选等价，Agda也不会主动利用这个证明来合并候选。因此，目标1和目标2目前无法直接实现，只能通过调整实例搜索的行为（如优先级）来避免冲突。

内容的提问来源于stack exchange，提问作者otah007