Exponential blowup with Hint Unfold

[cpitclaudel]

Description of the problem

I'm running into performance issues with Hint Unfold. The following example shows eauto 10 going from 0.01 second to 1 second by adding one Hint Unfold, and to 1 minute by adding another hint:

Fixpoint exp (P: Prop) n :=
  match n with
  | O => P
  | S x => exp P x /\ exp P x
  end.

Create HintDb test discriminated.

Goal exp False 12.
  unfold exp.

  Time eauto 10.

  Hint Unfold plus : test.
  Time eauto 10 with test.

  Hint Unfold minus : test.
  Time eauto 10 with test.

The problem is that the first eauto exits immediately, whereas the second one explores an exponential number of permutations of "unfold plus". Here's part of the output of debug eauto:

Debug: 1 depth=5
Debug: 1.1 depth=4 unfold Nat.sub
Debug: 1.1.1 depth=3 unfold Nat.sub
Debug: 1.1.1.1 depth=2 unfold Nat.sub
Debug: 1.1.1.1.1 depth=1 unfold Nat.sub
Debug: 1.1.1.1.1.1 depth=0 unfold Nat.sub
Debug: 1.1.1.1.1.2 depth=0 unfold Nat.add
Debug: 1.1.1.1.1.3 depth=0 simple apply conj
Debug: 1.1.1.1.2 depth=1 unfold Nat.add
Debug: 1.1.1.1.2.1 depth=0 unfold Nat.sub
Debug: 1.1.1.1.2.2 depth=0 unfold Nat.add
Debug: 1.1.1.1.2.3 depth=0 simple apply conj
Debug: 1.1.1.1.3 depth=1 simple apply conj
Debug: 1.1.1.1.3.1 depth=0 unfold Nat.sub
Debug: 1.1.1.1.3.2 depth=0 unfold Nat.add
Debug: 1.1.1.1.3.3 depth=0 simple apply conj
Debug: 1.1.1.2 depth=2 unfold Nat.add
Debug: 1.1.1.2.1 depth=1 unfold Nat.sub
Debug: 1.1.1.2.1.1 depth=0 unfold Nat.sub
Debug: 1.1.1.2.1.2 depth=0 unfold Nat.add
Debug: 1.1.1.2.1.3 depth=0 simple apply conj
Debug: 1.1.1.2.2 depth=1 unfold Nat.add
Debug: 1.1.1.2.2.1 depth=0 unfold Nat.sub
Debug: 1.1.1.2.2.2 depth=0 unfold Nat.add
Debug: 1.1.1.2.2.3 depth=0 simple apply conj
Debug: 1.1.1.2.3 depth=1 simple apply conj
Debug: 1.1.1.2.3.1 depth=0 unfold Nat.sub
Debug: 1.1.1.2.3.2 depth=0 unfold Nat.add
Debug: 1.1.1.2.3.3 depth=0 simple apply conj
Debug: 1.1.1.3 depth=2 simple apply conj
Debug: 1.1.1.3.1 depth=1 unfold Nat.sub
Debug: 1.1.1.3.1.1 depth=0 unfold Nat.sub
Debug: 1.1.1.3.1.2 depth=0 unfold Nat.add
Debug: 1.1.1.3.1.3 depth=0 simple apply conj

Am I doing something wrong?

Coq Version

A recent master: 598628f
Also in 8.12.

[ppedrot]

Am I doing something wrong?

Proving goals that computationally reduce to huge statements?

[JasonGross]

But I think eauto is bugged here: Hint Unfold should add a progress unfold hint, not an unfold hint.

[cpitclaudel]

Proving goals that computationally reduce to huge statements?

Woops, try that instead:

Goal False.
  Create HintDb cc discriminated.
  Hint Unfold Nat.add Nat.sub Nat.mul Nat.div : cc.
  Time eauto 10 with cc.
  (* Finished transaction in 10.966 secs *)

[ppedrot]

The funny thing is that I've been recently looking at that code, and there are actually two distinct bugs here.

For undiscriminated dbs, unfold is pre-filtered on the head of the goal, so in theory it shouldn't apply in the first example. I am not quite sure why it passes the dnet filter, maybe the goal is too big and the head is never reached...

For discriminated dbs, unfolding a global that is transparent in the db applies it indiscriminately to any goal (don't ask me why, but it's heavily relied upon). But I agree then that in any case, we should not try to unfold if the goal is untouched (or does not contain the constant).

[ppedrot]

But isn't the original example using a discriminated hint db?

@cpitclaudel Yes, the first part of my above post is irrelevant, because I misread the original example. Sorry :/

[cpitclaudel]

No worries! Thanks a lot for working on a fix :)