Stream: Coq users

Topic: Rewriting Type in Proof State


view this post on Zulip 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?

view this post on Zulip Julia Dijkstra (Dec 16 2023 at 18:24):

In particular I would like to see

pf1, pf2 : True

view this post on Zulip Quentin VERMANDE (Dec 16 2023 at 18:28):

You can try rewrite G2 in pf1, pf2.

view this post on Zulip Julia Dijkstra (Dec 16 2023 at 18:29):

I then get the following message:

Cannot change pf1, it is used in conclusion.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 16 2023 at 18:47):

try symmetry G2; destruct G2

view this post on Zulip Gaëtan Gilbert (Dec 16 2023 at 18:47):

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

view this post on Zulip Gaëtan Gilbert (Dec 16 2023 at 18:47):

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

view this post on Zulip Olivier Laurent (Dec 16 2023 at 18:50):

subst P or subst seems to work as well.

view this post on Zulip 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?

view this post on Zulip 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 destructs the equality, which allow you to replace all occurrences at once so that there are no intermediate ill-typed terms.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Julio Di Egidio (Dec 17 2023 at 10:27):

I too have it with subst.


Last updated: Jun 23 2024 at 04:03 UTC