如何在已知的情况下应用decidable？

Question

我正在尝试证明二进制排序树插入。我正在进行验证，环境是这样的：

  -- new rx : ℕ

  Goal: SortedTree (node leaf x (node (insertTree new rl) rx rr))
  Have: SortedTree (insertTree new (node rl rx rr) | new ≤? rx) 
  ————————————————————————————————————————————————————————————
  new≤rx : new ≤ rx

注意| new ≤? rx，它的意思是“我需要知道值才能进一步减少它”。

如何应用新的≤rx？

insertTree的定义如下：

  insertTree : (a : ℕ) →  (t : Tree ℕ) → Tree ℕ
  insertTree a (node l x r) with a ≤? x
  insertTree a (node l x r) | yes p = node (insertTree a l) x r
  insertTree a (node l x r) | no ¬p = node l x (insertTree a r)

我知道新≤的价值吗？rx (it's yes new≤rx)，实际上我现在被new ≤? x with了：

  ... | no  ¬n≤x with new ≤? rx
  ...        | yes new≤rx = {!proof⟦insertTree⟧ (node rl rx rr)  (sorted-rhs st) new !}
  ...        | no  p = {!!} 

那么，我如何告诉agda new ≤? rx的值是已知的，它应该与insertTree a (node l x r) | yes p = node (insertTree a l) x r一起使用呢

我试着使用重写

             where prf : (new ≤? rx ≡ yes new≤rx) → SortedTree (node (insertTree new rl) rx rr)
                   prf p1 rewrite p1 = {!proof⟦insertTree⟧ (node rl rx rr)  (sorted-rhs st) new !}

但即使我有p1 : new ≤? rx ≡ yes new≤rx，agda也忽略了它，说我有SortedTree (insertTree new (node rl rx rr) | new ≤? rx)

Answer 1

我设法通过检查+重写得到了它。

       proof⟦insertTree⟧ (node leaf x (node rl rx rr)) st new with new ≤? x 
       ... | yes p = st-node (empty new) (sorted-rhs st) p (st-cmp-rhs st)
       ... | no  ¬n≤x with new ≤? rx |  inspect (_≤?_ new) rx
       ...               | yes p | PropEq.[ eq ] = {!!}
              where prf : (new ≤? rx ≡ yes p) →  SortedTree (insertTree new (node rl rx rr)) → SortedTree (node (insertTree new rl) rx rr)
                    prf p0 p rewrite p0 = p

请注意，prf subproof接受SortedTree (insertTree new (node rl rx rr))类型的p并返回p本身，但由于重写，返回的类型被更改。