In the following proof state I would like to rewrite pf1 and pf2 to be of type True:

```
H : forall P Q : Prop, P <-> Q -> P = Q
P : Prop
pf1, pf2 : P
G1 : P <-> True -> P = True
G2 : P = True
(1 / 1)
pf1 = pf2
```

This is doable by reverting them and then rewriting the goal. Is there also a way of directly rewriting types in the proof state?

In particular I would like to see

```
pf1, pf2 : True
```

You can try `rewrite G2 in pf1, pf2`

.

I then get the following message:

```
Cannot change pf1, it is used in conclusion.
```

Ah, indeed, changing the type of pf1 would make the goal ill-typed. So I guess the answer is that you can not.

I wonder how this exercise was intended to be solved then, since revert is not mentioned until this point.

try `symmetry G2; destruct G2`

they use destruct in https://github.com/DeepSpec/sfdev/blob/a08306a5af0372f61f9cd827fd74cbc29f396d1c/lf/ProofObjects.v#L1424

(secret repo that you probably don't have access to ;))

`subst P`

or `subst`

seems to work as well.

subst does the trick, I'm guessing it tries to look for an assumption of the form `P=`

and then replaces all occurrences of it in your proof state?

Julia Dijkstra said:

subst does the trick, I'm guessing it tries to look for an assumption of the form

`P=`

and then replaces all occurrences of it in your proof state?

From experience, `subst`

is subtly more powerful then rewriting all occurrences. I suspect it simply `destruct`

s the equality, which allow you to replace all occurrences *at once* so that there are no intermediate ill-typed terms.

Julia Dijkstra said:

I wonder how this exercise was intended to be solved then, since revert is not mentioned until this point.

It indeed looks like `rewrite`

cannot handle this. It's possible to `revert pf1 pf2`

as you mention, but then, maybe it was possible not to `intros pf1 pf2`

in the first place and use `rewrite`

on only the goal? That, or some alternatives to `revert`

like `generalize pf1 pf2`

which maybe have been mentioned before.

the proof of equality is built from pf1 or pf2 so it's not possible to avoid the intros

Gaëtan Gilbert said:

the proof of equality is built from pf1 or pf2 so it's not possible to avoid the intros

Right, I found the exercise in `ProofObject`

(it's a nice part, btw).

`generalize dependent`

is available since at least https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html so I would say it is the way to go.

I too have it with `subst`

.

Last updated: Jun 23 2024 at 04:03 UTC