Stream: Elpi users & devs

Topic: Preprocessing before itauto


view this post on Zulip Karl Palmskog (Nov 10 2022 at 16:01):

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?

view this post on Zulip Karl Palmskog (Nov 10 2022 at 16:03):

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.

view this post on Zulip Enzo Crance (Nov 15 2022 at 08:58):

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 bool or 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 TT defined by a signature STS_T, and an automation tactic autoT able to syntactically recognise an instance of STS_T, with a standard type T and an implementation of this STS_T interface. If your goal contains another encoding of theory TT, e.g. a type T' and other values to stand for STS_T, 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. T' to T and bool to Prop).

I hope this clarifies the scope of Trakt and to what extent it can fit your needs.

view this post on Zulip Karl Palmskog (Nov 15 2022 at 09:07):

@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?

view this post on Zulip Karl Palmskog (Nov 15 2022 at 09:09):

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 firstorder, right?

view this post on Zulip Enzo Crance (Nov 15 2022 at 10:38):

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. intros and split behaviour can probably not be simulated.

view this post on Zulip Karl Palmskog (Nov 15 2022 at 10:42):

I see. I guess we'll try sauto then. Thanks.


Last updated: Feb 04 2023 at 02:03 UTC