## Stream: Coq users

### Topic: Defer unificiation until tactic?

#### Shea Levy (Oct 30 2020 at 00:04):

I have some function like $foo : \forall a, B a \to C$ where B is a complex function. I'd like to be able to write something like foo _ b and use a tactic to fill in the a based on the form of b, but unfortunately coq throws a type error because it can't see how b can be of the right type. Is there any way I can tell coq not to try to unify the type of b with B _, just type it as best it can and let the tactic fill in?

#### Paolo Giarrusso (Oct 30 2020 at 01:15):

That can't be done, but foo ltac:(tactic1) b should work here.

#### Fabian Kunze (Oct 30 2020 at 06:33):

What i did one was to define a notation "foo' a b" that uses inline-ltac to first ro first check b, compute a, and then return "exact (foo a b)'.

#### Shea Levy (Oct 30 2020 at 09:10):

Paolo Giarrusso said:

That can't be done, but foo ltac:(tactic1) b should work here.

And tactic1 will be able to inspect b?

#### Paolo Giarrusso (Oct 30 2020 at 10:59):

Not per se, but Fabian's trick works here: you have b so you can pass it to the tactic by hand or with a notation

#### Paolo Giarrusso (Oct 30 2020 at 11:01):

I mean, I still don't get where your requirements come from, and what they are even.

#### Paolo Giarrusso (Oct 30 2020 at 11:02):

You can write tactic notations that take a uconstr, which is not typed.

#### Paolo Giarrusso (Oct 30 2020 at 11:04):

But "type it as best as it can" doesn't seem to be possible, at least in my conceptual model.

#### Paolo Giarrusso (Oct 30 2020 at 11:05):

"Notation foo' b tac := (foo ltac:(tac b) b)" would work

#### Paolo Giarrusso (Oct 30 2020 at 11:06):

Is b too big to duplicate?

#### Shea Levy (Oct 30 2020 at 11:35):

Paolo Giarrusso said:

"Notation foo' b tac := (foo ltac:(tac b) b)" would work

Ah yeah, this should be good enough

#### Shea Levy (Oct 30 2020 at 11:38):

Paolo Giarrusso said:

I mean, I still don't get where your requirements come from, and what they are even.

Playing around with relations of arbitrary arities:

Require Import Unicode.Utf8.

Inductive arity :=
| arity_nil : arity
| arity_cons : ∀ T, (T → arity) → arity.

Fixpoint type_function_type a :=
match a with
| arity_nil => Type
| arity_cons _ f => ∀ t, type_function_type (f t)
end.

Definition foo a (R : type_function_type a) : nat := 0.

Check (foo (arity_cons Type (λ T, arity_cons T (λ _, arity_cons T (λ _, arity_nil)))) (@eq)).


The first argument I passed to foo can be mechanically derived from eq, but if you leave a hole for that argument (even within a refine or somewhere not expecting to be able to resolve all evars) you get a type error

#### Shea Levy (Oct 30 2020 at 13:05):

I guess another option would be to replace the (@eq) with (_ @eq) that I fill in with id once I've filled in the arity

#### Paolo Giarrusso (Oct 30 2020 at 13:10):

I don't know if bidirectional inference does better, but refine should use it. But my practical advice here is to just pass the arguments in order when refining.

#### Paolo Giarrusso (Oct 30 2020 at 13:11):

Instead of _ @eq, just _

#### Shea Levy (Oct 30 2020 at 13:11):

But I want @eq to come from the user and the tactic to fill in the other hole. So I guess I have to use the notation trick to pass @eq to the tactic directly

Yes.

#### Paolo Giarrusso (Oct 30 2020 at 13:14):

In general, tactics try to keep terms well-typed at all times. (That's not 100% enforced, nor necessary for soundness, but it's annoying to finish a proof and get a type error at the end)

#### Paolo Giarrusso (Oct 30 2020 at 13:15):

And the other problem is that unification can't infer things here, because it generally can't invert functions (except constructors)

#### Shea Levy (Oct 30 2020 at 13:16):

Paolo Giarrusso said:

And the other problem is that unification can't infer things here, because it generally can't invert functions (except constructors)

Right, so the behavior I was hoping for was some way to say "don't even try to unify this yet, just use the type you have for the term, including any evars if there are implicits". So halfway between not typechecking and full unification.

#### Paolo Giarrusso (Oct 30 2020 at 13:16):

So this shows up when "apply foo" fails but "apply (foo a)" is legal because, after reducing the type of "foo a", the result does unify.

#### Paolo Giarrusso (Oct 30 2020 at 13:18):

Yeah yeah, but see the other point. What you ask for might be doable in OCaml (no real clue), but you really don't want that (it's malpractice that I even suggest that)

#### Shea Levy (Oct 30 2020 at 13:20):

I guess if I wanted to get really fancy I can use a custom entry and map application to building up an ltac (2?) datatype

#### Paolo Giarrusso (Oct 30 2020 at 13:46):

I wonder if stdpp telescopes might be relevant here.

#### Paolo Giarrusso (Oct 30 2020 at 13:47):

Probably not on the inference question, but on the rest: they're about a type of "functions from N arguments for any natural N"

#### Shea Levy (Oct 30 2020 at 13:47):

Oh hey, yeah that's the same type

Last updated: Jun 17 2024 at 22:01 UTC