Я играю с joinˡ⁺ из реализации дерева AVL стандартной библиотеки. Эта функция определяется шестью предложениями сопоставления с образцом. Когда я применяю функцию к аргументу, Agda уменьшает или не сокращает выражение моего приложения функции, в зависимости от того, какое из шести предложений соответствует моему аргументу. (Или мне так кажется.)
Вот код, который применяет функцию к аргументу, который соответствует первому предложению функции. Это левая часть равенства в воротах. Agda сокращает его до правой части, и я могу sh завершить доказательство refl. Так что этот работает, как ожидалось.
(Обратите внимание, что код использует версию 1.3 стандартной библиотеки. Похоже, что в более поздних версиях код дерева AVL был перемещен с Data.AVL на Data.Tree.AVL.)
module Repro2 where
open import Data.Nat using (ℕ ; suc)
open import Data.Nat.Properties using (<-strictTotalOrder)
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Data.AVL.Indexed <-strictTotalOrder
okay :
∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
≡
(0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)
okay k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl
Следующий пример нацелен на второе предложение определения функции. В отличие от вышеупомянутого, цель не уменьшается все это время, то есть joinˡ⁺ не go отходит.
not-okay : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
≡
(0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
not-okay k₄ k₂ t₁ t₃ t₅ = {!!}
Что мне не хватает?
Дополнение после ответа MrO
MrO прибил. Я знал, что если шаблон предложения соответствует подтермингу аргумента (или всему аргументу), то мне, очевидно, нужно передать соответствующий конструктор данных для этого подтермина, чтобы оценщик выбрал это предложение. Однако этого недостаточно. Как указал MrO, в некоторых случаях мне также необходимо передать конструкторы данных для подтермингов, которые другие предложения (т. Е. Не только предложение, которое я собираюсь использовать) соответствуют шаблону, даже если данное предложение не соответствует на них наплевать.
Чтобы изучить это (для меня: главное новое) понимание, я попробовал оставшиеся четыре предложения joinˡ⁺. Последнее предложение, пункт № 6, привело к еще одному выводу.
Здесь пункт № 3. Он работает почти так же, как not-okay.
clause₃ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
≡
(1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
-- This does not work:
-- clause₃ k₄ k₂ t₁ t₃ t₅ = {!!}
clause₃ k₄ k₂ t₁ (node k t₃ t₄ bal) t₅ = refl
Пункт 4 более сложен.
clause₄ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (1# , t₁) t₃ ∼0
≡
(1# , node k₂ t₁ t₃ ∼-)
-- This does not work:
-- clause₄ k₂ t₁ t₃ = {!!}
-- This still doesn't, because of t' (or so I thought):
-- clause₄ k₂ (node k t t′ b) t₃ = {!!}
-- Surprise! This still doesn't, because of b:
-- clause₄ k₂ (node k t (leaf l<u) b) t₃ = {!!}
-- clause₄ k₂ (node k t (node k′ t′′ t′′′ b') b) t₃ = {!!}
clause₄ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₄ k₂ (node k t (leaf l<u) ∼-) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼+) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼0) t₃ = refl
clause₄ k₂ (node k t (node k′ t′′ t′′′ b') ∼-) t₃ = refl
Пункт 5 аналогичен пункту 4.
clause₅ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
k₂ (1# , t₁) t₃ ∼+
≡
(0# , node k₂ t₁ t₃ ∼0)
clause₅ k₂ (node k t (leaf l<u) ∼0) t₃ = refl
clause₅ k₂ (node k t (leaf l<u) ∼-) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼+) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼0) t₃ = refl
clause₅ k₂ (node k t (node k′ t'′ t′′′ b′) ∼-) t₃ = refl
Пункт № 6 был для меня немного неожиданностью. Я думал, что мне нужно передавать конструкторы данных везде, где они требуются в любом из пунктов. Но это не то, что сказал MrO. И это показано в этом предложении:
clause₆ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (0# , t₁) t₃ b
≡
(0# , node k₂ t₁ t₃ b)
clause₆ k₂ t₁ t₃ b = refl
Проще, чем я думал: никаких дополнительных конструкторов данных не требуется. Зачем? Я пошел прочитать часть сопоставления с образцом в справочнике Agda:
https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case -trees
Я читал его раньше, но совершенно не смог применить то, что он говорит. Agda находит предложение для выбора с помощью дерева решений, дерева вариантов . Мне теперь кажется, что Agda нужны конструкторы данных до тех пор, пока она не достигла листа дерева вариантов, т.е. пока она не выяснила, какое предложение выбрать.
Для рассматриваемой функции, дерево вариантов, кажется, начинается с вопроса: 0# или 1#? По крайней мере, это объясняет пункт №6:
Если это 0#, то мы знаем, что это должен быть пункт №6, конструкторы данных больше не требуются. Пункт № 6 - единственное соответствие для 0#. Итак, мы находимся на листе, наш обход дерева вариантов завершен.
Если это 1#, то нам нужно выполнить большее сопоставление, т. Е. Перейти вниз по дереву вариантов к следующий уровень. Здесь нам нужен еще один конструктор данных. Таким образом, в целом нам нужен конструктор данных для каждого посещенного уровня дерева случаев.
По крайней мере, это моя текущая ментальная модель, которая, кажется, подтверждается наблюдениями, сделанными в отношении joinˡ⁺.
Пытаясь еще немного проверить эту ментальную модель, я пошел и модифицировал свою копию стандартной библиотеки, изменив порядок шести предложений в обратном порядке. Поскольку Agda строит дерево вариантов, просматривая предложения по порядку и переходя слева направо внутри каждого предложения, это должно дать нам гораздо лучшее дерево вариантов.
0# против 1# все равно будет первый уровень дерева решений, но за ним последует внешний баланс, а затем внутренний баланс. Нам не нужно было бы разбивать деревья на узлы, за исключением последнего (ранее первого) предложения, которое действительно соответствует этому.
И действительно, все складывается так, как ожидалось. Вот как выглядят доказательства с обратным порядком предложений в моей модифицированной стандартной библиотеке.
clause₁′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ b →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (0# , t₁) t₃ b
≡
(0# , node k₂ t₁ t₃ b)
clause₁′ k₂ t₁ t₃ b = refl
clause₂′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {suc h} {suc h}
k₂ (1# , t₁) t₃ ∼+
≡
(0# , node k₂ t₁ t₃ ∼0)
clause₂′ k₂ t₁ t₃ = refl
clause₃′ : ∀ {l u h} k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ →
joinˡ⁺ {l = l} {u} {h} {h} {h}
k₂ (1# , t₁) t₃ ∼0
≡
(1# , node k₂ t₁ t₃ ∼-)
clause₃′ k₂ t₁ t₃ = refl
clause₄′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-
≡
(1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
clause₄′ k₄ k₂ t₁ t₃ t₅ = refl
not-okay′ : ∀ {l u h} k₄ k₂ (t₁ : Tree (const ℕ) _ _ _) t₃ t₅ →
joinˡ⁺ {l = l} {u} {suc h} {h} {suc h}
k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-
≡
(0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
not-okay′ k₄ k₂ t₁ t₃ t₅ = refl
okay′ :
∀ {l u h} k₆ k₂ (t₁ : Tree (const ℕ) _ _ _) k₄ t₃ t₅ t₇ b →
joinˡ⁺ {l = l} {u} {suc (suc h)} {suc h} {suc (suc h)}
k₆ (1# , node k₂ t₁ (node {hˡ = h} {suc h} {suc h} k₄ t₃ t₅ b) ∼+) t₇ ∼-
≡
(0# , node k₄ (node k₂ t₁ t₃ (max∼ b)) (node k₆ t₅ t₇ (∼max b)) ∼0)
okay′ k₆ k₂ t₁ k₄ t₃ t₅ t₇ b = refl