## Stream: math-comp users

### Topic: ✔ Using the under tactic

#### Julien Puydt (Feb 21 2023 at 13:14):

There are a number of situations where I can use the under tactic with reasonable efficiency, but there are others where I'm pretty much drowned, with no clue why it doesn't work.

Here is a small script where I put different simple examples :

``````From mathcomp Require Import all_ssreflect.
From mathcomp Require Import boolp. (* not_andP is in MC-analysis *)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section EqForall.

Variable P Q R: nat -> Prop.

Lemma ok: forall n, ~(P n /\ Q n).
Proof.
Fail rewrite not_andP. (* it *is* a subterm, but it isn't seen *)
(* sometimes cheating is possible -- but it's inelegant *)
move=> n.
rewrite not_andP.
move: n.
Abort.

Lemma notok: forall n, ~(P n /\ Q n).
Proof.
Fail under eq_forall do rewrite not_andP. (* isn't that what's supposed to work? *)
under eq_forall => n.
Fail rewrite not_andP. (* nice try, but no *)
over.
Abort.

Lemma notok2: forall n, P n -> ~(Q n /\ R n).
Proof.
Fail under eq_forall do rewrite [X in _ -> X]not_andP. (* nope *)
Fail rewrite [X in forall _, _ -> X]not_andP. (* it's a subterm and it's just there! *)
Abort.

Lemma notok3: forall n, ~(P n /\ Q n) -> R n.
Proof.
Fail rewrite [X in forall _, X -> _]not_andP. (* didn't work above, doesn't work here... there is a point I'm missing *)
Abort.

End EqForall.
``````

Can someone shed a light on the matter? Thanks!

#### Laurent Théry (Feb 21 2023 at 13:27):

there is a difference between `(P <-> Q)` and `(P = Q)`, `eq_forall` is for `=`

#### Laurent Théry (Feb 21 2023 at 14:48):

``````Lemma notok: forall n, ~(P n /\ Q n).
Proof.
under eq_forall do rewrite (propext (not_andP _ _)).
``````

#### Julien Puydt (Feb 21 2023 at 20:29):

Excellent, that was what I was lacking ; thanks!

#### Notification Bot (Feb 21 2023 at 20:29):

Julien Puydt has marked this topic as resolved.

Last updated: Jul 25 2024 at 14:01 UTC