如何解决Coq-如何将匹配项与match子句一起使用?
我正在写一个有关快速排序正确性的证明。
我的程序定义了一个分区类型,该分区类型处理快速排序的递归分区步骤。
Inductive partition : Type :=
| empty
| join (left: partition) (pivot: nat) (right: partition).
还有一个检查分区是否已排序的函数
Fixpoint p_sorted (p: partition) : bool :=
match p with
| empty => true
| join l pivot r => match l,r with
| empty,empty => true
| join _ lp _,empty => if lp <=? pivot then p_sorted l else false
| empty,join _ rp _ => if pivot <=? rp then p_sorted r else false
| join _ lp _,join _ rp _ => if (lp <=? pivot) && (pivot <=? rp) then
(p_sorted l) && (p_sorted r) else false
end
end.
我用以下结构编写了引理,该结构指出已排序分区的左右分区也必须先进行排序。该引理使用“ match with”语法将一个分区分为其左和右子分区:
Lemma foo : forall (p: partition),(match p with
| empty => True
| join left pivot right => (p_sorted p = true) -> (p_sorted left = true) /\ (p_sorted right = true)
end).
Proof. (* ... proof ... *) Qed.
这个引理已经得到证明。
现在,我想在一个新的证明中使用它,假设的形式是
p_sorted x = true
如何应用以前的引理,将其转换为p_sorted left = true /\ p_sorted right = true
?
apply foo
由于模式匹配构造而无法统一。
解决方法
您可以使用pose proof (foo x) as Hfoo
。然后,您需要使用destruct x
;在x
不为空的情况下,您将需要执行一些操作。
但是,这样的证明很尴尬,所以我建议您改进理论的“ API”,即foo
的声明方式;最好将foo
专用于p = join ...
情况。
编辑:实际上,可以通过修改p_sorted
的定义来简化某些证明。该定义需要对树进行“ 2级下移”模式匹配并重复一些逻辑,因此foo
可能需要重复2级区分大小写。而是,代码可以类似于以下内容(未经测试)编写:
Definition get_root (p : partition) : option nat :=
match p with
| empty => None
| join _ pivot _ => Some pivot
end.
Definition onat_le (p1 p2 : option nat) :=
match p1,p2 with
| Some n1,Some n2 => n1 <=? n2
| _,_ => false
end.
Fixpoint p_sorted (p: partition) : bool :=
match p with
| empty => true
| join l pivot r => p_sorted l && p_sorted r && onat_le (get_root l) (Some pivot) && onat_le (Some pivot) (get_root r)
end.
Lemma foo l pivot r:
p_sorted (join l pivot r) = true -> p_sorted l = true /\ p_sorted r = true.
Proof.
simpl. intros Hsort. split.
- destruct (p_sorted l); simpl in *; easy.
- destruct (p_sorted r); simpl in *; easy.
Qed.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。