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

@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 `firstorder`

, right?

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.

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

Last updated: Feb 04 2023 at 02:03 UTC