Say I have a tactic `normalize`

which proves `a = ?x`

where `x`

is a normalization of `a`

(e.g. how `ring`

would prove `2a - a = a`

). How could I use ltac to use this to normalize all subterms (of the proper type) of my goal?

In pseudoltac I think it would look something like

```
repeat match goal with
| _ |- context[ ?a : A ] => progress (setoid_)replace a with (normalized a)
end.
```

but I'm unsure how to make it work.

I don't know how to do this in ltac, but for ring we have ring_simplify which should do what you want for ring

Though I am actually unable to do what you want with it

Yes I also realized that ring_simplify does exactly what I want (over rings), but I need it for a different 'simplifier' (`aac_normalise`

from AAC Tactics)

If you can easily generate the equalities, then using `rewrite`

might be suitable?

That can match on subterms easily

https://coq.inria.fr/refman/proofs/writing-proofs/rewriting.html?highlight=rewrite#coq:tacn.rewrite

I agree, but generating the equalities is the problem; I want ltac to figure these out (by normalization)

You can do something like this:

```
Require Import ZArith.
Open Scope Z_scope.
Goal forall a b c:Z,
(a + b + c) ^ 2 =
a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
intros.
eassert (H : (a + b + c) ^ 2 = _) by (ring_simplify; reflexivity).
rewrite H.
```

Now you just need to find the subterms that you want to simplify

That part I am not sure how to do

This should also work for aac_normalise from looking at the doc but I haven't tried it

Though maybe @Karl Palmskog knows about it since he is a maintainer

I think the question here is about Ltac. AAC_tactics does almost all the work at the OCaml level (using type class information)

Hmm well you can match on `abstract [P ?a ?b]`

for whatever connective `P`

and have a few cases like this. I am not sure how to enforce what the type of `?a`

and `?b`

are however.

For instance, in the integers, I might look at sub expressions of `+`

`*`

`-`

etc.

Then when you have the term you want to normalize you can do the `eassert`

like I did above and rewrite with it.

Thanks @Ali Caglayan , I got it to work using `eassert`

(though I'm afraid my implementation checks all subterms at the moment, I guess adding a check for operators as you mentioned would help if speed becomes an issue)

I think this is best achieved by writing a tactic which goes recursively through the term and returns an equality between the original term and the normalized term. The main obstacle for this in Ltac1 are the heuristics which decide if a tactic returns a term or a tactic. In Ltac2 this is easier to do. Note that in term matches the head symbol can be a variable, so typically you need only a few cases in a match (depending on what Gallina constructs you want to dig into or leave untouched).

Benjamin Salling Hvass has marked this topic as resolved.

Last updated: Jun 23 2024 at 23:01 UTC