itauto unfolds definitions

While trying out itauto lia on bedrock2, I ran into a case where it kept eating more and more RAM until I killed coqc at 5GB of RAM usage. I haven't managed to isolate the RAM consumption issue yet (I suspect it requires dependent types that depend on large nat constants), but here's a simpler example that already exhibits some undesired behavior:

Require Import ZArith List.
Require Import Cdcl.Itauto.

Fixpoint compile(program: nat): list Z :=
  match program with
  | S n => Z.of_nat n :: compile n
  | O => nil
  end.

Axiom F: list Z -> list Z.

Goal F (compile 1000) = compile 1000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 0.206 secs *)
Goal F (compile 2000) = compile 2000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 0.754 secs *)
Goal F (compile 3000) = compile 3000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 1.678 secs *)
Goal F (compile 4000) = compile 4000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 2.987 secs *)


Axiom opaque_compile: nat -> list Z.

Goal F (opaque_compile 1000) = opaque_compile 1000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 0.016 secs *)
Goal F (opaque_compile 2000) = opaque_compile 2000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 0.029 secs *)
Goal F (opaque_compile 3000) = opaque_compile 3000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 0.042 secs *)
Goal F (opaque_compile 4000) = opaque_compile 4000 -> 0 = 0.
Proof. intros. Time itauto reflexivity. Qed.   (* 0.055 secs *)

These timing numbers suggest that itauto reflexivity does something like unfolding the definition of compile.

In my experience, any tactic that tries to be smart and unfolds definitions in a way not controllable by the user will eventually become unusably slow.

Of course, sometimes some smart but uncontrollable unfolding is useful, but I'd say that this only works on very small goals, and firstorder lia or firstorder congruence already does that.

Therefore, I wonder if itauto could guarantee its users that it never unfolds anything?

Here's another instance of probably the same problem (taken from https://github.com/coq/coq/issues/10158):

Require Import ZArith_base.
Require Import Coq.micromega.Lia.
Require Import Cdcl.Itauto.

Open Scope Z_scope.

Fixpoint fib (n: nat) : Z :=
  match n with
  | O => 1
  | S O => 1
  | S (S n as p) => fib p + fib n
  end.

Axiom fib_47_computed: fib 47 = 2971215073.

Lemma fib_bound:
  fib 47 < 2 ^ 32.
Proof.
  pose proof fib_47_computed.
  (* Time lia. 0.002 secs *)
  itauto lia. (* takes forever *)

Note that lia solves this goal immediately, so it seems that itauto is the problem.

mentioned in issue #4

I think the culprit is vm_compute together with the reification. The reification embeds too much of the goal: there are maps containing propositions and proof terms that are reduced by vm_compute.

I hope the solution is to generalize the (atomic) propositions before reifying. lia is actually doing that.

closed with commit 84486bd0

There are two workarounds.

1. 84486bd0 generalises the propositions. Therefore, they should not intervene into the computation

2. The other workaround is to use tauto as backend and set Ltac itauto_use_tauto ::= constr:(true) . In this case, itauto is very close to intuition.