如何读取Braun树插入的语法？

Question

在关于插入到博朗树（第118页）的章节中，作者对代码应该做什么做了一些解释，但是将其留在一边，本书中的一个明显ommision并不是解释函数模式匹配中用于定理证明的奇怪语法。

据我所知，with pattern可以通过使用|进一步解构和我可以理解，使用时rewrite，|也可以用来分离不同的重写，但是这使得它混乱。

据我所知，重写绝对不是一个函数。然后出现以下内容：

bt-insert a (bt-node{n}{m} a' l r p) 
    rewrite +comm n m with p | if a <A a' then (a , a') else (a' , a) 
bt-insert a (bt-node{n}{m} a' l r _) | inj₁ p | (a1 , a2) 
    rewrite p = (bt-node a1 (bt-insert a2 r) l (inj₂ refl)) 
bt-insert a (bt-node{n}{m} a' l r _) | inj₂ p | (a1 , a2) = 
    (bt-node a1 (bt-insert a2 r) l (inj₁ (sym p))) 

我真的很困惑，应该如何精神分析rewrite +comm n m with p | if a <A a' then (a , a') else (a' , a)。一个人如何阅读| inj₁ p | (a1 , a2) rewrite p？另外，在测试前面的例子时，我发现由于某种原因，重写的顺序并不重要。这是为什么？

Answer 1

琢磨它一点后，我意识到，如果......

   p | if a <A a' then (a , a') else (a' , a) 
     inj₁ p | (a1 , a2) 

我把这样的表达式是的话很有道理视觉。在bt_insert的第二种情况下，重写在if语句之前，在第三种情况下，在if模式的解构之后。

那么，这留下了弄清楚该功能的其余部分正在做什么。

Answer 2

如果你忽略了秒的证明，这个功能可以简化为

bt-insert : ∀ {n: ℕ} → A → braun-tree n → braun-tree (suc n) 
bt-insert a (bt-node {n} {m} a' l r _) = bt-node a1 (bt-insert a2 r) l _ 
    where 
    (a1, a2) = if a <A a' then (a , a') else (a' , a) 

所以(a1, a2)只是(min a a', max a a')即(a, a')排序。

所有其他的代码是有保持不变的证明：

• 我们rewrite +comm n m这样我们就可以返回braun-tree (2 + (m + n))即使返回类型需要braun-tree (2 + (n + m))。

• p被用来证明结果树仍然是平衡的：p证明n ≡ m ∨ n ≡ suc m，所以它要么inj₁ (p : n ≡ m)或inj₂ (p : n ≡ suc m)。我们使用任一性质的证明来计算suc m ≡ n ∨ suc m ≡ suc n的证明（记得我们通过交换证明翻转了n和m）。