I have some function like 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?
That can't be done, but foo ltac:(tactic1) b should work here.
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)'.
Paolo Giarrusso said:
That can't be done, but foo ltac:(tactic1) b should work here.
And tactic1
will be able to inspect b
?
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
I mean, I still don't get where your requirements come from, and what they are even.
You can write tactic notations that take a uconstr, which is not typed.
But "type it as best as it can" doesn't seem to be possible, at least in my conceptual model.
"Notation foo' b tac := (foo ltac:(tac b) b)" would work
Is b too big to duplicate?
Paolo Giarrusso said:
"Notation foo' b tac := (foo ltac:(tac b) b)" would work
Ah yeah, this should be good enough
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
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
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.
Instead of _ @eq, just _
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.
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)
And the other problem is that unification can't infer things here, because it generally can't invert functions (except constructors)
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.
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.
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)
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
I wonder if stdpp telescopes might be relevant here.
Probably not on the inference question, but on the rest: they're about a type of "functions from N arguments for any natural N"
Oh hey, yeah that's the same type
Last updated: Oct 13 2024 at 01:02 UTC