coq - Coq 中 bool 表达式的案例证明

Question

我有一个包含功能:

Fixpoint contains (l: list string) (x: string): bool :=
  match l with
  | [] => false
  | h :: tl => (if (string_dec h x) then true else (contains tl x))
  end.

它检查字符串是否在字符串列表中。我想通过对是否 contains (vars e) y进行案例分析来证明一个定理。持有。但是，当我对这个 bool 值进行破坏时，对于不同的子案例，我没有得到任何额外的假设。

我该如何解决这个问题？

Answer 1

如果你想得到相应的假设，就用“方程”给它们起个名字。即:destruct (contains (vars e) y) eqn:name.