Coq 中的递归和模式匹配

Question

我正在学习 Coq，想知道为什么以下代码在 Coq 中不起作用？我来自 Haskell 背景，那里没问题。

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.

错误是：

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".

我不得不重写为：

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

递归调用必须在作为参数传递的术语的一部分上——你不能添加任何东西。那就是“e2::”是非法的。

但是有一个简单的方法可以绕过它：你可以给尾巴部分一个单独的名字：

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.