一切都比平常更复杂,因为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.
现在的问题是如何证明这个结果。这是我所知道的唯一解决方案,我认为它确实令人不满意。
我用的是战术fix_sub_eq
位于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
and 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
但它似乎做了同样的事情。