apply tactic, similar to rewrite

[patrick-nicodemus]

Let me know if you can suggest useful ways to eliminate duplication here between apply and rewrite, both of them are doing the same thing where they traverse nested foralls.

Is repeatedly calling refine and failing inefficient? I have no idea.

I would also be interested if you have suggestions for making it stronger, it would be nice to have it behave as
"if the type of term f is unifiable with forall (x : A), B, then recursively apply f _. But I don't know how to check that checks whether a type is unifiable with a product type.

[patrick-nicodemus]

Not sure if coq.saturate is appropriate here, if we want to be able to apply f : A -> (B -> C) to the goal B -> C.
Unless we want to saturate both the term to be applied and the goal.

[gares]

Thanks for your contribution, please have a look at my comments.

[gares]

Why do you want to check this? Can't it be an arbitrary term?

[patrick-nicodemus]

I just want the type Ty of the term T somehow, so that I can iteratively drop down through the nested foralls of Ty.

[gares]

Then the typecheck line suffices, no need for the '; mem ...' part

[gares]

There seems to be a misconception here, I think you want to reduce the type, not the proof term
Untested:

Suggested change

	apply Term (prod _ _ B) G GL :-
	whd (app [Term, Hole]) [] HD ARGS,
	unwind HD ARGS Term',
	apply Term' (B Hole) G GL.
	apply Term Ty G GL :-
	whd Ty [] (prod _ _ B) [],
	apply {coq.mk-app Term [Hole]} (B Hole) G GL.

[gares]

Suggested change

	apply T _ G GL :- refine T G GL.
	apply T _ G GL :- refine T G GL, !.

[gares]

Let me know if you can suggest useful ways to eliminate duplication here between apply and rewrite, both of them are doing the same thing where they traverse nested foralls.

Is repeatedly calling refine and failing inefficient? I have no idea.

I would also be interested if you have suggestions for making it stronger, it would be nice to have it behave as "if the type of term f is unifiable with forall (x : A), B, then recursively apply f _. But I don't know how to check that checks whether a type is unifiable with a product type.

I did do a whd. If you want to be stronger and unify, you can call coq.unify-eq Ty {{ forall x, lp:(B x) }} ok (the quotation is not necessary, but looks nicer than (prod _ _ B) (or (prod _ _ x\B x) that I do recomment since it documents B takes an argument.