Я не могу увидеть все определения из-за некоторого юникода - многие введенные вами символы отображаются как квадраты. Базовая c идея WellFounded не является доказательством того, что некоторый тип данных становится меньше. Основная идея c состоит в том, что Agda может видеть, что Acc _<_ x, созданный функцией доступа, заключенной в Acc _<_ y, становится меньше.
В вашем случае кажется, что preSmaller - это такой _<_. Трудно судить, так ли это, потому что много текста отсутствует. Затем вам нужно будет создать функцию, которая может построить Acc preSmaller y для любых двух заданных x y : UniNbh.
В отредактированном вопросе все еще отсутствуют некоторые определения (например, что такое post nil . Но я понимаю, что происходит.
Ваше определение preSmaller похоже на следующее определение _<_ для Nat:
data _<_ : Nat -> Nat -> Set where
z< : {n : Nat} -> zero < (succ n)
s<s : {m n : Nat} -> m < n -> (succ m) < (succ n)
Обратите внимание, что это отличается от стандартного определения, потому что и m, и n становятся больше. Это влияет на построение доказательства WellFounded -ности.
-- may just as well import, but let me be self-contained:
data Acc {A : Set} (_<_ : A -> A -> Set) (x : A) : Set where
acc : ((y : A) -> y < x -> Acc _<_ y) -> Acc _<_ x
Well-founded : (A : Set) -> (R : A -> A -> Set) -> Set
Well-founded A _<_ = (x : A) -> Acc _<_ x
{-# BUILTIN EQUALITY _==_ #-} -- rewrite rule needs this, if I am not using
-- Unicode version of it from Prelude
<-Well-founded : Well-founded Nat _<_
<-Well-founded zero = acc \_ ()
<-Well-founded (succ x) = acc aux where
aux : (y : Nat) -> y < (succ x) -> Acc _<_ y
aux zero _ = <-Well-founded zero
aux (succ y) (s<s y<x) with <-Well-founded x | is-eq? (succ y) x
... | acc f | no sy!=x = f (succ y) (neq y<x sy!=x)
... | wf-x | yes sy==x rewrite sy==x = wf-x
Вспомогательные функции:
data False : Set where
false-elim : {A : Set} -> False -> A
false-elim ()
data Dec (A : Set) : Set where
yes : A -> Dec A
no : (A -> False) -> Dec A
_==?_ : {A : Set} -> A -> A -> Set
_==?_ x y = Dec (x == y)
s== : {m n : Nat} -> (succ m) == (succ n) -> m == n
s== refl = refl
is-eq? : (m n : Nat) -> m ==? n
is-eq? zero zero = yes refl
is-eq? (succ m) zero = no \()
is-eq? zero (succ n) = no \()
is-eq? (succ m) (succ n) with is-eq? m n
... | no f = no \sm=sn -> f (s== sm=sn)
... | yes m=n = yes (cong succ m=n)
-- if m < n and m+1 /= n, then m+1 < n
neq : {m n : Nat} -> m < n -> ((succ m) == n -> False) -> (succ m) < n
neq {_} {zero} ()
neq {zero} {succ zero} z< f = false-elim (f refl)
neq {zero} {succ (succ n)} z< f = s<s z<
neq {succ m} {succ n} (s<s m<n) f = s<s (neq m<n \m=n -> f (cong succ m=n))
Важные вещи, которые нужно убрать:
Стандартное определение _<_ позволяет построить более простое доказательство WellFounded -ности, потому что можно уменьшать один из аргументов за раз. другое определение _<_ требует сокращения обоих, и это кажется проблемой. Тем не менее, с помощью вспомогательной функции neq можно построить рекурсию, в которой только один и тот же аргумент становится меньше.
Реш. способность _==_ для Nat позволяет мне построить такую рекурсию. Agda может видеть, что рекурсивный вызов <-WellFounded предназначен для структурно меньшего x, поэтому он завершается. Затем результат этого используется по-разному в зависимости от результата проверки равенства. Ветвь, использующая neq, вычисляет необходимое Acc с учетом функции, которую <-WellFounded обнаружил для меньшего x: функция завершается, потому что Agda разрешила создание такой функции. Другая ветвь, где x == (succ y), использует значение как есть, потому что rewrite убеждает Agda в правильности его типа.
Обоснованность затем может использоваться для доказательства функции завершается путем создания экземпляра <-WellFounded:
_-|-_ : Bin -> Bin -> Bin
x -|- y with max-len x y
... | n , (x<n , y<n) = Sigma.fst (a (<-Well-founded n) b (x , x<n) (y , y<n)) where
a : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ n)
a+O : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))
a+I : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))
a+O f c m n with a f c m n
... | r , r<n = r O , s<s r<n
a+I f c m n with a f c m n
... | r , r<n = r I , s<s r<n
a {zero} _ _ (_ , ())
a {succ sz} (acc f) cc mm nn with cc | mm | nn
... | b | m O , s<s m< | n O , s<s n< = a+O (f sz n<n1) b (m , m<) (n , n<)
... | b | m O , s<s m< | n I , s<s n< = a+I (f sz n<n1) b (m , m<) (n , n<)
....-- not including the whole thing here - it is too long.
Я не включаю всю конструкцию сложения двух двоичных чисел (также неэффективную - просто упражнение на доказательство обоснованности). Здесь важно отметить, как запускается рекурсия и как она повторно используется для создания новых экземпляров Acc для сопоставления типов - здесь S-Bin представляет двоичное число длиной не более n, а Agda убежден, что Acc _<_ n становится меньше, хотя не может доказать, что S-Bin n становится меньше.