I have a QED blow up issue with AAC-tactics. As far as I understand it is in maintenance mode (community maintained), so I wanted to fix it myself. From what I have learned in writing several reflexive tactics, what is needed is a lazy eval in the **type** of `decision_thm`

defined here:

and in Coq:

with a handful of symbols in the delta list (all symbols used in the `eval`

function defined - see:

This eval should make the unification task trivial during both, tactic application and QED time, since then the type of `decision_thm`

should match the goal exactly.

I guess it would take me some time to figure out how to do the lazy eval in the type of the theorem in OCaml, so if someone could just tell me the magic line, I would appreciate it.

P.S.: I know how to introduce symbols from Coq into OCaml, but I would need an example on how such an external symbol is fed into the lazy delta list.

formally, I'm the maintainer of AAC Tactics, but I see the scope of my maintenance work as:

- making sure it works with Coq
`master`

- doing releases compatible with new Coq releases
- ensuring the existing functionality is preserved

Enhancements like the ones Michael is proposing are welcome as PRs and will be merged if they are compatible with the above goals.

not sure I understand, isn't that what the convert_concl does?

ie by_aac_reflexivity does something like `vm_cast (r (eval t) (eval t')); apply (decision_thm ...); vm_compute; reflexivity`

what do you want it to do instead?

@Gaëtan Gilbert : the cast goes wild on the arguments of the relation (see the example I posted i the issue). What I do in all my reflexive tactics is an explicit lazy eval to make the term structurally identical to the goal, so that the unification is trivial. If one unifies arbitrary terms, there is always a chance it goes wild. As far as I can tell an explicit evaluation (with delta list) is not done, which can be seen by the fact that e.g. eval_aux is not declared external, und thus not available at the OCaml level.

@Karl Palmskog : this is perfectly fine. I understand "community maintained" as "if you see a chance to fix an issue as user of a development, at least try it".

You have the goal, why do you need to evaluate something to get it?

The statement of `derives`

is `eval u == eval v`

. Here `u`

and `v`

are reified versions of the original goal and `eval`

converts this reified form back to the original Coq term. The `eval`

function is not trivial, and the unification simply can blow up. So what I tend to do in such cases is to explicitly evaluate the `eval`

function, so that the type of the correctness lemma is identical to the goal, not just unifiable.

See e.g. my Rosetta stone example:

If I leave away this cbv (I would use lazy now), this tactic very easily blows up at QED time. With the cbv it is safe.

(In this case modulo the fact that I evaluate some Z functions, as said in the example to do it properly one would have to copy these. But the AAC tactics look clean in this respect).

that does `cbv in hyp`

, I thought that didn't change the proof term, how does it impact Qed?

I am not so sure what happens if one does the evaluation before the instantiation, but this tactic does work. I need to double check how exactly I do it in production tactics. Possibly one has to do something slightly more contrived, like first generalize / revert the posed theorem, then evaluate in the goal and then introduce it again.

@Gaëtan Gilbert : you are right, the example is bad. In production code I do this (Ltac2):

```
let theorem_id:=fresh_name_not_in_local_hyps @__solve_goal in
let theorem := constr:(ExprProp_check_Implies_ExprProp_interpret $ast $ctx $ctx_proof) in
let theorem_type := Constr.type theorem in
let theorem_type_eval := Std.eval_cbv (redflags_delta_only_all (interpretation_symbols())) theorem_type in
pose ($theorem_id:=$theorem);
let thereom_inst:=constr_of_ident theorem_id in
my_repleace_refl theorem_type theorem_type_eval theorem_id;
apply $thereom_inst;
```

With

```
Ltac2 my_repleace_refl (a : constr) (b : constr) (hyp : ident):=
(* ltac1:( a b id |- replace a with b in id by (idtac "POS1" b; time (abstract reflexivity))) (Ltac1.of_constr a) (Ltac1.of_constr b) (Ltac1.of_ident hyp). *)
ltac1:( a b id |- replace a with b in id by reflexivity) (Ltac1.of_constr a) (Ltac1.of_constr b) (Ltac1.of_ident hyp).
```

(Maybe there is meanwhile a better way of doing this in Ltac2)

Thinking about this, the odd things is that I prove the equivalence of the evaluated proof statement and the unevaluated one also with reflexivity - this should be the same as what happens if I don't do this at all. Possibly the order (what is left and right in unification) matters here.

What I can say is that I had QED problems with my tactic as well and the QED issues are gone with the above code. My tactic works in a very similar way.

I wonder if `pose ($theorem_id:=$theorem:$theorem_type_eval)`

would work ...

@Gaëtan Gilbert : do you have some hints / pointers on how to write the eval and replace from the above Ltac2 code in an OCaml tactic?

OK, I guess it is time to go through Yves' OCaml plugin tutorial then ...

`replace a with b in id by tac`

is `Equality.replace_in_clause_maybe_by a b cl (Some tac)`

where `cl`

is a https://github.com/coq/coq/blob/deaf8493b2bb10de01101423188c655c397a09f2/pretyping/locus.mli#L41-L56 saying `in id`

(something like `{ concl_occs = NoOccurrences; onhyps = Some [(AllOccurrences, id), InHyp] }`

)

since you know the terms involved you could also try to directly generate the terms involved, ie doing something like

```
pose proof (@eq_ind_r _ a ?P id b eq_refl) as id'; clear id; rename id' into id
```

where `?P`

is the generalization of the type of `id`

over `a`

(and you can decide if you prefer to use `@eq_refl _ a`

or `@eq_refl _ b`

)

@Gaëtan Gilbert : thanks for the pointers - just in time!! I meanwhile figured out how to collect the delta list for the eval lazy and got this working. It is a bit tricky because aac-tactics does quite a few let defines in various places and I need to collect these let symbols (and then convert them to the correct type). I am learning ...

I think I meanwhile learned enough about writing Tactics in OCaml to fix AAC tactics. I have one question, though. The original code has these lines (see):

```
let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in
let convert = Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast in
let apply_tac = Tactics.apply decision_thm in
```

Here `t`

and `t'`

are the reified terms. As far as I understand this tries to convert the original (unreified) goal to the uninterpreted reified goal `r (eval t) (eval t')`

- where `r`

is usually `=`

- using a VMcast. The problem is that one needs to (partially) reduce `convert_to`

to get to the goal. Doesn't this try to (fully) reduce the goal to get to `convert_to`

? As far as I can see, this would be quite a disaster and leave a much harder unification task to the `apply`

following next . Of course this depends on the terms on which the AAC operator is applied, but even a `(a+b)%Z`

doesn't look very nice after full evaluation.

It’s unclear what kind of evars could appear here, from the comment above. But I suppose that the conversion `R (eval (quoted_t)) (eval quoted_u)`

to the goal `R t u`

should be cheap

It’s unclear what kind of evars could appear here

most definitions involved have some type class arguments, but I don't see why these should not be instantiated at this point. I am not aware that there are other evars around.

But I suppose that the conversion R (eval (quoted_t)) (eval quoted_u) to the goal R t u should be cheap

Well it is what QED dies on in rather trivial examples. Somehow the unification can get lost in the inner structure of the arguments to the AAC operator. See the issue example which is essentially `x+0=x`

where `+`

is replaced with some VST memory operator and `x`

with a not to complicated VST memory predicate. QED cannot go wild on the premise, because this is fully reduces to Eq = Eq, and there is nothing else in the proof term.

But my main quest is what the `Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast`

does here. Does it a full VM evaluation of the goal? I would think I can find not to complicated examples, where a full evaluation of an equality leads to astronomic (or worse) run times.

convert_concl uses Reductionops.infer_conv (kernel conversion as a evar aware api) regardless of which cast kind it produces

@Gaëtan Gilbert : sorry, but this doesn't help me much - I don't know what `Reductionops.infer_conv`

does exactly either and the documentation mostly mentions universe constraints, which I don't think are a problem here.

I expect that `Tactics.convert_concl ~cast:true ~check:true convert_to Constr.VMcast`

converts the goal to `convert_to`

in some way and leaves some hints for the kernel. I would like to understand how exactly it does the conversion and what hint it leaves for the kernel. There is not that much documentation for the details (or I can't find it). Especially I wonder if the `Constr.VMcast`

means either at tactic execution time or at QED time a VM compute is done, and if so one which term and when.

A vm_compute (or any form of full compute) on anything which involves user supplied terms, would for sure lead to computational blow up in many cases.

IMHO the proper way of doing this is to do a full compute on the `Eq = Eq`

premise of `decision_thm`

and do full reduction but with only the symbols used on the `eval`

function in the delta list on the conclusion of `decision_thm`

and then apply it to the goal.

it does something like `match goal with |- ?g => refine (_ :? g); change ty end`

(where `:?`

is whatever cast kind was given)

so there is vm computation on both sides at Qed but not at tactic time

I would like to understand how exactly it does the conversion

it's the standard `lazy`

based kernel conversion

Thanks - this was clear!

To recap (please correct me when wrong):

- AAC tactics handles AAC operators applied to arbitrary terms
- these arbitrary terms are contained in the original goal and in the evaluated reified terms
- the
`Tactics.convert_concl .... Constr.VMcast`

does a vm compute at QED time on the original goal and the evaluated reified terms - as a result this blows up at QED time if a vm_compute on any of the involved terms blows up

I see, agreed Michael. Isn't there a "safe" way to avoid the conversions of the arbitrary terms using set/pattern and clearbody's? I suppose other reflexive tactics might do that

https://github.com/coq-community/aac-tactics/pull/134

@Matthieu Sozeau : there are a few problems with abstracting the user terms e.g. hiding them behind opaque definitions or, as you suggested, using clearbody in relevant subgoals. One problem is that this is slowish - not really slow but it can easily take longer than the rest of the reflexive tactic. The other problem is that this also depends on the involved operators. Some operators fully reduce to quite a mess even with opaque variables as arguments. Of course one could also abstract the operators ...

As I said, my preferred solution is to use lazy with an explicit delta list which contains only the symbols used in the `eval`

function (or interpretation function as I tend to call it) and this way make the statement of the decision theorem and the goal identical.

Last updated: Oct 13 2024 at 01:02 UTC