Hello all,

I have got a question related to setoid rewriting. I don't know if this is an issue or known/expected behaviour, but wanted to check.

There is helpful support of conditional rewriting by the setoid rewriting mechanism... what I mean by "conditional" is that if I have a lemma `P -> (Q <-> R)`

, I can rewrite Q by R in (almost) any context provided I can prove P (P, Q, R being Props).

Now, in my experience, conditional rewriting doesn't work anymore under binders; it seems however it is working if you change slightly the type of the lemma to force a forall being used rather than a (non-dependent) implication (please see the following example), but it seems somewhat hacky to me...

What are your thoughts?

Thanks

```
Require Export Coq.Setoids.Setoid.
(* Very simple first-order logic theorem (illustrating the issue):
if P is true, then any implication with condition P will be equivalent to the
consequence *)
Theorem test (P Q : Prop) :
P -> ((P -> Q) <-> Q).
Proof.
intros H₁.
split;
intros H₂.
{ apply H₂.
assumption. }
{ intros _.
assumption. }
Qed.
(* An immediate related result is that any implication with condition the
"always-true" predicate is equivalent to the consequence.
This can be proved using setoid rewriting. *)
Theorem test' (P : Prop) :
(True -> P) <-> P.
Proof.
setoid_rewrite test.
{ reflexivity. }
{ constructor. }
Qed.
(* The following theorem should also be (in my opinion) provable thanks to
setoid rewriting (using rewriting under binders), but it fails. *)
Theorem test'_under_binder {T} (PP : T -> Prop) :
(forall x : T, True -> PP x) <-> forall x : T, PP x.
Proof.
Fail (setoid_rewrite test).
Abort.
(* However, a slight modification of the lemma type to force a forall being
used leads to success. *)
Theorem test'_under_binder_working {T} (PP : T -> Prop) :
(forall x : T, True -> PP x) <-> forall x : T, PP x.
Proof.
setoid_rewrite (
@id (forall (P Q : Prop) (H₁ : P), let _ := H₁ in (P -> Q) <-> Q) test
).
{ reflexivity. }
{ (* note, importantly, that there is a new x in scope here, so it works as
expected *)
constructor. }
Qed.
```

If you use `setoid_rewrite (test _ _ _).`

in `test'_under_binder`

the rewrite works. I don't know why, but maybe this already helps :)

conditional rewriting doesn't work anymore under binders

s/conditional//: only setoid_rewrite can go under binders (outside some ssreflect special tactics), allegedly for backward compatibility reasons

For anyone interested: note that the behaviour described in my initial message has been fixed (thanks Coq team!) in https://github.com/coq/coq/pull/14986

Last updated: Jun 24 2024 at 14:01 UTC