证明在勒柯克

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为true的情况下，在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_ext在Program.Wf.WfExtensionality战术fix_sub_eq。

这给了像：

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，但它似乎做同样的事情。