Coq中的案例分析证明 [英] Proof by case analysis in Coq

问题描述

我试图证明有关以下功能的命题：

I am trying to prove a Proposition about the following function:

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为true的情况下，进一步考虑leq_nat n m中的案例分析。

I am trying to prove some fact involving division. I wrote down an informal proof were I first consider a case analysis in lt_nat 0 n and then in the case when lt_nat is true a further case analysis in leq_nat n m. This is in order to reduce the definition of division.

但是我找不到在Coq中表达这种案例分析的方法。我尝试了 destruct（leq_nat n m），但是它什么也没做。我希望Coq会生成两个子目标：一个目标是假设 leq_nat nm =假来证明我的主张，而另一个目标是假设 leq_nat nm = true code>。

However I can not find how to express this case analysis in Coq. I tried with destruct (leq_nat n m) but it does nothing. I am expecting Coq to generate two subgoals: one where I need to prove my proposition assuming leq_nat n m = false and one assuming leq_nat n m = true.

此外，我无法在证明中展开除法的定义！当我尝试展开除法时，我得到： division_func（existT（fun _：nat => nat）mn）。

Furthermore, I can not unfold the definition of division in my proof! When I try unfold division I get: division_func (existT (fun _ : nat => nat) m n).

如何在 leq_nat nm 中进行案例分析？为什么我不能像平常使用其他功能一样显示除法的定义？

How can I perfom case analysis in leq_nat n m? Why is it that I can not unfold the definition of division as I usually do with other functions?

谢谢。

推荐答案

由于 Program Fixpoint ，一切都比平时更复杂，它不能像传统版本那样定义您的功能固定点，因为它需要找到一种结构上递归的方式来定义它。 division 的真正含义是隐藏在 division_func 中。

Everything is more complicated than usual because of Program Fixpoint, which does not define your function as you would expect with a classic Fixpoint, since it needs to find a structurally recursive way of defining it. What division really is, is hidden in division_func.

因此，要操纵您的功能，您需要证明基本的引理，包括一个说明您的函数可以被其主体代替的引理。

Therefore, to manipulate your function, you need to prove basic lemmas, including the one stating that your function can be replaced by its body.

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.

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

Now, the question is how to prove this result. Here is the only solution I know, which I consider really unsatisfying.

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

I use the tactic fix_sub_eq located in Program.Wf, or fix_sub_eq_ext in Program.Wf.WfExtensionality.

这给出了类似的内容：

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 直接调用它们，从而给您一个目标。

But the second goal is quite complicated. The easy and general way of solving it is to use the axioms proof_irrelevance and functional_extensionality. It should be possible to prove this particular subgoal without any axioms, but I have not found the right way to do it. Instead of manually applying the axioms, you can use the second tactic fix_sub_eq_ext which calls them directly, leaving you a single goal.

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 的原因，该函数具有其他默认值，但直接生成等式引理。

I have not found a better way to use Program Fixpoint, that's why I prefer using Function, which has other defaults, but generates directly the equation lemma.

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.

现在您有了方程引理，可以照常重写并推理。

Now you have the equation lemma, you can rewrite with it and reason as usual.

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

About your problem with destruct, destruct does not unfold the definitions. Therefore, if you have no occurrences of the term you're destructing in your goal or any of the hypotheses, destruct will not do anything interesting, unless you save the equation it produces. You can use destruct ... eqn:H for this purpose. I did not know case_eq but it seems to do the same thing.

这篇关于Coq中的案例分析证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！