Coq 中的案例分析证明
Proof by case analysis in Coq
我正在尝试证明关于以下函数的命题:
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
中进行案例分析?为什么我平时用其他函数做除法的定义不能展开?
谢谢。
由于 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
和 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
但它似乎做同样的事情。
我正在尝试证明关于以下函数的命题:
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
中进行案例分析?为什么我平时用其他函数做除法的定义不能展开?
谢谢。
由于 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
和 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
但它似乎做同样的事情。