Benjamin Salling Hvass (Oct 07 2021 at 10:55): 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.
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
Ali Caglayan (Oct 07 2021 at 11:22):Though I am actually unable to do what you want with it
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)
Ali Caglayan (Oct 07 2021 at 12:01):If you can easily generate the equalities, then using rewrite might be suitable?
Ali Caglayan (Oct 07 2021 at 12:01):That can match on subterms easily
Ali Caglayan (Oct 07 2021 at 12:02):https://coq.inria.fr/refman/proofs/writing-proofs/rewriting.html?highlight=rewrite#coq:tacn.rewrite
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)
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.
Now you just need to find the subterms that you want to simplify
Ali Caglayan (Oct 07 2021 at 12:10):That part I am not sure how to do
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
Ali Caglayan (Oct 07 2021 at 12:12):Though maybe @Karl Palmskog knows about it since he is a maintainer
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)
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.
Ali Caglayan (Oct 07 2021 at 12:32):For instance, in the integers, I might look at sub expressions of + * - etc.
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.
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)
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).
Notification Bot (Oct 08 2021 at 10:09):Benjamin Salling Hvass has marked this topic as resolved.
Last updated: Jan 31 2023 at 12:01 UTC