Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Rewrites using iffT

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewrites using iffT


Chronological Thread 
  • From: Caitlin D'Abrera <Caitlin.Dabrera AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Rewrites using iffT
  • Date: Thu, 31 Oct 2019 04:26:16 +0000
  • Accept-language: en-AU, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=5F2uVxdsQAzSu7USihd2jpGcP7hR/RusMmACjMikpHg=; b=A4b4ENp7qr2c6Rwoad00N6oAhy0kw/qOxHIfQVkpXk3BiGF33gyZhDIaPww71gkQvyBXNbd1fRTRj/xME5/esi+YtNhXsAWHKngRkNULin14/EAzdKjM8TyyxhElwI6HyU7a4JgIofwsrIFSSGjB+rdFS9Jo3KGn/XeYFTZ97dpmkZDzr9E25wn9lkIiiQ82q3scez9NiIPcMNWXZ3SM5zd3lwjv7Jz7SwkzQ3T/0mKindH3dGgy/Z0+k5dYqUbFopkHLeSKrh55ACx6Ml9FMq+gCz1jQQYVU/mjxSfYMwoYAk+yNFYTkNNIrnfaYe5fA1ETGJYP2+mMsY9orbN5WA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Pc65LfUN9hJSCmLdqp7M4Nutn/ruGUqlq1bZMR8GvPGKG/euwvXG3a6KVB8JNGRfy/Mm/4uY/57B/n4vhGxzM+/cKwMwgsc+YcG7Mu9XQRgpTpyt/NKdSSJLGnNkvJR3LbOO7JbwdJQMI1lNZO5kPyU3Wr+J5vcPeh2sYn8qcx0pZt0XC+o3MfPveoAKWzqCVCGrnxnrCnKR2mG3ysO2HsIZN6QwFd3LhbP1iBGT9aphgZN7MqT+FhCnIdRXo/tgUrWr8Ab/rrueG9JKKF612diNRGmr9L1TwRdeJtmr5zS/FxCP5bgo/zq2eRUJc6ImnG8fINhQZNHARTmb77W5CQ==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Caitlin.Dabrera AT anu.edu.au; spf=Pass smtp.mailfrom=Caitlin.Dabrera AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:T1jEJxH8OTOXW4hoDf49up1GYnF86YWxBRYc798ds5kLTJ7yp8mwAkXT6L1XgUPTWs2DsrQY0rGQ6vi8EjNZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba58IRmssAndqsYbjYRgJ6os1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK/qRJi347aboKbNPR8caPcYdwVSnFMUdxNWyBdGI6wc5cDA/QHMO1Fr4f9vVwOrR6mCASyHuzvyyNIhnv33a08zu8vHwLK0RA7ENIUrnvUts/6P7oVXO2r1qbIzCnDb/dX2Tf78oTGfAouruqWXb1ua8re01IiGBnDjlWNs4DqIS6a1vkXv2eB8uptTOSigHMkpQFpujWiydsghpPUio4JyF3I7zh1zYg0KNGiVUJ3f9CpHINNuyyaK4d6WN0uT31mtSog1LEKpIO3cDIXxJknyRPTc/KHfJaL7x7/UeucJCt3iG5+d72ighu96lWsxfHhWcSx0VtHqitIn93Ju38X0xHe6ceKR/1g9Um7wzmPzRrc6uRcLEA0i6XbL5khz6Ysm5UdrErPAjL6lFzxgqGZa0ko4++o5P/5bbn8oZ+cKpN0hRr5MqQznMywHP40MhAUX2ic5eSzyqHs/VH4QLVNiP06iK7ZsI3GJcQfoa65BAxV3pw/5Ba4CjeqyNUYnX8ZI1JZYB+KgJTlN0vTLPzkD/qzmUmgnTlqyvzcI7HtHJvAImDGkLj7fLZ970BcyBA0zdBa/59ZFKsOIPPvWk/1tdzYCAU1PQKuzOn8EtVyyJkeVniUD6CDNqPSrEWE6fwyLOmRfoMaoiv9J+A/5/HylX85hUMdfa6x0JQLb3C4B+1qLFmdYXrxmdgMCnwKvwo7TOzyklKOSz9TZ3CoX6I9/D43EoymDZ2QDryq1faK2z7+FZlLbEhHDEqNGDHmbc/MD/wLcWeZJtJruj0CT7moDYE7g0KArgj/npFuL/bQ+ytQmd3K3sJ4/eSbwTo79CBwDsLb/2iHVWxul0sBQSJw0axi50VgnATQmZNkiuBVQIQAr8hCVR03YMaFk75KTuvqUweERe+nDU68S4z8Uzg3U5Q8z8JIalsvQ4zz3CCG5DKjBvour5LOAZU19qzG2H2ofZR0zWuA2aU8yVA7EJIWaD+Ww5Vn/g2WPLbn1kWUk6H2KvY14RWVrSKm4DPLu0tVFgltTa/CQHYTIFPMqsj07V/DSLnoDqk7NgxGyoiJLa4YM9A=
Thanks, Jason. Yes, that's strange. I'll report it.

Cheers,
Caitlin
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jason Gross <jasongross9 AT gmail.com>
Sent: Wednesday, 30 October 2019 6:13 PM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Rewrites using iffT
 
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.


Archive powered by MHonArc 2.6.18.

Top of Page