Agda 递归证明

Question

我在 Agda 中创建了一个递归数据类型“Positive”。我使用这种数据类型来索引一些树。 在这些树上，我试图证明对某些索引 q 的设置操作不会影响另一个索引 p 的获取操作（结果）。

gso : {A : Set} -> ∀ (i j : Positive) (t : Tree A) (v : A) → ((i ≡ j) → ⊥) → get i (set j v t) ≡ get i t
gso (xI p) (xI p) t v = ? 
gso (xO p) (xO p) t v = ?
gso p q t v = ? -- this works fine 

我尝试将树的不同情况分成这样的

gso (xI p) (xI q) (Nodes (node001 t)) v neq = gso p q (Nodes t) v neq

但这里我收到错误：

p != (xI p) of type Positive
when checking that the expression neq has type p ≡ q → ⊥

或者如果我从调用证明中删除 neq：

(p ≡ q → ⊥) → get p (set q v (Nodes t)) ≡ get p (Nodes t) !=<
get (xI p) (set (xI q) v (Nodes (node001 t))) ≡
get (xI p) (Nodes (node001 t))
when checking that the expression gso p q (Nodes t) v has type
get (xI p) (set (xI q) v (Nodes (node001 t))) ≡
get (xI p) (Nodes (node001 t))

**我现在的问题是为什么 Agda 不理解这一步，我怎样才能让它对 Agda 更明显？或者我对使用证明的理解有什么问题 **

感谢您提供的任何帮助。

我尝试创建一个证明，证明 与添加的构造函数/步骤保持相同。但我在这里遇到了同样的错误。

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_)
open Eq.≡-Reasoning


data Positive : Set where 
    xH : Positive
    xI : Positive -> Positive
    xO : Positive -> Positive

proof : ∀ (p q : Positive) → (p ≡ q) → ((xI p) ≡ (xI q))
proof xH xH = λ _ → refl
proof (xI p) xH = λ ()
proof (xO p) xH = λ ()  
proof xH (xI q) = λ ()
proof (xI p) (xI q) = proof p q -- This is where i run into the error again   
proof (xO p) (xI q) = λ ()
proof xH (xO q) = λ () 
proof (xI p) (xO q) = λ ()
proof (xO p) (xO q) = ?

这也是一个最小的示例，可以执行它来解决我的问题。

Answer 1

我通过用以下内容替换证明的定义来解决这个问题：

gso : {A : Set} → ∀ (i j : Positive) (t : Tree A) (v : A) → (i ≠ j) → (get i (set j v t) ≡ get i t)

其中“≠”定义为

  data _≠_ : Positive → Positive → Set where 
    i≠o : ∀ {p q : Positive} → (xI p) ≠ (xO q)
    o≠i : ∀ {p q : Positive} → (xO p) ≠ (xI q)
    i≠i : ∀ {p q : Positive} → p ≠ q → (xI p) ≠ (xI q)
    o≠o : ∀ {p q : Positive} → p ≠ q → (xO p) ≠ (xO q)

证明可以写成：

  gso (xI p) (xI q) Empty v (i≠i x) = gso p q Empty v x