比较树的相互递归函数

Question

我正在尝试在类似树的类型上编写比较函数。

它有一个应该是字符串的值，但为了简单起见，我暂时将它设为 nat。它还有一个哈希来帮助加快比较，稍后将被 Sint63 取代，但为了现在简单起见，我将其设为 nat。

Require Import Coq.Lists.List.
Import Coq.Lists.List.ListNotations.

Inductive Info: Type :=
  mkInfo :
    forall
    (value: nat)
    (children: list Info)
    (hash: nat),
  Info.

比较函数必须尽快短路，为此它会在尝试子项之前尝试使用散列或值。使用散列可能会导致顺序可能不顺眼，但唯一重要的是该顺序具有确定性。

Fixpoint compare_info (x y: Info) {struct x} :=
  match x with
  | mkInfo xvalue xchildren xhash =>
    match y with
    | mkInfo yvalue ychildren yhash =>
      match Nat.compare xhash yhash with
      | Lt => Lt
      | Gt => Gt
      | Eq =>
        match Nat.compare xvalue yvalue with
        | Lt => Lt
        | Gt => Gt
        | Eq => compare_children xchildren ychildren
        end
      end
    end
  end
with compare_children (xs ys: list Info) {struct xs} :=
  match xs with
  | [] =>
    match ys with
    | [] => Eq
    | _ => Lt
    end
  | (x'::xs') =>
    match ys with
    | [] => Gt
    | (y'::ys') =>
      match compare_info x' y' with
      | Lt => Lt
      | Gt => Gt
      | Eq => compare_children xs' ys'
      end
    end
  end
.

问题是我收到以下错误：

Recursive definition of compare_children is ill-formed.
In environment
compare_info : Info -> Info -> comparison
compare_children : list Info -> list Info -> comparison
xs : list Info
ys : list Info
x' : Info
xs' : list Info
y' : Info
ys' : list Info
Recursive call to compare_info has principal argument equal to 
"x'" instead of "xs'".
Recursive definition is:
"fun xs ys : list Info =>
 match xs with
 | [] => match ys with
         | [] => Eq
         | _ :: _ => Lt
         end
 | x' :: xs' =>
     match ys with
     | [] => Gt
     | y' :: ys' =>
         match compare_info x' y' with
         | Eq => compare_children xs' ys'
         | Lt => Lt
         | Gt => Gt
         end
     end
 end".

我之前在单个递归函数中帮助 Coq 了解哪个元素是递归的，但我认为我以前没有用相互递归函数做过。

我不想使用 Program Fixpoint，因为我过去发现这使得证明函数的事情变得非常困难。

我想知道是否有另一种方法以 Coq 可接受的方式编写此函数？

感谢您的帮助

Answer 1

您使用的类型是Nested Inductive Type。您的代码是正确的，只有一个纯技术时刻：compare_children 的定义应定义为本地固定点，而不是相互固定点。

Fixpoint compare_info (x y: Info) {struct x} :=
  match x with
  | mkInfo xvalue xchildren xhash =>
    match y with
    | mkInfo yvalue ychildren yhash =>
      match Nat.compare xhash yhash with
      | Lt => Lt
      | Gt => Gt
      | Eq =>
        match Nat.compare xvalue yvalue with
        | Lt => Lt
        | Gt => Gt
        | Eq => ((fix compare_children (xs ys: list Info) {struct xs} :=
                   (match xs with
                    | [] =>
                      match ys with
                      | [] => Eq
                      | _ => Lt
                      end
                    | (x'::xs') =>
                      match ys with
                      | [] => Gt
                      | (y'::ys') =>
                        match compare_info x' y' with
                        | Lt => Lt
                        | Gt => Gt
                        | Eq => compare_children xs' ys'
                        end
                      end
                    end)) xchildren ychildren)
        end
      end
    end
  end.

有关详细信息，请参阅 Certified Programming with Dependent Types by Adam Chlipala. Needed Chapter 在线（搜索 Nested Inductive）。书中也有此类类型的归纳原理的例子。

比较树的相互递归函数

Mutually Recursive Function to Compare Trees

coq