## Stream: math-comp users

### Topic: Destruct `predD`

#### Julin Shaji (Mar 26 2024 at 05:38):

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?

#### Julin Shaji (Mar 26 2024 at 05:45):

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.
``````

#### Reynald Affeldt (Mar 26 2024 at 05:50):

`/=` alone reveals the underlying boolean operators

#### Reynald Affeldt (Mar 26 2024 at 05:55):

`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: Jul 15 2024 at 21:02 UTC