从归纳谓词到列表 A -> 列表 A -> 布尔
From an Inductive predicate to list A -> list A -> bool
尝试在列表的归纳谓词上编写可重用代码时，我自然地声明：
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 类型，我应该做出哪种（惯用的、常见的）声明，这样我才能继续，同时使代码尽可能通用？
（编辑：Coq 标准库提供了 Haskell == 运算符的直接对应 EqDec 类型 class），请参阅@anton-trunov 回答了解更多详情）。
一般来说，您至少有两个选择：
假设类型 A 具有可判定的相等性。这可以通过多种形式完成，通常你想要
Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y})
然后，你可以解构A_dec来比较元素。这用于标准库的多个部分，您可以使用类型 class 进行自动解析。我相信有几个第三方库使用这种方法（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 库提供了一个 class 层次结构，其中 class 类型具有可判定的相等性 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 方法的一个好处是它会自动为 nat 等类型推断 eqType 个实例。这有助于保持证明轻量级。关于上述证明的注意事项是我会通过使用 and "inversion view" 来避免倒置，但这是另一个话题。此外，使用已经存在的 seq.subseq 可能更有意义，或者您可能想要这样的东西：
Definition is_prefix (A : eqType) (s t : seq A) := s == take (size s) t.
什么更地道？恕我直言，这真的取决于。 AFAICT 不同的开发人员喜欢不同的技术。我发现第二种方法最适合我，代价是在证明中需要一些额外的 eqP 应用程序。
为了完成@ejgallego的回答，你也可以使用模块系统做相应的假设。如果你Require Import Structures.Equalities，你有一些有用的模块类型。例如，Typ 只包含类型 t，而 UsualBoolEq 假定存在运算符 eqb : t -> t -> bool 验证 eqb_eq : forall x y : t, eqb x y = true <-> x = y.
你可以把你的定义放在仿函数中。
Require Import Structures.Equalities.
Require Import List. Import ListNotations.
Require Import Bool.
Module Prefix (Import T:Typ).
Inductive prefix : list t -> list t -> Prop :=
| prefixNil: forall (l: list t), prefix nil l
| prefixCons: forall (a: t)(l m:list t), prefix l m -> prefix (a::l) (a::m).
End Prefix.
Module PrefixDecidable (Import T:UsualBoolEq).
Include Prefix T.
Fixpoint isPrefixOf (l m : list t) :=
match l with
| [] => true
| a::l' =>
match m with
| [] => false
| b::m' => andb (eqb a b) (isPrefixOf l' m')
end
end.
Theorem prefix_validate: forall (l m: list t),
prefix l m <-> isPrefixOf l m = true.
Proof.
split; intros H.
- induction H.
+ reflexivity.
+ simpl. rewrite andb_true_iff. split; [|assumption].
apply eqb_eq; reflexivity.
- revert dependent m; induction l as [|a l']; intros m H.
+ constructor.
+ destruct m as [|b m'].
* discriminate.
* simpl in H. rewrite andb_true_iff in H. destruct H as [H H0].
apply eqb_eq in H. subst b.
constructor. apply IHl'; assumption.
Qed.
End PrefixDecidable.
但是请注意，模块系统并不是 Coq 中使用起来最方便的部分。我倾向于更喜欢@ejgallego 提供的选项。提供此答案主要是为了完整性。
另一个版本，使用可判定等价 (Coq.Classes.EquivDec)。
Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Classes.EquivDec.
Set Implicit Arguments.
Section Prefix.
Variable A : Type.
Context `{EqDec A eq}. (* A has decidable equivalence *)
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).
Hint Constructors prefix.
Fixpoint isPrefixOf (l1 l2 : list A) : bool :=
match l1, l2 with
| [], _ => true
| _, [] => false
| h1 :: t1, h2 :: t2 => if h1 == h2 then isPrefixOf t1 t2
else false
end.
Theorem prefix_validate : forall (l m: list A),
prefix l m <-> isPrefixOf l m = true.
Proof.
induction l; split; intro Hp; auto; destruct m; inversion Hp; subst.
- simpl. destruct (equiv_dec a0 a0).
+ apply IHl. assumption.
+ exfalso. apply c. reflexivity.
- destruct (equiv_dec a a0).
+ rewrite e. constructor. apply IHl. assumption.
+ discriminate H1.
Qed.
End Prefix.
让我提供一些使用 isPrefixOf 进行计算的示例。对于 nats 这非常简单，因为 nat 已经是 EqDec:
的一个实例
Eval compute in isPrefixOf [1;2] [1;2;3;4]. (* = true *)
Eval compute in isPrefixOf [1;9] [1;2;3;4]. (* = false *)
下面是对用户定义类型的测试：
Inductive test : Type :=
| A : test
| B : test
| C : test.
Lemma test_dec : forall x y:test, {x = y} + {x <> y}.
Proof. decide equality. Defined.
Instance test_eqdec : EqDec test _ := test_dec.
Eval compute in isPrefixOf [A;B] [A;B;C;A]. (* = true *)
Eval compute in isPrefixOf [A;C] [A;B;C;A]. (* = false *)
尝试在列表的归纳谓词上编写可重用代码时，我自然地声明：
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 类型，我应该做出哪种（惯用的、常见的）声明，这样我才能继续，同时使代码尽可能通用？
（编辑：Coq 标准库提供了 Haskell == 运算符的直接对应 EqDec 类型 class），请参阅@anton-trunov 回答了解更多详情）。
一般来说，您至少有两个选择：
假设类型
A具有可判定的相等性。这可以通过多种形式完成，通常你想要Hypothesis (A_dec : forall x y : A, {x = y} + {x <> y})然后，你可以解构
A_dec来比较元素。这用于标准库的多个部分，您可以使用类型 class 进行自动解析。我相信有几个第三方库使用这种方法（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 库提供了一个 class 层次结构，其中 class 类型具有可判定的相等性
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 方法的一个好处是它会自动为
nat等类型推断eqType个实例。这有助于保持证明轻量级。关于上述证明的注意事项是我会通过使用 and "inversion view" 来避免倒置，但这是另一个话题。此外，使用已经存在的seq.subseq可能更有意义，或者您可能想要这样的东西：Definition is_prefix (A : eqType) (s t : seq A) := s == take (size s) t.
什么更地道？恕我直言，这真的取决于。 AFAICT 不同的开发人员喜欢不同的技术。我发现第二种方法最适合我，代价是在证明中需要一些额外的 eqP 应用程序。
为了完成@ejgallego的回答，你也可以使用模块系统做相应的假设。如果你Require Import Structures.Equalities，你有一些有用的模块类型。例如，Typ 只包含类型 t，而 UsualBoolEq 假定存在运算符 eqb : t -> t -> bool 验证 eqb_eq : forall x y : t, eqb x y = true <-> x = y.
你可以把你的定义放在仿函数中。
Require Import Structures.Equalities.
Require Import List. Import ListNotations.
Require Import Bool.
Module Prefix (Import T:Typ).
Inductive prefix : list t -> list t -> Prop :=
| prefixNil: forall (l: list t), prefix nil l
| prefixCons: forall (a: t)(l m:list t), prefix l m -> prefix (a::l) (a::m).
End Prefix.
Module PrefixDecidable (Import T:UsualBoolEq).
Include Prefix T.
Fixpoint isPrefixOf (l m : list t) :=
match l with
| [] => true
| a::l' =>
match m with
| [] => false
| b::m' => andb (eqb a b) (isPrefixOf l' m')
end
end.
Theorem prefix_validate: forall (l m: list t),
prefix l m <-> isPrefixOf l m = true.
Proof.
split; intros H.
- induction H.
+ reflexivity.
+ simpl. rewrite andb_true_iff. split; [|assumption].
apply eqb_eq; reflexivity.
- revert dependent m; induction l as [|a l']; intros m H.
+ constructor.
+ destruct m as [|b m'].
* discriminate.
* simpl in H. rewrite andb_true_iff in H. destruct H as [H H0].
apply eqb_eq in H. subst b.
constructor. apply IHl'; assumption.
Qed.
End PrefixDecidable.
但是请注意，模块系统并不是 Coq 中使用起来最方便的部分。我倾向于更喜欢@ejgallego 提供的选项。提供此答案主要是为了完整性。
另一个版本，使用可判定等价 (Coq.Classes.EquivDec)。
Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Classes.EquivDec.
Set Implicit Arguments.
Section Prefix.
Variable A : Type.
Context `{EqDec A eq}. (* A has decidable equivalence *)
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).
Hint Constructors prefix.
Fixpoint isPrefixOf (l1 l2 : list A) : bool :=
match l1, l2 with
| [], _ => true
| _, [] => false
| h1 :: t1, h2 :: t2 => if h1 == h2 then isPrefixOf t1 t2
else false
end.
Theorem prefix_validate : forall (l m: list A),
prefix l m <-> isPrefixOf l m = true.
Proof.
induction l; split; intro Hp; auto; destruct m; inversion Hp; subst.
- simpl. destruct (equiv_dec a0 a0).
+ apply IHl. assumption.
+ exfalso. apply c. reflexivity.
- destruct (equiv_dec a a0).
+ rewrite e. constructor. apply IHl. assumption.
+ discriminate H1.
Qed.
End Prefix.
让我提供一些使用 isPrefixOf 进行计算的示例。对于 nats 这非常简单，因为 nat 已经是 EqDec:
Eval compute in isPrefixOf [1;2] [1;2;3;4]. (* = true *)
Eval compute in isPrefixOf [1;9] [1;2;3;4]. (* = false *)
下面是对用户定义类型的测试：
Inductive test : Type :=
| A : test
| B : test
| C : test.
Lemma test_dec : forall x y:test, {x = y} + {x <> y}.
Proof. decide equality. Defined.
Instance test_eqdec : EqDec test _ := test_dec.
Eval compute in isPrefixOf [A;B] [A;B;C;A]. (* = true *)
Eval compute in isPrefixOf [A;C] [A;B;C;A]. (* = false *)