Allow "use: ..." option to accept lemmas with implicit arguments?

[ccyip]

Coq version: 8.12.2 Hammer version: 1.3

So far the sauto/hauto/qauto tactics family has been amazing for my Coq development. However, it does not work quite well when we have lemmas with implicit arguments and a bunch of implicit type class constraints. This problem becomes more unfortunate when I am also using the stdpp library (https://gitlab.mpi-sws.org/iris/stdpp), which contains a lot of such lemmas. One example of such lemmas is insert_mono from stdpp.fin_maps.

Let's say we have a lemma lem whose type is like forall {A}, .... We can use this lemma with eauto (eauto using lem), but we can not use it directly with sauto. Running sauto use: lem gives me errors about not being able to infer the implicit parameter A. (the use tactic behaves the same)

In this simple case, we can just prepend the lemma with @, so sauto use: @lem works. However, if this lemma also has a lot of type class constraints, sauto use @lem (or hauto, etc) may either fail or run forever. I suspect it is because the amount of assumptions sauto needs to discharge is huge. For example, pose proof @insert_mono (or use @insert_mono) produces the following hypothesis. (I apologize for the out-of-context example, but my point is some lemmas have a lot of typeclass assumptions)

  H : ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : 
                                                    ∀ A : Type, 
                                                      Lookup K A (M A)) 
         (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type, PartialAlter K A (M A)) 
         (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A)) 
         (EqDecision0 : EqDecision K),
         FinMap K M
         → ∀ (A : Type) (m1 m2 : M A) (i : K) (x : A),
             m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]> m2

My current workaround is to run epose proof lem first. For example, epose proof insert_mono produces the following hypothesis instead.

  H : ∀ (m1 m2 : amap ?A) (i : atom) (x : ?A), m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]> m2

As you can tell, Coq has already resolved all the type class constraints. If I run sauto now, it is more likely to solve the goal than sauto use: @lem.

It would be great if sauto family also accepts lemmas with implicit arguments like eauto does, and let Coq figure out what the type class instances are. I reckon this should be a fairly simple fix, because sauto apparently works well if I epose proof the lemmas first.

Thanks for your hardwork!

[lukaszcz]

Thank you for your feedback. The issue you mention is indeed "easy" to solve in the sense that this doesn't involve the sauto procedure at all and it's purely a matter of proper interfacing with Coq's OCaml API. And I know in principle how to solve it: look at how argument parsing is done for eauto (https://github.com/coq/coq/blob/master/plugins/ltac/g_auto.mlg) and implement it analogously for sauto (https://github.com/lukaszcz/coqhammer/blob/coq8.12/src/tactics/g_hammer_tactics.mlg).

However, Coq's OCaml API is quite elaborate, so it's not entirely straightforward to figure out how to use it. I remember I thought about doing this and guesstimated it would take me at least several hours to figure it out in detail. So I just declared arguments to "use:" as "ne_constr_list", which results in the implicit arguments not being inferred properly.

I will probably fix this at some point, when I have a free weekend or two. But it may take several months before I do. If you really need this feature and have at least passing familiarity with Coq plugin programming (or willing to learn it), you could try doing it yourself and submitting a pull request. Otherwise, you might need to wait quite some time before I get down to this.

[ccyip]

Thanks for your informative reply and pointers! I have no experience in Coq plugin development, but I will probably give it a shot when I find some free time.

[ccyip]

See #98 . Any feedback is appreciated.

[lukaszcz]

Fixed with #98. Thanks.