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:
Is there some way to fix definition of Fun to avoid similar problems?Hello, Coq-clubI was kind of succesful but encountered a problem.
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⁻¹.
Last one rewrite failed with "setoid rewrite failed: Unable to satisfy the following constraints" and I had to work around it a bit.Best wishes,IlmarsRequire 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.
- [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment), Ilmārs Cīrulis, 06/07/2017
- Re: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment), Ilmārs Cīrulis, 06/08/2017
- Re: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment), Ilmārs Cīrulis, 06/26/2017
- Re: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment), Ilmārs Cīrulis, 06/08/2017
Archive powered by MHonArc 2.6.18.