Определение рекурсивной функции по типу продукта - PullRequest
Новая
       41

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

5 голосов
/ 05 июля 2019

Я пытаюсь формализовать каждое целое число как класс эквивалентности пар натуральных чисел, где первый компонент является положительной частью, а второй компонент является отрицательной частью.

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.

Однако Кок говорит:

Ошибка: Рекурсивное определение нормализуется неправильно. В среде normalize: целое число -> целое число я: целое число a: nat б: нат a ': nat б ': нат Рекурсивный вызов нормализации имеет главный аргумент равно "(a ', b')" вместо подтермы "i".

Думаю, это может быть связано с обоснованной рекурсией?

Ответы [ 4 ]

6 голосов
/ 05 июля 2019

Теперь 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 из здесь !

6 голосов
/ 05 июля 2019

В дополнение к ответу @ 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).
5 голосов
/ 05 июля 2019

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

3 голосов
/ 05 июля 2019

Хотя полезно научиться писать этот тип рекурсивной функции, в данном конкретном случае я думаю, что было бы лучше избежать рекурсии и использовать стандартные определения: 

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).
...