Как прочитать синтаксис для вставки дерева Брауна?

Question

В разделе о вставке в деревья Брауна книги " Проверенное программирование в Агде" (стр. 118) автор дает некоторое объяснение того, что должен делать код, но оставляя в стороне то, что он делает, в качестве основного упущения в книге. не объясняет странный синтаксис в сопоставлении с образцом функции для доказательства теорем.

Я понимаю, что шаблон с может быть дополнительно деструктурирован с помощью | и я могу понять, что при использовании 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

Если вы игнорируете доказательства в течение секунды, эта функция может быть упрощена как

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 через доказательство коммутативности).

Answer 2

Поразмыслив немного, я понял, что если...

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

Я ставлю такие выражения, тогда это имеет смысл визуально. Во втором случае bt_insert перезапись предшествует оператору if, а в третьем - после деструктуризации шаблона if.

Что ж, остается понять, что делает остальная часть функции.