The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Hello, Coq-club

I tried to define something similar to Bishop sets (using existing parts of Standard Library about Equivalences and Morphisms), then defined Group structure with equivalence instead of equality and tried to prove that a ∘ b ≡ e → b ≡ a⁻¹.

I was kind of succesful but encountered a problem.

Last one rewrite failed with "setoid rewrite failed: Unable to satisfy the following constraints" and I had to work around it a bit.

Is there some way to fix definition of Fun to avoid similar problems?

Best wishes,

Ilmars

Require Import Utf8 Relations Equivalence Morphisms Setoid.
Set Implicit Arguments.

Class Equiv := {
  EquivT : Type;
  EquivR : relation EquivT;
  EquivE :> Equivalence EquivR
}.
Coercion EquivT: Equiv >-> Sortclass.

Notation "x ≡ y" := (EquivR x y) (at level 70).

Class Fun (A B: Equiv) := {
  FunF : @EquivT A → @EquivT B;
  FunP :> Proper (@EquivR A ==> @EquivR B) FunF
}.
Coercion FunF: Fun >-> Funclass.

Definition FunEquiv (A B: Equiv): Equiv.
Proof.
  pose (λ (F1 F2: Fun A B), ∀ x y, x ≡ y → F1 x ≡ F2 y) as R.
  simple refine (let E := (_ : Equivalence R) in _).
    split.
    + unfold Reflexive. intros x. apply x.
    + unfold Symmetric. unfold R. intros. rewrite H0, (H y0 y0); reflexivity.
    + unfold Transitive. unfold R. intros.
      rewrite (H x0 y0 H1), (H0 y0 y0 (reflexivity _)); reflexivity.
  + exact (Build_Equiv E).
Defined.
Check (λ A B, FunEquiv A B: Type).

Print Scopes.

Structure Group := {
  GroupT: Equiv;
  GroupOp: Fun GroupT (FunEquiv GroupT GroupT);
  GroupAssoc: ∀ a b c, GroupOp (GroupOp a b) c ≡ GroupOp a (GroupOp b c);
  GroupId: GroupT;
  GroupIdR: ∀ a, GroupOp GroupId a ≡ a;
  GroupIdL: ∀ a, GroupOp a GroupId ≡ a;
  GroupInv: Fun GroupT GroupT;
  GroupInvR: ∀ a, GroupOp a (GroupInv a) ≡ GroupId;
  GroupInvL: ∀ a, GroupOp (GroupInv a) a ≡ GroupId;
}.

Print Group.
Notation "a ∘ b" := ((GroupOp _) a b) (at level 60, right associativity).
Notation "a '⁻¹'" := ((GroupInv _) a) (at level 55).
Notation "'e'" := (GroupId _).

Theorem T0 (G: Group) (a b: GroupT G):
  a ∘ b ≡ e → b ≡ a⁻¹.
Proof.
  intros. rewrite <- (GroupIdL _ (a⁻¹)). rewrite <- H. rewrite <- GroupAssoc.
  rewrite <- (GroupIdR _ b) at 1.
  (* why does this fail? *) try (rewrite (GroupInvL _ a); reflexivity).
  destruct G. destruct GroupOp0. apply FunP0.
  rewrite GroupInvL0. reflexivity. reflexivity.
Qed.