coq - Coq 中的案例分析证明

Question

我正在尝试证明关于以下函数的命题:

Program Fixpoint division (m:nat) (n:nat) {measure m} : nat :=
match lt_nat 0 n with
  | false => 0
  | true => match leq_nat n m with
      | false => 0
      | true => S (division (menos m n) n)
  end
end.

menos是自然减法。

我试图证明一些涉及除法的事实。我写下了一个非正式的证明，我首先考虑在 lt_nat 0 n 中进行案例分析，然后在 lt_nat 为真时在 leq_nat n m 中进行进一步的案例分析。这是为了减少除法的定义。

但是我找不到如何在 Coq 中表达这个案例分析。我尝试过 destruct (leq_nat n m)但它什么也没做。我期望 Coq 生成两个子目标:一个是我需要证明我的命题，假设 leq_nat n m = false假设 leq_nat n m = true .

此外，我无法在我的证明中展开除法的定义!当我尝试 unfold division我得到:division_func (existT (fun _ : nat => nat) m n) .

如何在leq_nat n m中进行案例分析？为什么我不能像通常处理其他函数那样展开除法的定义？

谢谢。

Answer 1

由于Program Fixpoint，一切都比平常更复杂，它没有像您期望的经典Fixpoint那样定义您的函数，因为它需要找到一个结构性的递归的方式来定义它。 division 的真正含义隐藏在 division_func 中。

因此，要操纵您的函数，您需要证明基本引理，包括声明您的函数可以被其主体替换的引理。

Lemma division_eq : forall m n, division m n = match lt_nat 0 n with
| false => 0
  | true => match leq_nat n m with
      | false => 0
      | true => S (division (menos m n) n)
  end
end.

现在的问题是如何证明这个结果。这是我所知道的唯一解决方案，我认为它确实不能令人满意。

我使用位于 Program.Wf 中的 fix_sub_eq 策略，或位于 Program.Wf.WfExtensionality 中的 fix_sub_eq_ext .

这给出了类似的东西:

Proof.
  intros.
  unfold division. unfold division_func at 1.
  rewrite fix_sub_eq; repeat fold division_func.
  - simpl. destruct (lt_nat 0 n) eqn:H.
    destruct (leq_nat n m) eqn:H0. reflexivity.
    reflexivity. reflexivity.

但是第二个目标相当复杂。解决这个问题的简单而通用的方法是使用公理 proof_irrelevance 和 function_extensionality。应该可以在没有任何公理的情况下证明这个特定的子目标，但我还没有找到正确的方法。您可以使用第二种策略 fix_sub_eq_ext 直接调用它们，而不是手动应用公理，从而为您留下一个目标。

Proof.
  intros.
  unfold division. unfold division_func at 1.
  rewrite fix_sub_eq_ext; repeat fold division_func.
  simpl. destruct (lt_nat 0 n) eqn:H.
  destruct (leq_nat n m) eqn:H0. reflexivity.
  reflexivity. reflexivity.
Qed.

我还没有找到更好的方法来使用Program Fixpoint，这就是为什么我更喜欢使用Function，它有其他默认值，但直接生成方程引理。

Require Recdef.
Function division (m:nat) (n:nat) {measure (fun n => n) m} : nat :=
match lt_nat 0 n with
  | false => 0
  | true => match leq_nat n m with
      | false => 0
      | true => S (division (menos m n) n)
  end
end.
Proof.
  intros m n. revert m. induction n; intros.
  - discriminate teq.
  - destruct m. discriminate teq0.
    simpl. destruct n. destruct m; apply le_n.
    transitivity m. apply IHn. reflexivity. assumption. apply le_n.
Qed.

Check division_equation.

现在您有了方程引理，您可以用它重写并像往常一样进行推理。

关于 destruct 的问题，destruct 不会展开定义。因此，如果您在目标或任何假设中没有出现要破坏的项，则 destruct 不会做任何有趣的事情，除非您保存它生成的方程。为此，您可以使用destruct ... eqn:H。我不知道 case_eq 但它似乎做了同样的事情。