我试图在 Coq 中定义并证明正确的函数,该函数可以有效地比较两个排序列表。由于它并不总是在结构较小的项上递归(第一个或第二个列表较小),Fixpoint
不会接受它,所以我尝试使用Program Fixpoint
反而。
当尝试使用策略证明函数的属性时simpl
or program_simpl
,Coq 花费几分钟计算,然后生成一个长达数百行的巨大术语。我想知道我是否正在使用Program Fixpoint
错误的方式,或者在推理时是否应该使用其他策略而不是简化?
我还想知道在像这样的参数中包含正确性所需的属性是否是一个好习惯,或者最好有一个单独的包装函数将正确性属性作为参数,并使该函数仅将两个列表进行比较?
请注意,我确实尝试定义一个更简单的版本make_diff
,仅将 l1 和 l2 作为参数并固定类型A
和关系R
,但这仍然产生了一个巨大的术语program_simpl
or simpl
战术被应用。
*编辑:我的包含内容是(尽管这里可能并不需要全部):
Require Import Coq.Sorting.Sorted.
Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Definitions.
Require Import Recdef.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.
代码:
Definition is_decidable (A : Type) (R : relation A) := forall x y, {R x y} + {~(R x y)}.
Definition eq_decidable (A : Type) := forall (x y : A), { x = y } + { ~ (x = y) }.
Inductive diff (X: Type) : Type :=
| add : X -> diff X
| remove : X -> diff X
| update : X -> X -> diff X.
Program Fixpoint make_diff (A : Type)
(R : relation A)
(dec : is_decidable A R)
(eq_dec : eq_decidable A)
(trans : transitive A R)
(lt_neq : (forall x y, R x y -> x <> y))
(l1 l2 : list A)
{measure (length l1 + length l2) } : list (diff A) :=
match l1, l2 with
| nil, nil => nil
| nil, (new_h::new_t) => (add A new_h) :: (make_diff A R dec eq_dec trans lt_neq nil new_t)
| (old_h::old_t), nil => (remove A old_h) :: (make_diff A R dec eq_dec trans lt_neq old_t nil)
| (old_h::old_t) as old_l, (new_h::new_t) as new_l =>
if dec old_h new_h
then (remove A old_h) :: make_diff A R dec eq_dec trans lt_neq old_t new_l
else if eq_dec old_h new_h
then (update A old_h new_h) :: make_diff A R dec eq_dec trans lt_neq old_t new_t
else (add A new_h) :: make_diff A R dec eq_dec trans lt_neq old_l new_t
end.
Next Obligation.
Proof.
simpl.
generalize dependent (length new_t).
generalize dependent (length old_t).
auto with arith.
Defined.
Next Obligation.
Proof.
simpl.
generalize dependent (length new_t).
generalize dependent (length old_t).
auto with arith.
Defined.