How to refer a hypothesis in an assert?

Using Rocq
1

Hi,

I would like to know how to reuse a hypothesis in an assert definition.

The hypothesis body is long and copy-pasting it is not efficient, so I tried to refer the required hypothesis by its name, but it turned out a different thing and Rocq prover rejects the same prop when it is referred.

command:

assert (NH: ~ H).

goals:

H: long-prop
============
False

response:

The term "H" has type "..." while it is expected to have type "Prop".
2

it seems like you want the type of the hypothesis, not the hypothesis itself
so “let t := type of H in assert (NH: ~ t)”

Gaëtan Gilbert

2 Likes