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 exact_no_check
.
(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?
I assumed 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.
I think unfold
and 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: Oct 13 2024 at 01:02 UTC