Как перейти от явного доказательства уменьшения размера к алгоритму уменьшения остановки?

Question

Предположим, у меня есть:

• A Linear : Set тип для линейных терминов λ-исчисления.

• A reduce-once : Term → Term функция, которая выполняетглобальное сокращение переопределений.

• A size : Linear → Nat отношение, которое считает количество конструкторов.

• Доказательство reduce-once-halts : (t : Linear) → size (reduce-once t) < size t.

То есть у меня есть доказательство того, что применение reduce-once всегда уменьшает размер термина. Исходя из этого, логически следует иметь возможность реализовать завершающую функцию reduce : (t : Linear) → Sigma t IsNormalized, которая сокращает срок до нормальной формы. Поскольку я считаю, что это обычная ситуация, мой вопрос: как это обычно оформляется в Агде? Как я могу убедить его, что функция, которая уменьшает размер своего аргумента, может быть применена рекурсивно и в конечном итоге остановится?

Answer 1

Вы можете использовать <-rec из модуля Data.Nat.Induction, чтобы сделать обоснованную индукцию более _<_. В этом случае одним из решений является введение в предикат «условия, размер которых строго меньше n, могут быть уменьшены»:

open import Data.Nat
open import Data.Nat.Induction
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

postulate
  Term : Set
  reduce-once : Term → Term
  size : Term → ℕ
  reduce-once-halts : (t : Term) → size (reduce-once t) < size t

reduce-aux : (n : ℕ) (t : Term) → size t < n → Term
reduce-aux = <-rec
  (λ n → (t : Term) → size t < n → Term)
  λ n h t size-t<n → h (size t) size-t<n (reduce-once t) (reduce-once-halts t)

reduce : Term → Term
reduce t = reduce-aux (1 + size t) t ≤-refl