Recursion and Pattern matching in Coq

Question

I am learning Coq and need to know why the following code does not work in Coq? I am coming from a Haskell background and it is alright there.

Require Import List.
Require Import Bool.
Require Import Nat.

Fixpoint sorted l :=
    match l with
    | nil => true
    | _ :: nil => true
    | e1 :: e2 :: tl => andb (e1 <=? e2) (sorted (e2 :: tl))
    end.

Error is:

Recursive definition of sorted is ill-formed.
In environment
sorted : list nat -> bool
l : list nat
e1 : nat
l0 : list nat
e2 : nat
tl : list nat
Recursive call to sorted has principal argument equal to
"e2 :: tl" instead of one of the following variables: 
"l0" "tl".
Recursive definition is:
"fun l : list nat =>
 match l with
 | nil => true
 | e1 :: nil => true
 | e1 :: e2 :: tl => (e1 <=? e2) && sorted (e2 :: tl)
 end".

I had to rewrite as:

Definition initially_sorted l := 
    match l with
    | nil => true
    | _ :: nil => true
    | e1 :: e2 :: _ => ifb (e1 <=? e2) true false
    end.

Fixpoint sorted l :=
    match l with
    | nil => true
    | _ :: nil => true
    | e1 :: tl => andb (initially_sorted l) (sorted tl)
    end.

Answer 1

The recursive calls have to be on parts of the term passed as argument - you can't add anything. That is the "e2::" is illegal.

But there is an easy way around it: you can give a separate name to the tail part:

Require Import List.
Require Import Bool.
Require Import Nat.

Fixpoint sorted l :=
    match l with
    | nil => true
    | _ :: nil => true
    | e1 :: ((e2 :: _) as t) => andb (e1 <=? e2) (sorted t)
    end.