Stream: Coq users

Topic: setoid_rewrite: conditional rewriting under binder


view this post on Zulip Martin C (May 03 2021 at 10:05):

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.

view this post on Zulip Yannick Forster (May 03 2021 at 10:55):

If you use setoid_rewrite (test _ _ _). in test'_under_binder the rewrite works. I don't know why, but maybe this already helps :)

view this post on Zulip Paolo Giarrusso (May 03 2021 at 22:56):

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

view this post on Zulip Martin C (Dec 03 2021 at 19:58):

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: Jan 31 2023 at 14:03 UTC