Comment lire la syntaxe de l'insertion de l'arbre de Braun?

Question

Dans la section sur l'insertion dans les arbres Braun du Verified Programming in Agda book (page 118), l'auteur explique ce que le code est censé faire, mais en laissant de côté ce qu'il fait, une ommision singulière dans le livre n'est pas encore expliquer la syntaxe étrange dans la correspondance de modèle de fonction pour la démonstration de théorème.

Je comprends que le with pattern peut encore être déstructuré en utilisant | et je peux comprendre que lors de l'utilisation rewrite, | peut également être utilisé pour séparer les différents remaniements, mais cela rend confus. Pour autant que je sache, réécrire n'est définitivement pas une fonction. Et puis vient ce qui suit:

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))) 

Je suis vraiment confus quant à la façon dont rewrite +comm n m with p | if a <A a' then (a , a') else (a' , a) doit être analysé mentalement. Et comment lit-on | inj₁ p | (a1 , a2) rewrite p? Aussi, tout en testant les exemples précédents, j'ai découvert que pour une raison quelconque, l'ordre des réécritures n'a pas d'importance. Pourquoi donc?

Answer 1

Après avoir réfléchi pendant un peu, je me suis aperçu que si ...

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

je mets les expressions comme ça alors il est visuellement sens. Dans le second cas de bt_insert, la réécriture vient avant l'instruction if et dans le troisième cas, elle vient après la déstructuration du motif if.

Eh bien, cela laisse penser à ce que fait le reste de la fonction.

Answer 2

Si vous ignorez les preuves pour une seconde, cette fonction peut être simplifiée comme

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) 

Alors (a1, a2) est juste (min a a', max a a') dire (a, a') triés.

Tout autre code est là pour maintenir les preuves des invariants:

• Nous rewrite +comm n m pour que nous puissions retourner un braun-tree (2 + (m + n)) même si le type de retour nécessite un braun-tree (2 + (n + m)).

• p est utilisé pour prouver que l'arbre résultant est encore équilibré: p prouve que n ≡ m ∨ n ≡ suc m, il est donc soit inj₁ (p : n ≡ m) ou inj₂ (p : n ≡ suc m). Nous utilisons la preuve de l'une ou l'autre propriété pour calculer la preuve de suc m ≡ n ∨ suc m ≡ suc n (rappelez-vous que nous avons retourné n et m via la preuve de la commutativité).