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: Oct 13 2024 at 01:02 UTC