The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi.

I've figured out a way to (almost) apply non-polymorphic functions as if they were polymorphic, using the quirky fact that [context] doesn't type-check the term it creates (see code at bottom).  There is the minor annoyance that my tactic requires a dummy variable to instantiate the function with.  (Does anyone have a way around this that doesn't involve [admit]?  I tried [evar], but that leaves over an uninstantiated existential variable.)  There is the larger annoyance that this tactic cannot deal with opaque proofs in the term which are insufficiently polymorphic, such as those generated by [Qed] or [abstract].  I pose the following challenge: Suppose I have a tactic [tac] which can re-create from scratch the proof of any term [pf : T] where [T : Prop], which appears in the output of [Set Printing All. Eval simpl in f.].  Can someone come up with a tactic which is like [polymorphically_apply] (below), but which replaces all existing proofs of things of type [Prop] in [f] with a freshly made proof?

Thanks!

  Local Ltac replace_by_context from to expr :=

    match expr with

      | appcontext expr'[from] => let expr'' := context expr'[to] in

                                  replace_by_context from to expr''

      | _ => expr

    end.

  Local Ltac polymorphically_apply' f x mk_dummy_x simpl_tac then_tac :=

    match type of f with

      | forall _ : ?T, _ => let x0 := fresh in assert (x0 : T) by mk_dummy_x;

                                              let fx0 := simpl_tac (f x0) in

                                              let fx := replace_by_context x0 x fx0 in

                                              clear x0;

                                                then_tac fx

    end.

  Local Ltac polymorphically_apply f x mk_dummy_x then_tac :=

    polymorphically_apply' f x mk_dummy_x ltac:(fun fx => eval simpl in fx) then_tac.

  Definition id_set (a : Set) := a.

  Arguments id_set / a.

  Definition foo : Type.

    (* exact (id_set Set). *)  (* Error: The term "Set" has type "Type" while it is expected to have type "Set". *)

    (* let t := eval simpl in (id_set Set) in exact t. *)  (* Error: The term "Set" has type "Type" while it is expected to have type "Set". *)

    polymorphically_apply id_set Set ltac:(exact nat) ltac:(fun fx => exact fx).

  Defined.

  Print foo. (* foo = (fun _ : Set => Set) nat : Type *)

-Jason