Coq - 如何应用带有匹配子句的蕴涵？

Question

我正在写一个快速排序正确性的证明。

我的程序定义了一个分区类型，它处理快速排序的递归分区步骤。

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.

我写了一个具有以下结构的引理，它指出已排序分区的左右分区也必须排序。该引理使用“匹配”语法将分区分成左右子分区:

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 由于模式匹配构造而无法统一。

Answer 1

你可以使用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.