functional-programming - 我如何推理 Coq 中的条件？

Question

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

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.

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

  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

H 的唯一途径如果 a <> x 为真如果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 , ...) 以便可以决定匹配(或者对于 if ，事情必须减少到第一个或你使用它的任何类型的第二个构造函数。)大多数时候，你需要得到案例分析的值(虽然不是在这里)。如果你需要它，做一个 remember (<value>) as foo; destruct foo 而不是直接破坏。)