The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Are you looking for something like this?  (Initial idea courtesy of Georges Gonthier.)  Note that the typeclasses must be resolved (and resolvable) when defining the thing of type [foo a b].  Otherwise, you can define [k] of type [list a -> b], and then write [(k : foo a b) : bar a b].

(* your definitions *)

Class X (a : Type) : Type := {}.

Class Y (b : Type) : Type := {}.

Axiom onEach : forall a b, X a -> Y b -> (list a -> b) -> (a -> b).

Definition bar a b := a -> b.

(* abuse of typeclasses *)

Class foo_holder (a b : Type) := { foo : Type ; xa : X a ; yb : Y b ; good : foo = (list a -> b) }.

Arguments foo a b {_}.

Instance mk_foo a b (xa' : X a) (yb' : Y b) : foo_holder a b

  := {| foo := list a -> b ; xa := xa' ; yb := yb' ; good := eq_refl |}.

Coercion onEach' a b f (x : @foo a b f) : bar a b

  := onEach _ _ (@xa _ _ f) (@yb _ _ f) match @good _ _ f with

                                          | eq_refl => x

                                        end.

(* example *)

Global Instance: forall a, X a := {}.

Global Instance: forall a, Y a := {}.

Axiom a : Type.

Axiom b : Type.

Axiom k : foo a b.

Check k : bar a b.

On Fri, Oct 2, 2015 at 1:32 PM, Gregory Malecha <gmalecha AT gmail.com> wrote:

Hi, Jason --

Thanks for the pointer. I think it would have worked, except my example a little bit more simplified since [a] and [b] need associated type class instances. So the type of [onEach] is really [forall a b, X a -> Y b -> foo a b -> bar a b]. Coq reports that this does not respect the uniform inheritence condition, which is in line with what is written in the manual.

On Thu, Oct 1, 2015 at 4:12 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

As a kludge, stick the definitions in a module, their types in a module type, declare the coercion in a functor, and then import the applied functor?

-Jason

On Oct 1, 2015 6:54 PM, "Gregory Malecha" <gmalecha AT gmail.com> wrote:

Hello --

I have some types (similar to):

Definition foo a b  := list a -> b.

Definition bar a b := a -> b.

and I have a function to transport [foo]s into [bar]s.

Definition onEach : forall a b, foo a b -> bar a b.

I want to declare [onEach] as a coercion:

Coercion onEach : foo >-> bar.

but I get

Error: Found target class bar instead of Funclass.

Is there some way to tell Coq that it should treat [bar] as opaque? I know that I can make [bar] a record type, but I don't really want to pack and unpack functions all the time.

Thanks.

--

gregory malecha

--

gregory malecha