Transparency in hint databases need some more documentation

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5301
From: @jhjourdan
Reported version: 8.6
CC: @RalfJung

[coqbot]

Comment author: @jhjourdan

When are constants considered opaque for eauto ?

[Hint Opaque] should make it possible to make some constant opaque, but apparently it does not in all cases, and particular in the following script:

Parameter P : nat -> Prop.

Definition d := 1.

Hint Opaque d.

Parameter H : P 1.
Hint Resolve H.

Goal P d. eauto.  (* H has been used although d is opaque. *) Qed.

Moreover, it seems like (even though I am not sure) Hint Opaque annotations are completely ignored when it comes to unfold constants appearing in hints (as opposed to when they appear in the goals they are unified to).

Additionally, the [discriminated] option that we can put on hint databases has poor documentation. Is it possible to get an example where it makes a difference in performance and/or in behavior?

[maximedenes]

I would need answers to these questions. @mattam82 or @Zimmi48 can you say a few words about it? Thanks!

[mattam82]

Essentially, auto and new auto ignore this flag for conversion of closed terms (when unification falls back to conversion) when using non-discriminated databases, new auto with a discriminated database supports it consistently (i.e. for closed and non-closed cases) and typeclasses eauto supports it consistently.

Example:

Parameter P : nat -> Prop.
Definition d := 1.
Create HintDb mine discriminated.
(* Hint Constants Transparent : mine. *)
Hint Opaque d : mine.
Print HintDb mine.
Parameter H : True -> P 1.
Hint Resolve H : mine.
Goal P d. Fail progress new auto with mine. 

IIRC, the reason for this highly annoying discrepancy is compatibility. Théo has been working on fixing this.

[maximedenes]

Thanks! And apart from its limitations, what does the flag itself mean? Does it make constants opaque on both sides of the resolution (i.e. the current goal and the hints)?

[mattam82]

Yes, it calls unification with that constant declared opaque, so in both the goal and hint side.

…

On Sat, Nov 10, 2018 at 2:00 PM Maxime Dénès ***@***.***> wrote: Thanks! And apart from its limitation, what does the flag itself mean? Does it make constants opaque on both sides of the resolution (i.e. the current goal and the hints)? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#5301 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAGARbRHAq3r869qrjSQ7F4XkXUiWimpks5utszWgaJpZM4YXsrO> .

[maximedenes]

Thanks @mattam82! One more thing I was wondering. Suppose I have an alias like Definition a := b, and I would like hints and goals to unify indifferently when they mention a or b.

Does Hint Transparent help with that? Should I use another command?

Context: I'm trying to remove some module-related features from the kernel, but I need to tweak the behavior of hints w.r.t. aliases.

[mattam82]

A priori, you will have to fix auto for that to work in general, as for unification of non-closed terms, auto uses the empty transparent state while new auto uses the one from the database (so in that case, it's likely that just moving from auto to new auto would work). The core database has no unfoldable constants or variables by default, so you could make this work by declaring Hint Transparent for the constants you want to be unfoldable indeed. One caveat though: if the constant appears as a head this will not work (hints for b won't apply to a goals) as the indexing of hints is syntactic on the head. You'd need Hint Unfold a for that.

[maximedenes]

Maybe I misinterpreted what you wrote above, but is the following a bug w.r.t. Hint Transparent, then?

Axiom b : nat -> Prop.
Definition a := b.

Create HintDb foo.

Hint Transparent a : foo.
Hint Unfold a : foo.

Axiom ax0 : a 0.
Hint Resolve ax0 : foo.

Goal b 0.
Proof.
new auto with foo.
Qed. (* fails *)

[mattam82]

Oh I see now. This is not symmetric as I said earlier. Only in discriminated databases ax0 is treated as a hint with no pattern because you declared it transparent, which makes it apply to the `b 0` goal. Otherwise we’re looking for the b head and nothing is found. Le lun. 12 nov. 2018 à 18:24, Maxime Dénès <notifications@github.com> a écrit :

…

Maybe I misinterpreted what you wrote above, but is the following a bug w.r.t. Hint Transparent, then? Axiom b : nat -> Prop.Definition a := b. Create HintDb foo. Hint Transparent a : foo.Hint Unfold a : foo. Axiom ax0 : a 0.Hint Resolve ax0 : foo. Goal b 0.Proof. new auto with foo.Qed. (* fails *) — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#5301 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAGARZQYldbmaYjAaN0mApS0aXd0h4UEks5uua7QgaJpZM4YXsrO> .

[maximedenes]

But then why doesn't it work with a discriminated database?

Axiom b : nat -> Prop.
Definition a := b.

Create HintDb foo discriminated.

Hint Transparent a : foo.
Hint Unfold a : foo.

Axiom ax0 : a 0.
Hint Resolve ax0 : foo.

Goal b 0.
Proof.
new auto with foo.
Qed.

[mattam82]

Gah, because we still register ax0 as a hint for a and not a hint with no pattern as it should be in that case (the is_unfold line 638 of hints.ml) :/

[maximedenes]

Gah

So, is it a bug? If yes, I'll report it and try to fix it.

and not a hint with no pattern

I would have expected the registration to unfold a to find the pattern (so b), rather than no pattern, no?

[andrew-appel]

Here's another example demonstrating (in Coq 8.9.0) the original bug:

Fixpoint repeat n := match n with O => nil | S n' => cons tt (repeat n') end.

Hint Resolve @eq_refl : foo.

Definition N := 100.
Lemma N_eq : N = 100. Proof. reflexivity. Qed.
Opaque N.

Goal length (repeat N) = N.
Proof.
Fail simple apply @eq_refl.
Fail progress (auto with nocore).
Print HintDb foo.
solve [auto with nocore foo].  (* This is a bug! *)
Qed.

The auto with nocore foo behaves like apply eq_refl, but Print HintDb foo claims that it will behave like simple apply @eq_refl.

If we "fix" auto so that it respects Opaque, how many users' proofs will break? Can we have a mode-switch for this, so that we can make experiments to investigate this question?