Stream: Coq users

Topic: Rewriting Type in Proof State

Julia Dijkstra (Dec 16 2023 at 18:23):

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?

Julia Dijkstra (Dec 16 2023 at 18:24):

In particular I would like to see

``````pf1, pf2 : True
``````

Quentin VERMANDE (Dec 16 2023 at 18:28):

You can try `rewrite G2 in pf1, pf2`.

Julia Dijkstra (Dec 16 2023 at 18:29):

I then get the following message:

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

Quentin VERMANDE (Dec 16 2023 at 18:32):

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

Julia Dijkstra (Dec 16 2023 at 18:32):

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

Gaëtan Gilbert (Dec 16 2023 at 18:47):

try `symmetry G2; destruct G2`

Olivier Laurent (Dec 16 2023 at 18:50):

`subst P` or `subst` seems to work as well.

Julia Dijkstra (Dec 16 2023 at 18:54):

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?

Johannes Hostert (Dec 16 2023 at 20:05):

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.

Pierre Rousselin (Dec 16 2023 at 21:21):

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.

Gaëtan Gilbert (Dec 16 2023 at 22:41):

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

Pierre Rousselin (Dec 17 2023 at 06:24):

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.

Julio Di Egidio (Dec 17 2023 at 10:27):

I too have it with `subst`.

Last updated: Jun 23 2024 at 04:03 UTC