I've proved an equivalence and_distributes_over_or:
Theorem and_distributes_over_or : forall P Q R : Prop,
P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
Elsewhere I have a goal of
exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 xs)
(For context I'm working through Logical Foundations; I'm on the In_map_iff exercise of the chapter on constructive logic. Please don't tell me the solution to the exercise though!)
I tried to use rewrite and_distributes_over_or on my goal (to get exists x0 : A, (f x0 = y /\ x = x0) \/ (f x0 = y /\ In x0 xs)). I got an error:
Found no subterm matching "?P /\ (?P0 \/ ?P1)" in the current goal.
Using my human brain I can see what seems to be a very obvious subterm of that form in the goal. Why can't Coq, with its non-human non-brain, see it under the existential quantifier? Do you have any tips to make this work?
I've read a previous question with a similar title to this one but that's about rewriting in hypotheses, not goals, and the answer doesn't appear to be applicable to my situation.
Just use setoid_rewrite instead of rewrite, and make sure to Require Setoid. (though loading List has already done so in this case).
The pattern Coq is looking for is underneath a binder; that is, it's in the body of a function. The binder isn't obvious because it's part of the exists, but your goal is actually ex (fun (x0:A) => f x0 = y /\ (x = x0 \/ In x0 xs)), and Coq's notation mechanism prints it nicely as exists x0, .... The basic rewrite tactic can't do rewrites inside functions, but setoid_rewrite can.
Aside: note that the definition ex and its notation exists x, ... aren't built-in to Coq but are defined in the standard library! You can inspect these sort of things with Locate exists (to find the notation) and Print ex (to view the definition). There's also Unset Printing Notations. if you're not sure what notations are in use, though bear in mind that there are a lot of notations you probably take for granted, like /\, =, and even ->.