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!

there is a difference between `(P <-> Q)`

and `(P = Q)`

, `eq_forall`

is for `=`

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

Excellent, that was what I was lacking ; thanks!

Julien Puydt has marked this topic as resolved.

Last updated: Jul 25 2024 at 14:01 UTC