Coq 程序定点与方程作为获得归约引理的最佳方法？

Question

我试图证明如何计算两个字符串之间的编辑距离的特定实现是正确的并且产生相同的结果。我采用最自然的方式将编辑距离递归地定义为单个函数（见下文）。这导致 coq 抱怨它无法确定递减的参数。经过一番查找，似乎使用Program Fixpoint机制并提供测量函数是解决这个问题的一种方法。然而，这导致了下一个问题，即策略简单不再按预期工作。我发现这个 问题 有类似的问题，但我陷入困境，因为我不不明白 Fix_sub 函数在 coq 为我的编辑距离函数生成的代码中扮演的角色，该函数看起来比上一个问题中的简单示例更复杂。

问题：

1. 对于像编辑距离这样的函数，Equations 包是否比 Program Fixpoint（自动获取归约引理）更容易使用？上一个关于这方面的问题是 2016 年提出的，所以我很好奇这方面的最佳实践是否从那时起就发生了演变。
2. 我遇到了这个 coq 程序 涉及使用归纳定义的 prop 的 edit_distance而不是一个函数。也许这是我仍在试图理解 Curry-Howard Correspondence，但为什么 Coq 愿意接受 edit_distance 的归纳命题定义而没有终止/测量投诉，而不是函数驱动的方法？这是否意味着存在一个使用创造性定义的归纳类型的角度，该类型可以传递给 edit_distance，其中包含包装为一对的字符串和一个数字，并且 coq 上的过程更容易接受作为结构递归？

是否有更简单的方法使用程序修复点来获得减少？

Fixpoint min_helper (best :nat) (l : list nat) : nat :=
match l with
  | nil => best
  | h::t => if h<?best then min_helper h t else min_helper best t
end.


Program Fixpoint edit_distance (s1 s2 : string) {measure (length s1+ length s2)} : nat :=
match s1, s2 with 
    | EmptyString , EmptyString => O
    | String char rest , EmptyString => length s1
    | EmptyString , String char rest => length s2
    | String char1 rest1 , String char2 rest2  =>  
                let choices : list nat :=  S ( edit_distance rest1 s2) :: S (edit_distance s1 rest2) :: nil   in 
                if (Ascii.eqb char1 char2) 
                        then  min_helper (edit_distance rest1 rest2 ) choices
                        else min_helper (S (edit_distance rest1 rest2)) choices
end.
Next Obligation.
intros. simpl. rewrite <- plus_n_Sm.    apply Lt.le_lt_n_Sm. reflexivity. Qed.
Next Obligation.
simpl. rewrite <- plus_n_Sm.    apply Lt.le_lt_n_Sm. apply PeanoNat.Nat.le_succ_diag_r. Qed.
Next Obligation. 
simpl. rewrite <- plus_n_Sm.    apply Lt.le_lt_n_Sm. apply PeanoNat.Nat.le_succ_diag_r. Qed.

Theorem simpl_edit : forall (s1 s2: string), edit_distance s1 s2  = match s1, s2 with 
    | EmptyString , EmptyString => O
    | String char rest , EmptyString => length s1
    | EmptyString , String char rest => length s2
    | String char1 rest1 , String char2 rest2  =>  
                let choices : list nat :=  S ( edit_distance rest1 s2) :: S (edit_distance s1 rest2) :: nil   in 
                if (Ascii.eqb char1 char2) 
                        then  min_helper (edit_distance rest1 rest2 ) choices
                        else min_helper (S (edit_distance rest1 rest2)) choices
end.
Proof. intros.  induction s1.
  -  induction s2.
  -- reflexivity. 
  --  reflexivity. 
  -  induction s2. 
  --  reflexivity. 
  --  remember (a =? a0)%char as test. destruct test. 
  ---  (*Stuck??? Normally I would unfold edit_distance but the definition coq creates after unfold edit_distance ; unfold edit_distance_func is hard for me to reason about*)

Answer 1

您可以改为使用 Coq 附带的 Function 并为您生成一个归约引理（这实际上还会生成一个图形作为 Inducing R_edit_distance ，就像您的替代开发一样）提到，但这里它非常粗糙 - 这可能是因为我对简洁进行了编辑）

Require Import String.
Require Import List.
Require Import PeanoNat.
Import ListNotations.
Require Import FunInd.
Require Recdef.

Fixpoint min_helper (best : nat) (l : list nat) : nat :=
  match l with
  | [] => best
  | h :: t => if h <? best then min_helper h t else min_helper best t
  end.

Function edit_distance
  (ss : string * string) (* unfortunately, Function only supports one decreasing argument *)
  {measure (fun '(s1, s2) => String.length s1 + String.length s2) ss} : nat :=
  match ss with 
  | (String char1 rest1 as s1, String char2 rest2 as s2)  =>
    let choices := [S (edit_distance (rest1, s2)); S (edit_distance (s1, rest2))] in 
    if Ascii.eqb char1 char2
      then min_helper (edit_distance (rest1, rest2)) choices
      else min_helper (S (edit_distance (rest1, rest2))) choices
  | (EmptyString, s) | (s, EmptyString) => String.length s
  end.
all: intros; simpl; rewrite Nat.add_succ_r; repeat constructor.
Qed.

Check edit_distance_equation. (* : forall ss : string * string, edit_distance ss = ... *)
Print R_edit_distance. (* Inductive R_edit_distance : string * string -> nat -> Prop := ... *)

图归纳定义（无论是你引用的好定义还是这里生成的混乱定义）不需要的原因终止的保证是归纳类型的项必须已经是有限的。术语R_edit_distance ss n（表示edit_distance ss = n）应被视为edit_distance。尽管一般的递归函数可能会陷入无限计算，但相应的归纳类型排除了无限对数：如果 edit_distance ss 发散，则 R_edit_distance ss n 对于所有 n 来说都是无人居住的，所以不会发生爆炸。反过来，给定 ss，您无法实际计算，edit_distance ss 是什么或 { 中的术语n | R_edit_distance ss n}，直到您完成一些终止证明。 （例如，证明 forall ss, {n | R_edit_distance ss n} 是 edit_distance 的终止证明形式。）

使用结构递归的想法在某些辅助类型上是完全正确的（这是无论如何都可用的唯一递归形式；Program和Function都只是在其上构建），但它实际上与图归纳没有任何关系......

Fixpoint edit_distance
  (s1 s2 : string) (n : nat) (prf : n = String.length s1 + String.length s2)
  {struct n}
: nat := _.

与上述类似的东西应该可以工作，但它会很混乱。 （您可以递归图归纳的实例，而不是这里的nat，但是，这又会让构建图归纳的实例彻底失败。）

Answer 2

这种对两个参数的递归有一个常见的技巧，即编写两个嵌套函数，每个函数对两个参数之一进行递归。

这也可以从动态规划的角度来理解，通过遍历矩阵来计算编辑距离。更一般地，编辑距离函数 edit xs ys 可以被视为 nat 矩阵，其中行由 xs 索引，列由 xs 索引>ys。外部递归遍历行 xs，对于其中的每一行，当 xs = x :: xs' 时，内部递归遍历其列 ys< /code> 从具有较小索引 xs' 的另一行生成该行的条目。

From Coq Require Import String Ascii.
Local Open Scope string_scope.

Infix "::" := String.

(* structural recursion on xs *)
Fixpoint edit (xs ys : string) : nat :=
  match xs with
  | "" => String.length ys
  | x :: xs' =>
    (* structural recursion on ys *)
    let fix edit_xs ys :=
      match ys with
      | "" => String.length xs
      | y :: ys' =>
        let orth := min (edit xs' ys) (edit_xs ys') in
        if (x =? y)%char then
          min (edit xs' ys') orth
        else
          orth
      end in
    edit_xs ys
  end.