如何讀取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）。