The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I suspect this is a bug in Coq, and probably worth reporting.  Note that if you replace `Lemma lem_iffT_P` with `Polymorphic Lemma lem_iffT_P` (similarly for your `_T` version), then the rewrites go through fine.  So there is some sort of universe issue, but I don't see why the polymorphic status of the lemma should matter, which is why I suspect this is a bug.

On Wed, Oct 30, 2019 at 2:35 AM Caitlin D'Abrera <Caitlin.Dabrera AT anu.edu.au> wrote:

Hi all,

I'm trying to rewrite using iffT in hypotheses. Rewriting in the conclusion works as well as in the context of an arbitrary Proper P. But I can't see why the rewrites in lem_iffT_P and lem_iffT below Fail. Any ideas on how to make these rewrites work?

Thanks in advance,

Caitlin

--------------------------------------------------------

Require Import Setoid.

Require Import Coq.Classes.CRelationClasses.

Require Import Coq.Classes.CMorphisms.

Parameter B C : Type.

Parameter P : Type -> Type -> Type.

(* This is used for rewrites for lem_P and lem_P_iffT. *)

Instance P_Proper : Proper (iffT ==> iffT ==> iffT) (P).

Admitted.

Lemma lem_P : forall A, iffT A B -> P A C -> P B C.

Proof.

  intros A H1 H2.

  rewrite H1 in H2. (* Comment out iffT_P_Proper to see this fail. *)

Abort.

Lemma lem_P_iffT : forall A, iffT A B -> P A C -> iffT B C.

Proof.

  intros A H1 H2.

  setoid_rewrite H1 in H2.  (* Comment out iffT_P_Proper to see this fail. *)

Abort.

(* Trying to do the same with iffT instead of P. *)

Instance iffT_Proper : Proper (iffT ==> iffT ==> iffT) iffT.

Admitted.

(* Just in case? *)

Instance arrow_Proper  : Proper (iffT ==> iffT ==> iffT ) (arrow).

Admitted.

Lemma lem_iffT_P : forall A, iffT A B -> iffT A C -> P B C.

Proof.

  intros A H1 H2.  

  Fail rewrite H1 in H2.

Abort.

Lemma lem_iffT : forall A, iffT A B -> iffT A C -> iffT B C.

Proof.

  intros A H1 H2.

  Fail setoid_rewrite H1 in H2.

Abort.