Ssreflect Users Discussion List

[Ian Zimmerman <>]

On 2019-09-20 08:41, Laurent Thery wrote:

> Error messages are often difficult to parse at the beginning (they often
> contain lots of information!), the key part of the error message is
> 
> Prop" == "(λ f : T → T, bijective f) h;
> cannot unify "Prop" and "bijective h").
> 
> it tells you that the system is expecting a proof of bijective h and
> is given a proof of Prop (ie a witness that Prop is inhabited)
> 
> In fact you give  :
> 
>  @exist _ _ h (@bijective T T h)
> 
> 
> where (@bijective T T h) : Prop
> 
> instead you should give
> 
>  @exist _ _ h H
> 
> where H is a proof that h is bijective
> 
> hope this helps

Thanks for this, and also for the 2 private replies sent to me by
others.  There's a multitude of lessons for me here.  First the solution:

Let perm_group_op (fb: perm_sig) (gb: perm_sig) : perm_sig := 
  match fb with exist f fp =>
    match gb with exist g gp =>
      @exist (T → T) _ (f \o g) (bij_comp fp gp)
    end
  end.

which leads to the most specific lesson: don't "forget" the proof part
of sigmas, it will be needed.

Second, try to remember the difference between "is" as "equals", and
"is" as "belongs to".  I guess this goes all the way back to Frege!

And third and most general, of course, don't omit type annotations until
I know what I'm doing, LOL.

Thanks again!

-- 
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.