This is a bit of a sanity check kind of question: I have a very large Ltac2 tactic that generates proof terms exclusively via
exact_no_check (including generating my own evars for subgoals which are then solved again with
exact_no_check). While inspecting a generated proof term in an example application of the tactic (outside my test suite, sadly) I noticed that sometimes my inner proof terms are wrapped in roughly 25 layers of useless type casts and I cannot figure out how that comes about. Before I take apart my entire tactic I wanted to ask: Does
exact_no_check ever generate casts? If not, can anyone think of anything else that would lead to terms of the form
(((( .... (((( x : t) : t) : t) : t) :t) ... ) : t) : t) : t)?
Oh, this should probably be in the Coq users channel, right? Could somebody move it over?
I don't think so
how do you generate the terms and evars to give to exact_no_check?
The evars are generated via an OCaml function with an Ltac2 wrapper. The function calls
Evarutil.new_evar. The proof term is generated unsafely as a single
App node with lots of non-evar arguments followed by (in this case) one evar.
The non-evar arguments are also all generated unsafely. The usual pattern for this is
make (App constr:(@head_term) (array_of_list [...])).
It might be noteworthy that after generating the evars in OCaml I take them apart in Ltac2 (i.e. split them into the actual evar and the evar instance) so that I can call
Control.new_goal on the evar itself after running
(It's probably called evar context, not evar instance, is it?)
maybe you call reduction a bunch of times? eg
Lemma foo : 1 + 1 = 2. Proof. do 5 simpl; exact_no_check (eq_refl 2). Defined. Set Printing All. Print foo.
Oh! I had completely forgotten that reduction tactics do this. I think there is a step of simplication before the nested proof term is generated. That would explain why it's always 25 layers of casts.
No such luck. There is a tactic that is called on the goal before my tactic runs again but replacing it by
idtac doesn't remove the casts. (I checked that replacing it with
fail actually makes everything fail just to make sure..)
I think I'll have to dig a little deeper. There are other bits that do not correspond to my expectation of what the tactic ought to be doing.
Oh, actually, no need. I was not looking at the right case. The term with casts is not one of my nested proof terms at all; it's a completely new invocation of the tactic and before that we run a tactic with 24 calls to
simpl. Mystery solved! Thank you!
On a related note: is it expected that
unfold f and
simpl f leave casts even when
f does not appear in the goal?
do you need
once try progress unfold f :frown: etc to avoid the casts, and would it even work?
(where once is my non-working attempt to prevent exponential backtracking if some later tactic fails after N try steps?)
why is it non-working?
once wasn't necessary. Does
try progress unfold f have multiple successes?
I was probably just sleepy and wondering about non-existent problems. Next time I should trust Coq more.
simpl both perform beta-reduction globally, even when
f does not appear in the goal, so it's at least not insane to leave casts?
we can try this https://github.com/coq/coq/pull/15104
Last updated: Dec 07 2023 at 09:01 UTC