How can we case analysis a goal involving a `predD`

?

As in:

```
From mathcomp Require Import all_ssreflect.
Goal forall (A: Type) (l: seq A) (p q: seq A -> bool),
[predD p & q] l.
move => A l p q.
(*
1 subgoal
A : Type
l : seq A
p, q : seq A -> bool
========================= (1 / 1)
[predD p & q] l
*)
```

Now, we could check the case for p and q like:

- p l
- ¬ (q l)

How can this be done?

I guess this is a way?

```
Goal forall (A: Type) (l: seq A) (p q: seq A -> bool),
[predD p & q] l.
move => A l p q.
Unset Printing Notations.
rewrite /predD.
rewrite simpl_predE.
Set Printing Notations.
apply/andP.
split.
```

`/=`

alone reveals the underlying boolean operators

`apply/andP; split`

is indeed the way to split a boolean conjunction in the goal (note however that depending on what you are doing this might not be necessary, if for example you can solve (parts of) the goal using rewrite's and simplifications)

Last updated: Oct 13 2024 at 01:02 UTC