Определение рекурсивной функции над типом продукта
Я пытаюсь формализовать каждое целое число как класс эквивалентности пар натуральных чисел, где первый компонент является положительной частью, а второй компонент — отрицательной частью.
Definition integer : Type := prod nat nat.
Я хочу определить функцию нормализации, в которой положительные и отрицательные значения максимально сокращаются.
Fixpoint normalize (i : integer) : integer :=
let (a, b) := i in
match a with
| 0 => (0, b)
| S a' => match b with
| 0 => (S a', 0)
| S b' => normalize (a', b')
end
end.
Однако Кок говорит:
Error: Recursive definition of normalize is ill-formed. In environment normalize : integer -> integer i : integer a : nat b : nat a' : nat b' : nat Recursive call to normalize has principal argument equal to "(a', b')" instead of a subterm of "i".
Я думаю, что это может быть связано с обоснованной рекурсией?
Кажется Program Fixpoint normalize (i: int) { measure (fst i) } : integer может сработать. См. пример здесь: cs.cornell.edu/courses/cs6115/2017fa/notes/lecture7.html (с measure (length xs))
Ответы 4
Рекурсивные вызовы должны выполняться на «подтермине» исходного аргумента. Подтермин для термина в индуктивном типе — это, по сути, термин того же типа, который использовался для создания исходного термина. Например, часть натурального числа, такого как S a', равна a'.
К сожалению для вашего определения (как написано), пара i: prod nat nat не имеет подтерминов в этом смысле. Это потому, что prod не является рекурсивным типом. Его конструктор pair: A -> B -> prod A B не принимает ничего типа prod A B в качестве аргумента.
Чтобы исправить это, я бы предложил сначала определить вашу функцию для двух отдельных натуральных чисел.
Fixpoint normalize_helper (a b : nat) : integer :=
match a with
| 0 => (0, b)
| S a' => match b with
| 0 => (S a', 0)
| S b' => normalize a' b'
end
end.
Тогда normalize можно легко определить через normalize_helper.
Кстати, вы можете сопоставить две вещи одновременно с помощью match a, b with 0, _ => [...] | _, 0 => [...] | S a', S b' => [...] end. Подчеркивание _ просто означает, что нам все равно, что находится в этом пространстве.
Я хотел предложить именно это. Хотя Function или Program Fixpoint действительно работают, в данном случае это лишние хлопоты (и об этом труднее рассуждать).
Теперь Program Fixpoint стало настолько хорошо, что вы можете определить normalize так:
Require Import Program.
Definition integer :Type := (nat*nat).
Program Fixpoint normalize (i:integer) {measure (max (fst i) (snd i))} :=
match i with
| (S i1, S i2) => normalize (i1, i2)
| (_, _) => i
end.
Он способен справиться со всеми обязательствами по доказыванию самостоятельно!
Чтобы использовать его и рассуждать об этом, вы, вероятно, захотите определить некоторые леммы перезаписи.
Lemma normalize_0_l i: normalize (0, i) = (0, i).
Proof. reflexivity. Qed.
Lemma normalize_0_r i: normalize (i, 0) = (i, 0).
Proof. destruct i; reflexivity. Qed.
Lemma normalize_inj i j: normalize (S i, S j) = normalize (i, j).
unfold normalize at 1; rewrite fix_sub_eq; simpl; fold (normalize (i, j)).
- reflexivity.
- now intros [[|x] [|y]] f g H.
Qed.
Я получил технику unfold... rewrite ... simpl... fold от здесь!
В дополнение к ответу @larsr: плагин Уравнения предлагает некоторые приятные функции, такие как автоматическое создание лемм упрощения, аналогичных normalize_0_l, и т. д. для примера ниже у нас есть normalize_equation_1, normalize_equation_2 и т. д.
Более того, как и плагин Function, Equations предоставляет схемы функциональной индукции, которые делают доказательства свойств функций весьма элегантными.
From Equations Require Import Equations.
Definition integer : Type := prod nat nat.
Equations normalize (i : integer) : integer by wf (fst i) :=
normalize (0, b) := (0, b);
normalize (S a', 0) := (S a', 0);
normalize (S a', S b') := normalize (a', b')
.
(* see Coq's response for the list of auto generated lemmas *)
Докажем некоторые свойства normalize, используя функциональную индукцию. Уравнения предоставляют некоторые тактики, которые облегчают их использование. Я буду использовать funelim в этом случае.
From Coq Require Import Arith.
Lemma normalize_sub_lt a b :
a < b -> normalize (a, b) = (0, b - a).
Proof.
funelim (normalize (a, b)); simpl in *.
- now rewrite Nat.sub_0_r.
- now intros []%Nat.nlt_0_r.
- intros a_lt_b%Nat.succ_lt_mono; auto.
Qed.
Вторую часть спецификации normalize можно доказать таким же образом.
Lemma normalize_sub_gte a b :
b <= a -> normalize (a, b) = (a - b, 0).
Хотя полезно научиться писать рекурсивные функции такого типа, в данном конкретном случае я думаю, что было бы лучше избегать рекурсии и использовать стандартные определения:
Require Import Coq.Arith.Arith.
Definition integer : Type := (nat * nat).
Definition normalize (i : integer) : integer :=
if snd i <=? fst i then (fst i - snd i, 0)
else (0, snd i - fst i).
Это путь дзен :) Полностью согласен.
Кок не может доказать, что функция сходится, так как
(a, b)не является подчленом(S a, S b). Я бы создал вспомогательную функцию, которая принимает два аргумента (aиb). Таким образом,aявляется частьюS a, и функция в конечном итоге сойдется. Возможно, вы каким-то образом сможете заставить coq понять, что ваша исходная функция сходится, но я недостаточно знаю coq, чтобы сказать, возможно ли это. Вы можете попробовать{measure (fst i)}, но я не могу проверить это прямо сейчас.