Мне трудно убедить Agda в том, что аргумент в рекурсивном вызове функции структурно меньше входящего аргумента.
Я определил пары, списки пар (представляющие конечные функции как «наборы» пар ввода / вывода) и объединения таких списков следующим образом:
data _x_ {l : Level} (A B : Set l) : Set l where
<_,_> : A -> B → A x B
data FinFun (A B : Set) : Set where
nil : FinFun A B
_::_ : A x B → FinFun A B → FinFun A B
_U_ : {A B : Set} -> FinFun A B -> FinFun A B -> FinFun A B
nil U f' = f'
(x :: xs) U f' = x :: (xs U f')
Я также определил «окрестности» и верхнюю грань двух таких окрестностей:
data UniNbh : Set where
bot : UniNbh
lam : FinFun UniNbh UniNbh -> UniNbh
_u_ : UniNbh -> UniNbh -> UniNbh
bot u bot = bot
bot u (lam f) = lam f
(lam f) u bot = lam f
(lam f) u (lam f') = lam (f U f')
Наконец, что наиболее важно для этого вопроса, я определил функцию, которая, учитывая список пар окрестностей, принимает верхнюю грань всех первых компонентов пар в списке:
pre : FinFun UniNbh UniNbh -> UniNbh
pre nil = bot
pre (< x , y > :: f) = x u pre f
Взаимно рекурсивная функция, которая вызывает у меня проблемы, по существу выглядит так:
f : UniNbh -> UniNbh -> UniNbh -> Result
-- Base cases here. When any argument is bot or lam nil, no
-- recursion is needed.
f (lam (a ∷ as)) (lam (b ∷ bs)) (lam (c ∷ cs)) =
f (lam (a ∷ as)) (pre (b ∷ bs)) (lam (c ∷ cs))
Кажется очевидным, что либо pre f меньше, чем lam f, либо один из базовых случаев завершит рекурсию, но Agda по понятным причинам не видит этого. Я пробовал довольно много разных идей, пытаясь решить эту проблему, но они не сработали. На данный момент я думаю, что единственный способ - использовать Induction.WellFounded из стандартной библиотеки, но я не могу понять, как это сделать.
Я безуспешно пытался показать, что следующий тип данных обоснован:
data preSmaller : UniNbh -> UniNbh -> Set where
pre-base : preSmaller (pre nil) (lam nil)
pre-step : ∀ (x y f f') ->
preSmaller (pre f) (lam f') ->
preSmaller (pre (< x , y > :: f')) (lam (< x , y > :: f'))
Я даже не уверен, что этот тип данных был бы полезен, даже если бы смог доказать, что он хорошо обоснован.
Оглядываясь вокруг, пытаясь найти информацию о том, как использовать Induction.WellFounded, я могу найти только очень простые примеры, показывающие, что ‹для натуральных чисел хорошо обосновано, и я не смог обобщить эти идеи на эту ситуацию.
Простите за длинный пост. Любая помощь будет принята с благодарностью!