Определение рекурсивной функции по типу продукта

Рекурсивные вызовы должны выполняться на «подтерме» исходного аргумента. Подтермин для термина индуктивного типа - это, по сути, термин того же типа, который использовался для создания исходного термина. Например, подтермин натурального числа, такого как 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.

Теперь 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: плагин Equations предлагает некоторые приятные функции, такие как автоматическое создание аналогичных лемм упрощения к 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).