The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

It makes sense that it increases the size of the search space for CS. It sounds like the answer is that it isn't possible, and that the correct thing to do is to write all of the instances that you need.

Thanks.

On Sat, Feb 29, 2020 at 11:07 AM Beta Ziliani <beta AT mpi-sws.org> wrote:

Sounds like that would bloat the search space of CS. In this case is obvious, but how do you foresee if you need some coercion (and which one!)?

Written from mobile. Excuse my limited communication.

On Sat, Feb 29, 2020, 11:39 AM Gregory Malecha <gmalecha AT gmail.com> wrote:

Hello --

Is there a way to get canonical structures and coercions to work together? Here's my toy example:

Structure EX : Type :=
{ t :> Type
; GET : t -> Prop }.

Definition foo {e : EX} := e.(GET).

Canonical Structure TrueEX : EX :=
  {| GET := fun _ : bool => true |}.

Definition to_bool (n : nat) :=
  match n with
  | 0 => false
  | _ => true
  end.

Coercion to_bool : nat >-> bool.

Check (foo true). (* works great! *)
Check (foo 1).    (* fails *)

Intuitively, I would expect the term [@foo boolEX (to_bool 1)] but instead I get a type error "the term 1 has type nat while it is expected to have type EX".

Is there some way to make this work without making instances for, e.g. [natEX], which is the composition of [to_bool] and [foo]?

Thanks.

--

gregory malecha

gmalecha.github.io

--

gregory malecha

gmalecha.github.io