Well founded recursion in Coq

问题:

I am trying to write a function for computing natural division in Coq and I am having some trouble defining it since it is not structural recursion.

My code is:

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.

As you can see, Coq does not like my function div, it says

Error: Cannot guess decreasing argument of fix.

How can I supply in Coq a termination proof for this function? I can prove that if n>O ^ n<=m -> (m-n) < m.

回答1:

The simplest strategy in this case is probably to use the Program extension together with a measure. You will then have to provide a proof that the arguments used in the recursive call are smaller than the top level ones according to the 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 *)

回答2:

Although gallais's answer is definitely the way to go in general, I should point out that we can define division on the natural numbers in Coq as a simple fixpoint. Here, I'm using the definition of nat in the standard library for simplicity.

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.

The definition of minus is essentially the one from the standard library. Notice on the second branch of that definition we return n. Thanks to this trick, Coq's termination checker can detect that minus n' m' is structurally smaller than S n', which allows us to perform the recursive call to div.

There's actually an even simpler way of doing this, although a bit harder to understand: you can check whether the divisor is smaller and perform the recursive call in a single step.

(* 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.

Once again, because of the form of the minus function, Coq's termination checker knows that n' in the second branch of div'_aux is a valid argument to a recursive call. Notice also that div'_aux is dividing by m + 1.

Of course, this whole thing relies on a clever trick that requires understanding the termination checker in detail. In general, you have to resort to well-founded recursion, as gallais showed.