Stream: math-comp users

Topic: Destruct `predD`


view this post on Zulip 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:

How can this be done?

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (Mar 26 2024 at 05:50):

/= alone reveals the underlying boolean operators

view this post on Zulip 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