Stream: Coq users

Topic: ✔ Normalize all subterms


view this post on Zulip Benjamin Salling Hvass (Oct 07 2021 at 10:55):

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.

view this post on Zulip Ali Caglayan (Oct 07 2021 at 11:17):

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

view this post on Zulip Ali Caglayan (Oct 07 2021 at 11:22):

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

view this post on Zulip Benjamin Salling Hvass (Oct 07 2021 at 11:54):

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)

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:01):

If you can easily generate the equalities, then using rewrite might be suitable?

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:01):

That can match on subterms easily

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:02):

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

view this post on Zulip Benjamin Salling Hvass (Oct 07 2021 at 12:04):

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

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:09):

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.

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:09):

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

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:10):

That part I am not sure how to do

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:12):

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

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:12):

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

view this post on Zulip Karl Palmskog (Oct 07 2021 at 12:14):

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

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:31):

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.

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:32):

For instance, in the integers, I might look at sub expressions of + * - etc.

view this post on Zulip Ali Caglayan (Oct 07 2021 at 12:32):

Then when you have the term you want to normalize you can do the eassert like I did above and rewrite with it.

view this post on Zulip Benjamin Salling Hvass (Oct 07 2021 at 13:22):

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)

view this post on Zulip Michael Soegtrop (Oct 07 2021 at 13:24):

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

view this post on Zulip Notification Bot (Oct 08 2021 at 10:09):

Benjamin Salling Hvass has marked this topic as resolved.


Last updated: Sep 23 2023 at 07:01 UTC