Stream: Coq devs & plugin devs

Topic: exact_no_check, repeated casts in proof terms


view this post on Zulip Janno (Oct 28 2021 at 10:44):

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)?

view this post on Zulip Janno (Oct 28 2021 at 10:45):

Oh, this should probably be in the Coq users channel, right? Could somebody move it over?

view this post on Zulip Gaëtan Gilbert (Oct 28 2021 at 10:51):

I don't think so
how do you generate the terms and evars to give to exact_no_check?

view this post on Zulip Janno (Oct 28 2021 at 10:54):

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.

view this post on Zulip Janno (Oct 28 2021 at 10:55):

The non-evar arguments are also all generated unsafely. The usual pattern for this is make (App constr:(@head_term) (array_of_list [...])).

view this post on Zulip Janno (Oct 28 2021 at 10:57):

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.

view this post on Zulip Janno (Oct 28 2021 at 10:59):

(It's probably called evar context, not evar instance, is it?)

view this post on Zulip Gaëtan Gilbert (Oct 28 2021 at 11:02):

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.

view this post on Zulip Janno (Oct 28 2021 at 11:03):

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.

view this post on Zulip Janno (Oct 28 2021 at 11:09):

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..)

view this post on Zulip Janno (Oct 28 2021 at 11:12):

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.

view this post on Zulip Janno (Oct 28 2021 at 11:15):

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!

view this post on Zulip Janno (Oct 28 2021 at 11:24):

On a related note: is it expected that unfold f and simpl f leave casts even when f does not appear in the goal?

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 00:11):

do you need once try progress unfold f :frown: etc to avoid the casts, and would it even work?

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 00:13):

(where once is my non-working attempt to prevent exponential backtracking if some later tactic fails after N try steps?)

view this post on Zulip Gaëtan Gilbert (Oct 29 2021 at 08:11):

why is it non-working?

view this post on Zulip Janno (Oct 29 2021 at 09:24):

I assumed once wasn't necessary. Does try progress unfold f have multiple successes?

view this post on Zulip Paolo Giarrusso (Oct 29 2021 at 19:27):

I was probably just sleepy and wondering about non-existent problems. Next time I should trust Coq more.

view this post on Zulip Jason Gross (Nov 01 2021 at 15:44):

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?

view this post on Zulip Gaëtan Gilbert (Nov 01 2021 at 16:40):

we can try this https://github.com/coq/coq/pull/15104


Last updated: Feb 06 2023 at 19:03 UTC