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