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

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成立进行案例分析来证明一个定理。但是，当我对这个布尔值进行破坏时，对于不同的子情况，我没有得到任何额外的假设。

我该如何解决这个问题？

标签： coq

Answer 1

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