Упорядоченная рекурсия в Coq

Question

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

Мой код:

Inductive N : Set := 
    | O : N 
    | S : N -> N. 

Inductive Bool : Set := 
    | True : Bool 
    | False : Bool. 

Fixpoint sum (m :N) (n : N) : N := 
match m with 
    | O => n 
    | S x => S (sum x n) 
end. 

Notation "m + n" := (sum m n) (at level 50, left associativity). 

Fixpoint mult (m :N) (n : N) : N := 
match m with 
    | O => O 
    | S x => n + (mult x n) 
end. 

Notation "m * n" := (mult m n) (at level 40, left associativity). 

Fixpoint pred (m : N) : N := 
match m with 
    | O => S O 
    | S x => x 
end. 

Fixpoint resta (m:N) (n:N) : N := 
match n with 
    | O => m 
    | S x => pred (resta m x) 
end. 
Notation "m - x" := (resta m x) (at level 50, left associativity). 

Fixpoint leq_nat (m : N) (n : N) : Bool := 
match m with 
    | O => True 
    | S x => match n with 
    | O => False 
    | S y => leq_nat x y 
    end 
end. 

Notation "m <= n" := (leq_nat m n) (at level 70). 

Fixpoint div (m : N) (n : N) : N := 
match n with 
    | O => O 
    | S x => match m <= n with 
    | False => O 
    | True => pred (div (m-n) n) 
    end 
end. 

Как вы можете видеть, Coq не нравится моя функция DIV, он говорит

Error: Cannot guess decreasing argument of fix .

Как я могу поставить в Coq терминации доказательство для этой функции? Я могу доказать, что если n> 0^n < = m -> (m-n) < m.

Answer 1

Простейшая стратегия в данном случае, вероятно, использовать расширение Program вместе с measure. Затем вам нужно будет предоставить доказательство того, что аргументы, используемые в рекурсивном вызове, меньше, чем верхний уровень в соответствии с мерой.

Require Coq.Program.Tactics. 
Require Coq.Program.Wf. 

Fixpoint toNat (m : N) : nat := 
match m with O => 0 | S n => 1 + (toNat n) end. 

Program Fixpoint div (m : N) (n : N) {measure (toNat m)}: N := 
match n with 
    | O => O 
    | S x => match m <= n with 
    | False => O 
    | True => pred (div (m-n) n) 
    end 
end. 
Next Obligation. 
(* your proof here *) 

Answer 2

Хотя ответ Gallais, безусловно, путь в общем, я должен отметить, что мы можем определить деление на натуральные числа в Coq как простой фиксированной точки. Здесь я использую определение nat в стандартной библиотеке для простоты.

Fixpoint minus (n m : nat) {struct n} : nat := 
    match n, m with 
    | S n', S m' => minus n' m' 
    | _, _ => n 
    end. 

Definition leq (n m : nat) : bool := 
    match minus n m with 
    | O => true 
    | _ => false 
    end. 

Fixpoint div (n m : nat) {struct n} : nat := 
    match m with 
    | O => O 
    | S m' => 
    if leq (S m') n then 
     match n with 
     | O => O (* Impossible *) 
     | S n' => S (div (minus n' m') (S m')) 
     end 
    else O 
    end. 

Compute div 6 3. 
Compute div 7 3. 
Compute div 9 3. 

Определение minus, по существу, один из стандартной библиотеки. Обратите внимание, что во второй ветви этого определения мы возвращаем n. Благодаря этому трюку, проверка завершения Coq может обнаружить, что minus n' m' структурно меньше, чем S n', что позволяет нам выполнять рекурсивный вызов до div.

На самом деле есть еще более простой способ сделать это, хотя немного сложнее понять: вы можете проверить, меньше ли делитель и выполнить рекурсивный вызов за один шаг.

(* Divide n by m + 1 *) 
Fixpoint div'_aux n m {struct n} := 
    match minus n m with 
    | O => O 
    | S n' => S (div'_aux n' m) 
    end. 

Definition div' n m := 
    match m with 
    | O => O (* Arbitrary *) 
    | S m' => div'_aux n m' 
    end. 

Compute div' 6 3. 
Compute div' 7 3. 
Compute div' 9 3. 

Еще раз, из-за формы функции minus, прекращение проверки Coq в знает, что n' во второй ветви div'_aux является действительным аргументом рекурсивного вызова. Также обратите внимание, что div'_aux делится на m + 1.

Конечно, все это зависит от умного трюка, который требует понимания проверки завершения в деталях. В общем, вам нужно прибегнуть к обоснованной рекурсии, как показала галлия.