CODEWITHSUNDEEP
coqcoq-tactic
Max Heiber
Max Heiber

Reputation: 15582

How can I rename an existentially quantified variable in a hypothesis?

Is there an easy way to rename an existential variable in a hypothesis? Sometimes the variable names are confusing, because the same names are reused in unrelated hypotheses.

For example, I want to change H1 : exists p : nat, n0 = p * 2 to H1 : exists pminus1 : nat, n0 = pminus1 * 2.

Upvotes: 0

Views: 201

Answers (1)

Yves
Yves

Reputation: 4258

Here is a piece of code that does it:

match goal with
  an_h : @ex _ (?f) |- _ =>
  let new_f := eval lazy beta in (fun pminus_one => f pminus_one) in
  assert (my_h : @ex _ new_f) by exact an_h; clear an_h
end.

Upvotes: 2

Related Questions