Proof by cases on a boolean expression in Coq

user_5069802 0
Viewed 324

I have a contains function:

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.

which checks if a string is in a list of strings. I would like to prove a theorem by doing case analysis on whether contains (vars e) y holds. However, when I destruct on this boolean I don't get any extra hypothesis for the different subcases.

How can I solve this issue?

coq
1 Answers

If you want to get the corresponding assumptions, use "eqn" to give a name for them. that is: destruct (contains (vars e) y) eqn:name.

user_131956180
Related