Comments (11)
It is still the case that localize/unlocalize is not very robust, in the following sense. The way these tactics are used is,
localize [c]. (* where c is an mpred *)
forward. (* forward symbolic execution for one or more statements, perhaps with other proofs mixed in *)
unlocalize [d]. (* where d is an mpred *)
(* now prove an entailment involving c and d *)
The problem is that if there are hypotheses above the line before the localize
, that are needed in the entailment proof below the unlocalize
; and if the forward symbolic execution proof does something with evars in a way that entangles things, then those hypotheses cannot be used where they are needed.
P.R. #757 patches things back to the status quo up to Coq 8.16. That is, a certain forward symbolic execution using load_tac
had previously not entangled the evars; a change to the semantics of auto
in Coq 8.17 now invoked a different lemma that caused entanglement; the patch prevents that in limited cases, so that several existing proofs in the CertiGraph project continue to work.
But it's not a very general solution. localize\unlocalize is still fragile, because the forward-symbolic-execution proof between them might entangle the evars.
from vst.
The former, it turns out, entangles all open existential variables with the current proof goal,
What does this mean?
Maybe you want to clear all hypotheses that contain evars before running auto
?
from vst.
I don't know what it means. I find all of this very mysterious. But I don't think your proposal would work. The solution I have adopted is to ensure, whenever possible, that the foward symbolic execution between localize and unlocalize does not instantiate any evars. In the limited situations where localize/unlocalize is used, this is typically just one or two forward statements that load from a record field.
from vst.
I mean, auto
should always either do nothing or solve the current goal. So it is safe to replace auto
with try solve [ auto ]
. Now we can write a tactic clear_evars := repeat match goal with H : ?T |- _ => has_evar T; tryif clear dependent H then idtac else fail 1 (* if we can't clear all evar-containing hypotheses then we better not keep going, because we might mess up dependencies *) end
. Then it should be fine to replace try solve [ auto ]
with try solve [ progress clear_evars; auto | auto ]
; either we solve the goal after clearing evar-containing hypotheses, or we (probably) fail to solve the goal. This may be a bit slower, maybe we want to just do try solve [ clear_evars; auto ]
, and see if that works. Alternatively, we can do something like generalize over all evars, I can write that code for you if you want to see it, and it would probably work even better than clear_evars
.
This is all running on the assumption that auto
is the problematic tactic; is this assumption correct?
from vst.
The problem is that auto
is now (in Coq 8.17) succeeding with a lemma from the hint database, because auto is a bit more powerful. Previously, in Coq 8.16, auto
did not match as fully as simple apply
, but now it does, IIRC. And the lemma that gets thereby applied is the one that causes the problem. I could solve the same goal with a different lemma (eq_refl) and there is no interference with evars.
from vst.
What is the goal and context such that applying the lemma messes with evars? (Does the goal have evars? Is it using an assumption that has evars? Something else?)
And regardless, what if you used something like
Ltac set_evar ev := let e := fresh "e" in set (e := ev) in *.
(* Alternative if above is too slow *)
(*
Ltac set_evar ev :=
let e := fresh "e" in
pose ev as e;
change ev with e;
repeat match goal with
| [ H : context[ev] |- _ ] => progress change ev with e in H
| [ H := context[ev] |- _ ] => progress change ev with e in (value of H)
end.
*)
Ltac set_evars_in T :=
repeat match T with
| context[?e] => is_evar e; set_evar e
end.
Ltac set_evars :=
match goal with |- ?G => has_evar G; set_evars_in G end;
repeat match goal with
| [ H : ?T |- _ ] => has_evar T; set_evars_in T
| [ H := ?T |- _ ]
=> tryif is_evar T
then fail
else (has_evar T; set_evars_in T)
end.
Ltac generalize_evars :=
set_evars;
repeat match goal with
| [ H := ?e |- _ ] => is_evar e; clearbody H
end.
and then replaced auto
with try solve [ generalize_evars; auto ]
. This should preserve behavior on all goals that can be solved without unifying evars, and should refuse to unify evars otherwise.
from vst.
If you are super interested in this, I can spend an hour and produce instructions for reproducing this so you can see exactly where simple apply TT_right
seems to entangle some evars in a way that apply derives_refl
does not, with the proof goal, TT |-- !!True
. Or maybe you can look at the type of TT_right in VST to guess more about what may be happening. But really, I'm willing to drop this, because localize/unlocalize is not super-important right now.
from vst.
I think I don't have time to dig into it much more than I have, so we should just drop it if the Ltac I gave above for try solve [ generalize_evars; auto ]
does not work.
For future reference, I ended up porting this to Ltac2, though, and will leave the Ltac2 code here
From Ltac2 Require Import Ltac2.
Ltac2 set_evars_in (t : constr) :=
repeat (match! t with
| context[?e] => if Constr.is_evar e then set $e in * else Control.backtrack_tactic_failure "not evar"
end).
Ltac2 set_evars () :=
set_evars_in (Control.goal ());
List.iter
(fun (_, body, typ)
=> match body with
| Some body => if Constr.is_evar body then () else set_evars_in body
| None => ()
end;
set_evars_in typ)
(List.rev (Control.hyps ())). (* reverse hyps so that we deal with leaf evars before dealing with their dependencies *)
Ltac2 clearbody_evars () :=
Std.clearbody
(List.map
(fun (h, _, _) => h)
(List.filter
(fun (h, body, _)
=> Option.map_default Constr.is_evar false body)
(Control.hyps ()))).
Ltac2 generalize_evars () := set_evars (); clearbody_evars ().
(but it's a bit less robust than the Ltac1, I think)
from vst.
Thank you for the suggestion. The problem will be, I think, that it's not just a single call to auto
that's the problem. The entire forward symbolic execution between the localize and the unlocalize would have to be protected this way; it could include multiple user calls to forward, entailer!, and other tactics. It's only a lucky accident that, in many typical cases, this symbolic execution has comprised only a single forward
statement that has not been too complicated.
from vst.
It's possible that doing set_evars
at the beginning of localize
and calling
Ltac subst_evars :=
repeat match goal with H := ?e |- _ => is_evar e; subst H end.
at unlocalize
would perform decently. Many tactics are less willing to mangle evars that are hidden behind a context variable. And unlike the generalize_evars
solution, this one does not lose any information and so can be used even when we're not about to finish a goal.
from vst.
Remark 1
I adjusted the suggestion of @JasonGross to fix a bug and improve its features, as follows (but then see remark 2...)
Definition protect_evar {A} (x: A) := x.
Ltac set_evar_in T :=
match T with context [?ev] =>
is_evar ev;
let e := fresh "e" in
pose (e:= protect_evar ev);
change ev with e;
repeat match goal with
| [ H : context[ev] |- _ ] => progress change ev with e in H
| [ H := context[ev] |- _ ] => progress change ev with e in (value of H)
end
end.
Ltac set_evars :=
repeat match goal with |- ?G => set_evar_in G end;
repeat match goal with
| [ H : ?T |- _ ] => set_evar_in T
| [ H := ?T |- _ ]
=> tryif is_evar T then fail else
lazymatch T with
| protect_evar _ => fail
| _ => set_evar_in T
end
end.
Ltac subst_evars :=
repeat match goal with H := protect_evar ?e |- _ => red in H; subst H end.
Ltac localize R_L :=
set_evars; old_localize R_L.
Tactic Notation "unlocalize" constr(R_G2) :=
subst_evars; unlocalize_plain R_G2.
Remark 2.
It probably isn't necessary to search for all evars and protect them. There's one evar in particular that we care about, then one introduced by the eexists
in the localize
tactic. It seems to be fine just to protect that one. Easy, and fast. That's what I've done in P.R. #758. Instead of eexists
, create a protected evar w := protect_evar (?ww)
, and then do exists w
.
from vst.
Related Issues (20)
- Please create a tag for Coq 8.18 in Coq Platform 2023.10 HOT 5
- Some observations on `forward_call` performance HOT 21
- Useful lemma for users: nonempty_writable_glb
- do {S} while (0)
- Unnecessary premise in `Lemma field_at_app`
- fail levels in forward_if'_new
- overbroad match in try_conjuncts
- Function pointer comparison apparently not supported
- solve_load_rule_evaluation @proj_reptype HOT 3
- data_at_int_or_ptr_int share
- forward_call takes a long time HOT 2
- Improvements in deadvars
- solve_store_rule_evaluation HOT 1
- Please create a tag for Coq 8.19 in Coq Platform 2024.01 HOT 4
- inhabited_value doesn't really work well
- mkVSU external function check does not give useful error message HOT 3
- cstring should not need a compspecs argument HOT 2
- verif_incr should prove that it restores an uninitialized counter HOT 1
- IPM proof fails in lib/proof body_release, succeeds in atomics body_release HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from vst.