Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment)


Chronological Thread 
  • From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment)
  • Date: Thu, 8 Jun 2017 02:16:06 +0300
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f49.google.com
  • Ironport-phdr: 9a23:MJQ93Rxnm/iX/+DXCy+O+j09IxM/srCxBDY+r6Qd1OkfIJqq85mqBkHD//Il1AaPBtSEraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDqhicJNzA3/mLKhMJukK1WuwiuqwBlzoPOfI2ZKPhzc6XAdt0aX2pBWcNRWjRCDIO4aosKCfABPf1FpITjplsOtwa+BQ2tBOP01zRFgX723ak/0+s7CwHGxxYsEM4PsHTOsdX1MKYSUfuuwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesTS0UkiDx3JgkmUpID/PD6Y1v4Bv3aG4+duT+6ihGoqpgdsqTa13MgskJPGhocNx1DE6yp5xIE1KMW9SEFhYN6kFIJctz+ZN4dqW88iTW5ltSIgxr0Jvp67eycKyJA5yBLFd/OHdI2I7griVOaXPzh4mGpodKyjixu260Stye3xWtOq3FpXoCdJiNbBu3QV2xzW8MeHS/99/km72TaI0gDe8uBEIUQxlaXBMZ4h2aQ8mYYSsUTZAy/2nET2jLSNe0Ur/+in8eXnYrH8qpCAMI90jxnyMr4ylcynHeQ4Lg8OUnCH9uS7zb3v5FH2QLFXjvItiaTZq5DbJcEDpqGjGQNV04Aj6wy+Dzi8ytgYk2MHfxp5f0fNhI/wflrKPfrQDPGlgl3qni0hj6TNOaSkCZHQJFDClq3gdPBz8RgP5hA0yIV+45f/EKpJC/PpR0vwr5SMDxs8Ohavhe3mEsh515g2VmeGA6vfO6TX5wzbrtkzKvWBMddG8A32LOIosqbj

Changed the equivalence relation between two "Fun A B" (in the Proof of FunEquiv) to simple equality and, for now, everything seems working.

On Wed, Jun 7, 2017 at 8:43 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:
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.







Archive powered by MHonArc 2.6.18.

Top of Page