## Stream: math-comp users

### Topic: and3

#### Ricardo (Feb 23 2023 at 20:39):

Is there an intro pattern for `and3`? Or how is `and3` usually used?
Also, it'd be great to have `and3PP` in ssrbool.

#### Julien Puydt (Feb 23 2023 at 20:46):

``````From mathcomp Require Import all_ssreflect.

Section Examples.

Variable P Q R: Prop.

Lemma as_hyp: [/\ P, Q & R] -> True.
Proof.
move=> [HP HQ HR].
by [].
Qed.

Lemma as_concl (HP: P) (HQ: Q) (HR: R): [/\ P, Q & R].
Proof.
split.
- by exact HP.
- by exact HQ.
- by exact HR.
Qed.

End Examples.
``````

#### Ricardo (Feb 23 2023 at 21:00):

OK. I see. That's how I thought it'd work. However, I have something like this and it isn't working.

``````Variables (a b c : bool).
Definition p : bool := [&& a, b & c].
Definition P : Prop := [/\ a, b & c].
Lemma pP : reflect P p.
Proof. apply: (iffP and3P) => [Ha Hb Hc].
``````

I get the error `Incorrect number of goals (expected 2 tactics, was given 1).`

Now I see that if I split that line into `apply: (iffP and3P). move=> [HA HB HC].` it works. Any reason for that?

#### Ricardo (Feb 23 2023 at 21:01):

This also works `apply: (iffP and3P) => -[H1 H2 H3].`

#### Julien Puydt (Feb 23 2023 at 21:11):

Ah, I have also situations where for some reasons I can't chain an apply and a move and need several lines -- no clue why either.

But I don't know about the minus trick in the move yet... what does it do?

#### Laurent Théry (Feb 23 2023 at 21:22):

it is because `apply: foo => [_]` is a way to enforce the fact that `foo` generates one single goal.

#### Laurent Théry (Feb 23 2023 at 21:22):

in your case you could write

``````Variables (a b c : bool).
Definition p : bool := [&& a, b & c].
Definition P : Prop := [/\ a, b & c].
Lemma pP : reflect P p.
Proof. apply: (iffP and3P) => [] [Ha Hb Hc].
``````

#### Laurent Théry (Feb 23 2023 at 21:26):

but of course a better proof is :

``````Lemma pP : reflect P p.
Proof. exact: and3P. Qed.
``````
``````
``````

#### Ricardo (Feb 23 2023 at 21:29):

Julien Puydt said:

But I don't know about the minus trick in the move yet... what does it do?

The minus is a no-op in intro patterns. I just read about it. It's somehow useful when, for instance, a view generates several subgoals it seems.

#### Ricardo (Feb 23 2023 at 21:32):

Laurent Théry said:

but of course a better proof is :

``````Lemma pP : reflect P p.
Proof. exact: and3P. Qed.
``````

Yes, in this example `exact: and3P` is enough. In the code I'm working on I need to apply further views to each conjunt.

#### Ricardo (Feb 23 2023 at 21:32):

That's why I'm missing an `and3PP` in ssrbool.

#### Ricardo (Feb 23 2023 at 21:34):

Which I'm trying to prove now.

``````Lemma and3PP (P1 P2 P3 : Prop) (b1 b2 b3 : bool) :
reflect P1 b1 ->
reflect P2 b2 ->
reflect P3 b3 ->
reflect [/\ P1, P2 & P3] [&& b1, b2 & b3].
``````

#### Laurent Théry (Feb 23 2023 at 21:39):

ok now I understand :wink:

``````by move=> rP1 rP2 rP3; apply: (iffP and3P) => [] [/rP1 ? /rP2 ? /rP3].
``````

#### Paolo Giarrusso (Feb 23 2023 at 22:24):

Re the minus: by default, => [ ] only destructs an hypothesis after move/elim, for other tactics you need the minus for that effect; this is intentional (and documented somewhere in the coq reference manual, ssreflect chapter)

Last updated: Jul 25 2024 at 15:02 UTC