1

我们将使用有限集的标准定义：

Inductive fin : nat -> Set :=
| F1 : forall {n : nat}, fin (S n)
| FS : forall {n : nat}, fin n -> fin (S n).

让我们假设我们有一些P : forall {m : nat} (x y : fin m) : Set（重要的是 的两个参数P属于同一类型）。出于演示目的，设 P 为：

Definition P {m : nat} (x y : fin m) := {x = y} + {x <> y}.

现在，我们想编写一个比较两个数字的自定义函数：

Fixpoint feq_dec {m : nat} (x y : fin m) : P x y.

这个想法很简单：我们匹配xand y，对于x = F1，y = F1我们平凡地返回相等，对于x = FS x'，y = FS y'我们递归地调用过程x'和y'，对于其他情况，我们可以平凡地返回不等式。

将这个想法直接翻译成 Coq 显然失败了：

refine (
  match x, y return P x y with
  | F1 _, F1 _ => _
  | FS _ x', F1 _ => _
  | F1 _, FS _ y' => _
  | FS _ x', FS _ y' => _
  end
).

(*
 * The term "y0" has type "fin n0" while it is expected to have type "fin n".
 *)

在比赛期间x，y我们丢失了类型信息，因此我们无法将它们应用于P. 传递类型相等证明的标准技巧在这里没有帮助：

refine (
  match x in fin mx, y in fin my return mx = my -> P x y with
  | F1 _, F1 _ => _
  | FS _ x', F1 _ => _
  | F1 _, FS _ y' => _
  | FS _ x', FS _ y' => _
  end eq_refl
).

(*
 * The term "y0" has type "fin my" while it is expected to have type "fin mx".
 *)

那么，也许我们可以使用该相等性证明来强制转换x具有与 ? 相同的类型 y？

Definition fcast {m1 m2 : nat} (Heq : m1 = m2) (x : fin m1) : fin m2.
Proof.
  rewrite <- Heq.
  apply x.
Defined.

我们还需要能够在以后摆脱演员阵容。但是，我注意到这 fcast eq_refl x = x还不够，因为我们需要让它与任意等价证明一起工作。我找到了一个叫做 UIP 的东西，它可以满足我的需要。

Require Import Coq.Program.Program.

Lemma fcast_void {m : nat} : forall (x : fin m) (H : m = m),
  fcast H x = x.
Proof.
  intros.
  rewrite -> (UIP nat m m H eq_refl).
  trivial.
Defined.

现在我们准备完成整个定义：

refine (
  match x in fin mx, y in fin my
  return forall (Hmx : m = mx) (Hmy : mx = my), P (fcast Hmy x) y with
  | F1 _, F1 _ => fun Hmx Hmy => _
  | FS _ x', F1 _ => fun Hmx Hmy => _
  | F1 _, FS _ y' => fun Hmx Hmy => _
  | FS _ x', FS _ y' => fun Hmx Hmy => _
  end eq_refl eq_refl
); inversion Hmy; subst; rewrite fcast_void.
- left. reflexivity.
- right. intro Contra. inversion Contra.
- right. intro Contra. inversion Contra.
- destruct (feq_dec _ x' y') as [Heq | Hneq].
  + left. apply f_equal. apply Heq.
  + right. intro Contra. dependent destruction Contra. apply Hneq. reflexivity.
Defined.

它通过了！但是，它不会评估任何有用的价值。例如，以下产生一个具有五个嵌套匹配项而不是一个简单值（in_right或in_left）的术语。我怀疑问题出在我使用的 UIP 公理上。

Compute (@feq_dec 5 (FS F1) (FS F1)).

所以最后，我想出的定义几乎没有用。我也尝试过使用convoy 模式进行嵌套匹配，而不是同时匹配两个值，但我遇到了同样的障碍：一旦我对第二个值进行匹配，就P不再适用于它。我可以用其他方式吗？

4

2 回答 2

2

这是一个已知问题，在大多数情况下，使用底层证券的相等性nat然后获利比单to_nat射函数更好：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Import PeanoNat Fin.

Fixpoint to_nat m (x : t m) :=
  match x with
  | F1 _   => 0
  | FS _ x => (to_nat x).+1
  end.

Lemma to_nat_inj m : injective (@to_nat m).
Proof.
elim: m / => /= [|m t iht y].
  exact: (caseS (fun n (y : t n.+1) => _)).
move: m y t iht.
by apply: (caseS (fun n (y : t n.+1) => _)) => //= n p t iht [] /iht ->.
Qed.

Lemma feq_dec {m : nat} (x y : t m) : {x = y} + {x <> y}.
Proof.
have [heq | heqN] := Nat.eq_dec (to_nat x) (to_nat y).
  by left; apply: to_nat_inj.
by right=> H; apply: heqN; rewrite H.
Qed.

但即便如此，处理起来仍然很麻烦。您可以尝试'I_n在 ssreflect 中使用类型 include 将计算值与边界分开，在 SO 中进行一些搜索应该会给您足够的指针。

如果您将Qeds 转换Defined为上述内容，将为您的情况进行计算，并且通常它应该足以给您left ?或right ?允许依赖它的证明继续。

但是，如果您希望它在不相等的情况下通过正常形式，则需要进行大量调整[主要是O_S引理不透明，这也会影响Nat.eq_dec]

于 2017-07-23T13:58:01.330 回答
1

您可以手写条款，但这是一场噩梦。在这里，我描述了计算部分并使用策略来处理证明：

Fixpoint feq_dec {m : nat} (x y : fin m) : P x y.
refine (
match m return forall (x y : fin m), P x y with
  | O    => _
  | S m' => fun x y =>
  match (case x, case y) with
    | (inright eqx            , inright eqy)             => left _
    | (inleft (exist _ x' eqx), inright eqy)             => right _
    | (inright eqx            , inleft (exist _ y' eqy)) => right _
    | (inleft (exist _ x' eqx), inleft (exist _ y' eqy)) =>
    match feq_dec _ x' y' with
      | left eqx'y'   => left _
      | right neqx'y' => right _
    end
  end
end x y); simpl in *; subst.
- inversion 0.
- reflexivity.
- intro Heq; apply neqx'y'.
  assert (Heq' : Some x' = Some y') by exact (f_equal finpred Heq).
  inversion Heq'; reflexivity.
- inversion 1.
- inversion 1.
- reflexivity.
Defined.

以这种方式定义的函数按预期工作：

Compute (@feq_dec 5 (FS F1) (FS F1)).
(* 
 = left eq_refl
 : P (FS F1) (FS F1)
*)

此代码依赖于 3 个技巧：

1. 首先检查 bound m。

实际上，如果您对边界一无所知，您将分别从比赛中m了解两个不同的事实，并且您需要协调这些事实（即表明给您的两个前任实际上是相等的）。另一方面，如果您知道它具有形状，那么您可以...xymmS m'

2.使用case基于边界形状反转术语的函数

如果您知道界限有一个形状S m'，那么您就知道您的每个fins 处于以下两种情况之一：finisF1或 it is FS x'for some x'。case使它正式：

Definition C {m : nat} (x : fin (S m)) :=
  { x' | x = FS x' } + { x = F1 }.

Definition case {m : nat} (x : fin (S m)) : C x :=
match x in fin (S n) return { x' | x = FS x' } + { x = F1 } with
  | F1    => inright eq_refl
  | FS x' => inleft (exist _ x' eq_refl)
end.

Coq 将足够聪明，可以检测到我们返回的值是case它所接受参数的直接子项。x因此，当两者都y具有形状时执行递归调用FS _将不是问题！

3. 使用与 ad-hoc 函数的一致性来剥离构造函数

在我们执行了递归调用但得到否定回答的分支中，我们需要证明FS x' <> FS y'知道x' <> y'. 这意味着我们需要Heq : FS x' = FS y'变成x' = y'.

因为FS有一个复杂的返回类型，简单地执行inversiononHeq不会产生可用的结果（我们得到 ap和 a 的依赖对之间的相等性fin p）。这是finpred发挥作用的：它是一个完整的功能，当面对它时，它会FS _简单地剥离FS构造函数。

Definition finpred {m : nat} (x : fin m) : option (fin (pred m)) :=
match x with
  | F1    => None
  | FS x' => Some x'
end.

结合起来f_equal，Heq我们得到一个证明，证明Some x' = Some y'我们可以使用inversion并获得我们想要的平等。

编辑：我已将所有代码放在一个独立的 gist中。

于 2017-07-23T14:23:13.400 回答