The Coq mailing list

[Kiarash Rahmani <rahmank AT purdue.edu>]

Thank you so much, Gregory!

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Gregory Malecha <gmalecha AT cs.harvard.edu>
Sent: Monday, February 22, 2016 12:13 PM
To: Coq Club
Subject: Re: [Coq-Club] Remove a Hypothesis from the context

 

Hello, Kia --

There are a few options here.

1/ You can use the [rename] tactic to rename a hypothesis to another one. So you could do [clear H0. rename H1 into H0. ..] This is a bad solution in general.

2/ You can keep the existing definition (rename it to R') and make a copy of it (call it R) that is extended. Then you can prove that R -> R', for your relation this might look like: forall x y, R x y -> R' x y. Then you can apply that lemma to the hypothesis that you have and then to inversion as before.

In general, it is good practice to avoid automatically generated names but I'm guilty of doing it too.

Good luck.

On Mon, Feb 22, 2016 at 9:05 AM, Kiarash Rahmani <rahmank AT purdue.edu> wrote:

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

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/