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: Oct 13 2024 at 01:02 UTC