The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

Using QWIRE's matrices I was able to define:

```

Definition to_scalar (A : Matrix 1 1) : C := A 0 0.

Notation Matrix11 := (Matrix 1 1).

Coercion to_scalar : Matrix11 >-> C.

```

but I get the warning "to_scalar does not respect the uniform inheritance condition" which seems to imply "this coercion will not work". 

(The Coq documentation https://coq.inria.fr/refman/addendum/implicit-coercions.html implies that I shouldn't even be able to define a coercion that doesn't respect the uniform inheritance condition so I'm not sure why this gives a warning rather than an error.)

Alternatively, I can define:

```

Definition to_scalar (m n : nat) (A: Matrix m n) : C := A 0 0.

Coercion to_scalar : Matrix >-> C.

```

This works, but it doesn't obey your restriction that it only applies to Matrix 1 1 (which is a desirable restriction).

I would also like the ability to say `Coercion to_scalar : forall A, Matrix A -> A` (assuming parametric matrices) but `Coercion` doesn't seem to support any kind of dependency.

Best,

Robert

On Wed, Aug 21, 2019 at 12:07 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq Users,

 

I wonder if it is possible to define an implicit coercion between a 1x1 matrix (either using mathcomponent’s or Coquelicot’s definition) and the respective scalar type?

 

I see two problems with this:

 

1.)    I don’t see how I could specialize the coercion to the size parameters 1x1. I can define this as separate type mat11, but then I need to use a type annotation to mat11 to enable the coercion. I tried to make an identity coercion between matrix and mat11 but couldn’t figure it out.

2.)    Ideally I would like to have this for matrices of any types, not just specific types like R or C. But I don’t see a way to use a parameter of the first class as second class.

 

Is it possible to do this?

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928