Stream: math-comp users

Topic: and3


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

view this post on Zulip Julien Puydt (Feb 23 2023 at 20:46):

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.

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

view this post on Zulip Ricardo (Feb 23 2023 at 21:01):

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

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

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

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

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

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

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

view this post on Zulip Ricardo (Feb 23 2023 at 21:32):

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

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

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

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC