Stream: Elpi users & devs

Topic: Preprocessing before itauto

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?

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.

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

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?

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?

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.

Karl Palmskog (Nov 15 2022 at 10:42):

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

Last updated: Oct 13 2024 at 01:02 UTC