Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Rewrites using iffT
  • Date: Wed, 30 Oct 2019 04:17:39 +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=HIzyXEeWhuzinE7yBP+KE72rFvvyRydG80JJ8roMu54=; b=hmDJZ1QZiJ2DwHFpMqQsbN2IYIQ1emNtUkFHYs/A2beDDKVI4TaNGVOA1s+VKwhCB/ntfGuJWRlDN9yBmKorOyzQcppwpTxaZHgs9qDDs79XAR6DAQrVJeEARaNiuWtxBkSedPSxxakW7sZy+6UuTvuRClfLIZwEIdJx6Sq9t5vGX1M22SpiMmbPQ97zSfBVodiNTkegMe2sMJl+MvmmeGbSJneUWvqjyPTnWJ8Va3wvlPRPW/x917Mt+yvvh6KxbPyQnz+xCHdMPKN7GfT62vmjgiJwkH4fWtvj6LJnQ9Y/LbdQ0aSi1sNNBxGx+nL+M/4KTM5+Sj1iqiaeutGTdw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Ec3uscKUYcN7iePQPdh6tNWUVx5mLMSq9pd/WYTfiYInYy59LlVIbcmfbWXbqkVQ1I3qIsINvu6xG4sVe2kJ0nd34qeXFG9Uq4TxL1hOAlpsurnbxNOQIyWjOxOCBsVhNYs8IQfdUUqR3/u+sQFp+G2iL9muqqsU5SUa/xP0XlyqKsrJIXILJPihbaHqmtPPYmFXs9ZnPsI4emuiaZ1W7TCvfabInI8BXhxyPOw/p4YfaRtFyHtdaCUGmEjjNy1OBBo+4u+ptsg0yPK3dKnnSvGWMrECclqkLAzU8UCfj91k/oePsk2kgw6ajYKpuSP+/eVZMwcGIW7cc2y1l8/etA==
  • 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:GjATmhf7rBou5bM0G8AFTjHClGMj4u6mDksu8pMizoh2WeGdxcW6ZR7h7PlgxGXEQZ/co6odzbaP6Oa5ATZLv8bJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/MusUKn4duJac8xxjUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vpwJxzZPIYI+bN/R+f7/SctwBSGVbQspdSzZMDp+gY4cSCecKIOZWr5P6p1sLtRazGxOjBOLzyj9Mh3/227Ax3eoiHQzaxwMgBcwBsG7Oo97oM6ofT/q6zKjUzTXHbvNW3y3x5obSfR86u/GDQ6hwftDKxEY1EQPFk0+cppL4MDOIzOgCqXWb4vNmWOmyiGAnsxl8rzezyss2l4XFmoAYxkrZ+Sh3wYs5P8C0RFB0bNK8DZddtz2WO5FoTs8+TWxkojg2xqAbtZKhYSQHyJoqywbRa/OZcIWE/hfuWeONLjtkn31qZbeyiA2v/Ue81+LxU8i53VJLoydBl9TDrHQA2h/c58WBV/Bz5F2u2SyV2ADW8uxEIV47la7cK5M53rM/mIcdvVjeEiPvn0v4g7Kaelwj+uez9evreLLmpoKAN4BvjQH+L6IuldGlDeQgKAgOWHSb9vqg273//E35R7NKgucxkqnErJDaIcMbpqm6AwNPzokj7BO/Ay+n0NQeg3YHMEpIdR2bg4TzJl3CPPL1Ae2ij1mikTpn3e3KMqPuD5nVK3jMirbhfbJz605GzwozyMhS6oxOBbEAPPLzXk7xtNrCAhE3KQO72PznB8tn1owEQm+AGKmZML7IvVCW++0vPvOAa5UIuDrlMfgq++bujWMlmV8aZaSmwZwXaGmhEvt6J0WZfGHjj8waEWYKuwo+VPblhEeDUT5VfXayXrgz6is1CIK8Xs//QdXni7uYmSy/A5d+Z2ZcC1nKH22iP9GPXO5JYyaPKOdglCYFXP6vUdly+wupsVrRwrt7KuvSsgFXnJj52cJ8r7n4nBAu8T1ySeiU2XuAVWhcl2UVATI6weZ2vBoumR+4zaFkjqkARpRo7PRTX1JibM+O/6lBE9n3Hzn5UJKMQVeiTM+hBGhrHNs33pkDb1s7Esjw10mfjRrvOKcckvmwPLJx6rjVhiKjLsBgjXvKye8okgt+G5YdBSidnqd6sjPrKcvJnkGey/n4XJknhHeI0UraiG2EsQdfTRJ6VrjDUTYHfEzKoN/l50TECbizFbAgNQgHwsmHePJH
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