coq

"Cannot guess decreasing argument of fix" error when defining a Fixpoint for extracting the first half of a list

I'm trying to define a Fixpoint function for list X to get its first half of a sub-list, if it's an odd number of elements, then the middle element doesn't count in.

Here's what I've tried:

Fixpoint half {X : Type} (l : list X) : list X :=
  match l with
  | [] => []
  | h :: t => match (rev t) with
              | [] => []
              | p :: b => [h] ++ (half (rev b))
              end
  end.

Yet it gives this error:

Cannot guess decreasing argument of fix.

What am I missing here?

Solution

  • You can only make a recursive call if one of your arguments is a "well-founded" inductive data type. Coq must be able to verify that, and one way is if it can see that the recursive argument is one small part of the original argument.

    You can't just apply a function on it, as it may make the argument "larger", and then one cannot as easily prove that recursion will terminate.

    In your case, Coq can't see that rev b is not for instance returning a longer list. In this case, we can pick something else that we know is decreasing monotonically and use that to show that recursion terminates. Like the length of the input argument. But then we have to do some work to show that to Coq.

    If you want to use the more flexible way to specify recursion, import the Program Module, and use Program Fixpoint instead of just Fixpoint to define your function. And add an argument in {} that specifies a measure that is monotonically decreasing.

    For example, we can use {measure (length l)}, to specify that the length of argument l is decreasing in recursive calls.

    Then define the function and use Next Obligation. to get the remaining proof obligations.

    Require Import List. Import ListNotations.
Require Import Program.

(* add Program  and {measure ...} *)

Program Fixpoint half {X : Type} (l : list X) {measure (length l)} : list X :=
  match l with
  | [] => []
  | h :: t => match (rev t) with
              | [] => []
              | p :: b => [h] ++ (half (rev b))
              end
  end
  .
  
Next Obligation.
(* Here we need to prove that the length of 
   the argument to the recursive call is smaller than 
   that of the calling function's argument: 

  Heq_anonymous : p :: b = rev t 
  --------
  length (rev b) < length (h :: t) 
*)

(*  We need to find some lemma that shows that length (rev x) = length x
Search (length (rev _)).      (* found rev_length *)
rewrite (rev_length b).
simpl.
rewrite <- (rev_length t).
rewrite <- Heq_anonymous.
simpl.
auto.
Qed.