Is there an intro pattern for `and3`

? Or how is `and3`

usually used?

Also, it'd be great to have `and3PP`

in ssrbool.

This should answer:

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

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

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?

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

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?

it is because `apply: foo => [_]`

is a way to enforce the fact that `foo`

generates one single goal.

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

but of course a better proof is :

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

```
```

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.

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.

That's why I'm missing an `and3PP`

in ssrbool.

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

ok now I understand :wink:

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

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