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的策略Program.Wf或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和functional_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，但它似乎也做了同样的事情。