coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Remove a Hypothesis from the context

From: Kiarash Rahmani <rahmank AT purdue.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Remove a Hypothesis from the context
Date: Mon, 22 Feb 2016 17:05:04 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rahmank AT purdue.edu; spf=None smtp.mailfrom=rahmank AT purdue.edu; spf=Pass smtp.helo=postmaster AT na01-bn1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:RK/VqxwiwIexPyHXCy+O+j09IxM/srCxBDY+r6Qd0e8fIJqq85mqBkHD//Il1AaPBtWEra8YwLuJ+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU0pj8hr/60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05wj7v/B0wynSB8T2SLkyWHz29a5rTRbuiw8fKiQ17WyRh8Bt2vEI6Cm9rgByltaHKLqeM+BzK/vQ
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:23

Hello all,

This is Kia Rahmani, and I have been using Coq for a couple of months now.

Here is my question:

I have inductively defined a relation R, and later I have used inversion on R, to complete some large proofs.

However, now I need to add another assumption to the context of R, which will be used somewhere else (not in the current proofs); but this will result in an additional hypothesis in all the old proofs as well, and change the numbering of assumptions (H1 H2 H3....). Since the new assumption is not used in the old proofs, is there any way to remove it completely from them?

I know clear would remove a hypothesis, but it does not change the numbering of others back.

Thank you in advance,

Kia

[Coq-Club] Remove a Hypothesis from the context, Kiarash Rahmani, 02/22/2016
- Re: [Coq-Club] Remove a Hypothesis from the context, Gregory Malecha, 02/22/2016
  - Re: [Coq-Club] Remove a Hypothesis from the context, Kiarash Rahmani, 02/22/2016