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.

coq coq-tactic