I've been planning to set up some experiment to figure out if
firstorder can be replaced in one of our projects, and with what. One idea is to switch to sauto from CoqHammer (powerful, but likely not an easy change). Another idea is to check whether we can just do some preprocessing of goals before handing them to itauto, which we already use.
@Enzo Crance do you have any intuition about feasibility of doing "first order preprocessing" with Trakt before handing goals to a SAT solver like itauto? Could it work for at least a subset of typical
firstorder calls do you think?
to make the question more concrete, here is a goal that falls outside the scope of
itauto (discussion here), but could be solved by it after preprocessing:
Require Import Cdcl.Itauto. Require Import List. Goal forall A (s1 s2 s : list A), (forall x : A, In x s1 \/ In x s2 -> In x s) <-> (forall x : A, In x s1 -> In x s) /\ (forall x : A, In x s2 -> In x s). Proof. Fail itauto auto. intuition auto. Qed.
Hello. (sorry for the delay)
I am not sure about the kind of preprocessing you want on this goal. Can you be more precise?
Trakt could help you if your automation tactic requires logical preprocessing, i.e. it only processes
Prop, your goal expresses predicates in both or the "wrong" one, and you want to rewrite everything in the target logical type.
(e.g. preprocessing such as switching between these two goals:)
Goal forall (x : Z), odd x \/ even x. Goal forall (x : Z), oddb x || evenb x = true.
Trakt could also help you in the case of theory-based preprocessing. For instance, let's consider a theory defined by a signature , and an automation tactic
autoT able to syntactically recognise an instance of , with a standard type
T and an implementation of this interface. If your goal contains another encoding of theory , e.g. a type
T' and other values to stand for , if you are able to show that the second encoding can be embedded into the first (and standard one for
autoT), then Trakt can do the preprocessing for you and turn your goal into one that
autoT can prove automatically.
The tool is also able to do a combination of both kinds of preprocessing (e.g.
I hope this clarifies the scope of Trakt and to what extent it can fit your needs.
@Enzo Crance OK, let me try to be super precise. Recall that
itauto is a strict SAT solver, and consider the goal from above again:
Goal forall A (s1 s2 s : list A), (forall x : A, In x s1 \/ In x s2 -> In x s) <-> (forall x : A, In x s1 -> In x s) /\ (forall x : A, In x s2 -> In x s). Proof. Fail itauto auto. (* doesn't work due to itauto being "just" a SAT solver *) split. (* do manual pre-processing, can Trakt do this easily? *) - itauto auto. - itauto auto. Abort. Goal forall A (s1 s2 s : list A), (forall x : A, In x s1 \/ In x s2 -> In x s) <-> (forall x : A, In x s1 -> In x s) /\ (forall x : A, In x s2 -> In x s). Proof. split. - auto. - intros. (* first-order reasoning *) destruct H. (* propositional reasoning *) destruct H0. (* propositional reasoning *) + auto. + auto. Qed.
So for example, could Trakt remove all
<->, introduce all variables like
intros, to set up propositional reasoning?
I'm only asking about
Prop here, no booleans or similar. What I'd like to do is essentially: go through the context and goal, and break apart all Props and introduce variables as much as possible, then apply
itauto on all resulting goals. It should be possible to compare the outcome of this to simply running
In a nutshell, Trakt rewrites subterms but will not change the structure of the goal, except in the case of partial embeddings, which is not the topic here.
split behaviour can probably not be simulated.
I see. I guess we'll try sauto then. Thanks.
Last updated: Feb 04 2023 at 02:03 UTC