Ssreflect Users Discussion List

[Ian Zimmerman <>]

I'm working on a beginner's project: in the end, I hope to prove,
assuming classical axioms, that the bijections on a type (not
necessarily finite) form a group.

This is how far I got:

  From mathcomp Require Import ssreflect ssrfun ssrbool.
  Set Implicit Arguments.
  Unset Strict Implicit.
  Unset Printing Implicit Defensive.
  Require Import Utf8.

  Record group_op (A: Type): Type := Group_op {
    op: A → A → A;
    e: A;
    inv: A → A;
  }.

  Class group (A: Type) (g: group_op A) := Group {
    group_assoc_prop: let: Group_op o _ _ := g in associative o;
    group_neutral_l_prop: let: Group_op o e _ := g in left_id e o;
    group_neutral_r_prop: let: Group_op o e _ := g in right_id e o;
    group_inverse_l_prop: let: Group_op o e i := g in left_inverse e i o;
    group_inverse_r_prop: let: Group_op o e i := g in right_inverse e i o;
  }.

  Section Perm_group.

  Variable T: Type.

  Let perm_sig := {f: T → T | bijective f}.

  Let Φ (fb: perm_sig) : T → T := let: exist f _ := fb in f.

  Let perm_group_op fb gb : perm_sig := 
    let h := ((Φ fb) \o (Φ gb)) in @exist _ _ h (@bijective T T h).

And here I get this error:

  In environment
  T : Type
  perm_sig := {f : T → T | bijective f} : Type
  Φ := λ '(@exist _ _ f _), f : perm_sig → T → T
  fb : perm_sig
  gb : perm_sig
  h := Φ fb \o Φ gb : T → T
  The term "exist (λ f : T → T, bijective f) h (bijective h)" has type "{f : 
T → T | bijective f}"
  while it is expected to have type "perm_sig" (cannot satisfy constraint 
"Prop" == "(λ f : T → T, bijective f) h";
  cannot unify "Prop" and "bijective h").

"Cannot unify" ?? perm_sig was defined two lines above to _literally_ the
other type it is complaining about.  Coq 8.9.

-- 
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.