Обратная функция на Агде
Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. И мы знаем такое число, но никому не скажем, что это 2. Обобщим это наблюдение, введя бинарное отношение принадлежности величины образу функции f как тип данных Агды
data Image_∋_ {X Y : Set}(f : X → Y) : Y → Set where
im : (x : X) → Image f ∋ f x
Наличие всего одного конструктора отражает тот факт, что единственный способ сконструировать элемент образа f - выбрать аргумент x и применить f к этому x. Например, рассматривая функции
square : ℕ → ℕ
square n = n * n
и
cube : ℕ → ℕ
cube n = n * n * n
легко заметить, что im 2 может выступить свидетельством того, что образ square содержит 4
lem-4-is-square : Image square ∋ 4
lem-4-is-square = im 2
или того, что образ cube содержит 8
lem-8-is-cube : Image cube ∋ 8
lem-8-is-cube = im 2
Перейдём теперь к построению обратной функции. Обратная к f функция может иметь в качестве области определения не все значения из Y, а только те, что принадлежат образу f. Чтобы Агда могла проконтролировать этот факт, мы должны, помимо самой функции и аргумента, передать ещё и соответствующий объект-свидетельство про этот аргумент
inv : {X Y : Set}(f : X → Y)(y : Y) → Image f ∋ y → X
inv f .(f x) (im x) = x
Теперь можно посчитать значение функции, обратной к квадрату в точке 4
my-value-is-2 : ℕ
my-value-is-2 = inv square 4 lem-4-is-square
и функции, обратной к кубу в точке 8
my-value-is-2-too : ℕ
my-value-is-2-too = inv cube 8 lem-8-is-cube
Если же мы попробуем написать
i-am-not-a-nat = inv square 5 {! !}
то Агда затребует от нас сконструировать для дырки объект ?0 : Image square ∋ 5, необитаемость которого очевидна.
Ремарка. Точечный образец в определении inv необходим для подсказки компилятору о том, что после связывания f в первом аргументе и x - в третьем единственное корректное значение второго аргумента это (f x).
data Image_∋_ {X Y : Set}(f : X → Y) : Y → Set where
im : (x : X) → Image f ∋ f x
Наличие всего одного конструктора отражает тот факт, что единственный способ сконструировать элемент образа f - выбрать аргумент x и применить f к этому x. Например, рассматривая функции
square : ℕ → ℕ
square n = n * n
и
cube : ℕ → ℕ
cube n = n * n * n
легко заметить, что im 2 может выступить свидетельством того, что образ square содержит 4
lem-4-is-square : Image square ∋ 4
lem-4-is-square = im 2
или того, что образ cube содержит 8
lem-8-is-cube : Image cube ∋ 8
lem-8-is-cube = im 2
Перейдём теперь к построению обратной функции. Обратная к f функция может иметь в качестве области определения не все значения из Y, а только те, что принадлежат образу f. Чтобы Агда могла проконтролировать этот факт, мы должны, помимо самой функции и аргумента, передать ещё и соответствующий объект-свидетельство про этот аргумент
inv : {X Y : Set}(f : X → Y)(y : Y) → Image f ∋ y → X
inv f .(f x) (im x) = x
Теперь можно посчитать значение функции, обратной к квадрату в точке 4
my-value-is-2 : ℕ
my-value-is-2 = inv square 4 lem-4-is-square
и функции, обратной к кубу в точке 8
my-value-is-2-too : ℕ
my-value-is-2-too = inv cube 8 lem-8-is-cube
Если же мы попробуем написать
i-am-not-a-nat = inv square 5 {! !}
то Агда затребует от нас сконструировать для дырки объект ?0 : Image square ∋ 5, необитаемость которого очевидна.
Ремарка. Точечный образец в определении inv необходим для подсказки компилятору о том, что после связывания f в первом аргументе и x - в третьем единственное корректное значение второго аргумента это (f x).