我如何推理 Coq 中的条件？

Question

我正在研究 Coq 标准库中的 ListSet 模块。我不确定如何在证明中推理条件。例如，我在以下证明中遇到了麻烦。为上下文提供了定义。

Fixpoint set_mem (x : A) (xs : set) : bool :=
match xs with
  | nil       => false
  | cons y ys =>
      match Aeq_dec x y with
        | left  _ => true
        | right _ => set_mem x ys
      end
end.

Definition set_In : A -> set -> Prop := In (A := A).

Lemma set_mem_correct1 : forall (x : A) (xs : set),
  set_mem x xs = true -> set_In x xs.
Proof. intros. induction xs.
  discriminate.
  simpl; destruct Aeq_dec with a x.
    intuition.
    simpl in H.

当前的证明状态包括Aeq_dec 的inr 作为假设。我已经放弃了归纳的基本情况和Aeq_dec 的inl 为真的归纳情况。

  A : Type
  Aeq_dec : forall x y : A, {x = y} + {x <> y}
  x : A
  a : A
  xs : list A
  H : (if Aeq_dec x a then true else set_mem x xs) = true
  IHxs : set_mem x xs = true -> set_In x xs
  n : a <> x
  ============================
   a = x \/ set_In x xs

如果a <> x 为真，则H 为真的唯一方法是set_mem xs 为真。我应该能够将H 中的条件应用于a <> x 以获得set_mem xs。但是，我不明白如何做到这一点。如何处理、分解或应用条件？

Answer 1

你试过了吗？ （语法可能有问题，这里没有 coqtop atm）

destruct (Aeq_dec x a);
[ subst; elim (n eq_refl)
| right; apply (IHxs H)
].

(if <foo> 或多或少与match <foo> with 相同。您必须减少 (destruct, case, ...) 以便可以决定匹配（或@987654326 @，事情必须减少到你使用它的任何类型的第一个或第二个构造函数。）大多数时候，你需要进行大小写分析的值（虽然不是在这里）。如果你需要它，做一个remember (<value>) as foo; destruct foo，而不是直接破坏。）