从归纳谓词列出A - >列表A - > bool

Question

在尝试在列表上的归纳谓词上编写可重用代码时,我自然会声明:

Parameter A:Type.

然后我继续定义二元谓词(例如):

Inductive prefix : list A -> list A -> Prop :=
  | prefixNil: forall (l: list A), prefix nil l
  | prefixCons: forall (a: A)(l m:list A), prefix l m -> prefix (a::l) (a::m).

表达了给定列表是另一个列表的前缀这一事实.然后,人们可以继续研究这种关系并显示(例如)它是一个偏序.到现在为止还挺好.但是,很容易定义一个与数学概念不符的归纳谓词.我想通过进一步定义函数来验证归纳定义:

isPrefixOf: list A -> list A -> bool

为了证明等价:

Theorem prefix_validate: forall (l m: list A), 
  prefix l m <-> isPrefixOf l m = true.

这是我需要限制代码的一般性的地方,因为我不能再使用了list A.在Haskell,我们有isPrefixOf :: Eq a => [a] -> [a] -> Bool,所以我理解我需要做一些假设A,比如' Eq A'.当然,我可以假设:

Parameter equal: A -> A -> bool
Axiom equal_validate: forall (a b: A),
  a = b <-> equal a b = true.

并从那里开始.我可能会在另一个文件或一个部分中执行此操作,以免破坏前一代码的完整通用性.但是,我觉得我正在重新发明轮子.这可能是一种常见的模式(表达类似Haskell的东西Eq a => ...).

哪个(惯用的,常见的)声明应该对A允许我继续进行的类型做出,同时保持代码尽可能通用？

Answer 1

（编辑：Coq 标准库提供了==具有EqDec类型类的 Haskell 运算符的直接对应项），有关更多详细信息，请参阅 @anton-trunov 答案）。

一般来说，您至少有两个选择：

• 假设类型A具有可判定的相等性。这可以通过多种形式完成，通常您想要

  Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y})
  

  然后，您可以析构A_dec来比较元素。这在标准库的多个部分中使用，您可以使用类型类进行自动解析。我相信有几个第三方库使用这种方法（coq-ext-lib、TLC）。代码将变为：

  Require Import Coq.Lists.List.
  Section PrefixDec.
  
  Variable A : Type.
  Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y}).
  Implicit Types (s t : list A).
  
  Fixpoint prefix s t := 
    match s, t with
    | nil, t         => true
    | s, nil         => false
    | x :: s, y :: t => match A_dec x y with
                        | left  _ => prefix s t
                        | right _ => false
                        end
    end.
  
  Inductive prefix_spec : list A -> list A -> Prop :=
    | prefix_nil  : forall (l: list A),
        prefix_spec nil l
    | prefix_cons : forall (a: A) (l m:list A),
        prefix_spec l m -> prefix_spec (a::l) (a::m).
  
  Hint Constructors prefix_spec.
  
  Lemma prefixP s t : prefix_spec s t <-> prefix s t = true.
  Proof.
  revert t; induction s as [|x s]; intros [|y t]; split; simpl; try congruence; auto.
  + now intros H; inversion H.
  + destruct (A_dec x y); simpl; intros H; inversion H; subst; try congruence.
    now rewrite <- IHs.
  + destruct (A_dec x y); intros H; inversion H; subst.
    now constructor; rewrite IHs.
  Qed.
  
  End PrefixDec.
  
  (* Compute example *)
  Import ListNotations.
  Compute (prefix _ PeanoNat.Nat.eq_dec [2; 3; 4] [ 2; 3; 4; 5]).
  Compute (prefix _ PeanoNat.Nat.eq_dec [2; 3; 4] [ 2; 3; 5]).
  

• 按照您的方法并提供布尔相等运算符。math-comp 库提供了一个类层次结构，其中包含具有可判定的 equals 的类型类eqType。因此，对于A : eqType, x y : A，您可以使用==运算符来比较它们。有关列表的示例，请参阅http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.seq.html 。

  您的equal和validate假设完全封装在eqType（名为==和eqP）中。代码是：

  From mathcomp
  Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
  
  Section PrefixEq.
  
  Variable A : eqType.
  Implicit Types (s t : seq A).
  
  Fixpoint prefix s t :=
    match s, t with
    | nil, t          => true
    | s, nil          => false
    | x :: s, y :: t => if x == y then prefix s t else false
    end.
  
  Inductive prefix_spec : list A -> list A -> Prop :=
    | prefix_nil  : forall (l: list A),
        prefix_spec nil l
    | prefix_cons : forall (a: A) (l m:list A),
        prefix_spec l m -> prefix_spec (a::l) (a::m).
  
  Hint Constructors prefix_spec.
  
  Lemma prefixP s t : reflect (prefix_spec s t) (prefix s t).
  Proof.
  apply: (iffP idP); elim: s t => // x s ihs [|y t] //=.
  - by case: eqP => // ->; auto.
  - by move=> H; inversion H.
  - by move=> H; inversion H; subst; rewrite eqxx ihs.
  Qed.
  
  End PrefixEq.
  
  Compute (prefix _ [:: 1;2;3] [:: 1;2;3]).
  Compute (prefix _ [:: 1;2;3] [:: 1;3;3]).
  

  math-comp 方法的一个好处是它会自动eqType推断nat. 这有助于保持证明的轻量级。关于上述证明的一个注释是，我将通过使用“反转视图”来避免反转，但这是一个不同的主题。另外，使用已经存在的seq.subseq可能更有意义，或者您可能想要类似的东西：

  Definition is_prefix (A : eqType) (s t : seq A) := s == take (size s) t.
  

什么更地道？恕我直言，这确实取决于。AFAICT 不同的开发人员喜欢不同的技术。我发现第二种方法最适合我，但需要eqP在证明中进行一些额外的应用。

代码在这里： https: //x80.org/collacoq/akumoyutaz.coq