grind, non Prop goals, and existential witnesses

Stream: general

[Sam]

I've noticed that grind seems unable to solve non Prop goals, so something like example (x : Nat) : Nat := by grind fails. Is this expected to be a permanent limitation?

This is a curiosity which isn't well motivated by a real use case, but it came up in the context of prodding grind's behaviour around Exists, where it seems unable to produce even trivial witnesses. I'm primarily just asking because I find grind interesting, but I'm also curious what the ambition is in terms of how grind will deal with existential quantifiers; it seems to hit dead ends in even trivial cases at the moment, but perhaps this is largely down to lack of annotations.

[Sam]

As a tangential generalisation of this question, is the goal of grind that, if hypothetically supplied with the right satellite solvers (which can be done by users?), it should be able to solve any goal? Up to reasonable complexity/time/resource limits of course.

[Aaron Liu]

My guess is that grind is using false_or_by_contra somewhere internally so if you give it a non-prop goal then it basically forgets the goal and just tries to prove a contradiction.

[Sam]

Ah that does sound consistent with what I've observed. I suppose that means this is a hard limitation then.

[Chris Henson]

If you look at the error that grind reports, you can even see that the goal is False.

[Sam]

Yeah true. I did partially make that connection, but I suppose I'm asking whether it could/should be smarter about not trying to prove non prop goals by contradiction, or whether this is simply completely out of scope. For goals or subgoals which would normally use witnesses, is the assumption that there will always be some other theorem which can be used without manually supplying the witness?

These might be stupid questions. I'm not much of a lean user or that well mathematically educated, and am mostly interested in grind from the sidelines for its potential applicability to other domains around program verification.

[Kevin Buzzard]

I wonder whether you are looking for canonical if you want to fill in data.

[Ruben Van de Velde]

So the first question really is what you'd want grind to do in this case. If the goal is a Prop, that's easy, because any value (proof) is as good as the next - this is proof irrelevance. But if you need a natural number, it tends to matter whether you get 0 or 37

[Sam]

I came across this while playing with whether grind could handle example : ∃ _ : Nat, True := by grind which is a case where we do reasonably want to synthesise a value. However, I suppose the more sensible way is a grind annotation on something like exists_const?

[Sam]

My example is obviously so contrived as to perhaps be completely unrepresentative of almost any real use case.

[Kim Morrison]

Don't hold your breath on grind providing existential witnesses. We don't know of any sensible way to do this that doesn't introduce surprising behaviour and/or performance problems. Our intention is to deal with all the low hanging fruit of grind features that are predictable, fast, and helpful, and to have a think about existential witnesses again further down the track.