有目的的遞歸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. 

正如你所看到的，勒柯克不喜歡我的函數div，它說

Error: Cannot guess decreasing argument of fix .

我如何能提供在勒柯克終止證明了這個功能呢？我可以證明，如果n> O^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的的答案肯定是一般要走的路，我要指出的是，我們可以上在勒柯克自然數師定義爲簡單的固定點。在這裏，爲了簡單起見，我在標準庫中使用了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函數的形式，勒柯克的終止檢查知道n'在div'_aux第二分支是一個遞歸調用一個有效的論據。另請注意，div'_aux除以m + 1。

當然，這整個事情依賴於一個聰明的把戲，需要詳細瞭解終止檢查器。一般來說，你必須求助於有根有據的遞歸，就像加拉萊所表明的那樣。