Stream: Coq users

Topic: Defer unificiation until tactic?


view this post on Zulip Shea Levy (Oct 30 2020 at 00:04):

I have some function like foo:a,BaCfoo : \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?

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:15):

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

view this post on Zulip 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)'.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 11:02):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 11:05):

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

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 11:06):

Is b too big to duplicate?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 13:11):

Instead of _ @eq, just _

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 13:12):

Yes.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 13:46):

I wonder if stdpp telescopes might be relevant here.

view this post on Zulip 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"

view this post on Zulip Shea Levy (Oct 30 2020 at 13:47):

Oh hey, yeah that's the same type


Last updated: Jan 29 2023 at 01:02 UTC