coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[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: [Coq-Club] Tried to simulate Bishop sets (an question about problem in the experiment)
- Date: Wed, 7 Jun 2017 20:43:52 +0300
- Authentication-results: mail3-smtp-sop.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-f47.google.com
- Ironport-phdr: 9a23:2/Q4qhJCJYjiZzFtVNmcpTZWNBhigK39O0sv0rFitYgRKfnxwZ3uMQTl6Ol3ixeRBMOAuq0C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicJOTA67W/ZlNB/gblBrx69vRFy2ZLYbJ2XOfd4Y6jTfckaRW1EXstJVCJBBoa8ao0VD+oaIO1VsYj9p0ETrRu6BAmsH/7kxzhJhn/y2K01yf4hERrc0AM8HtIOqmnUrNH0NKcJSu21w6zIwi/Cb/NSwzvy9I/IchU4rPyKQLl+ctLRxFExGw/Zilics4/oMjOP2ugTrmSW4fBsWO2thmMhtgp/uCKgxt02hYnMno8Vyk7L9SF+wIstIN23Uk97Ydq9HJtOtCGWK5J6Qs0tTmxqoio6xboGuZm0fCgO1psr3QLQa/uCc4SQ4xLjUvieIStgiX57ZL6ygwy+/Eugx+HmSMW4zVhHojBKn9TOrnwN0gbc6smDSvtz5Eeh3jOP2hjS6uFAJEA7j7DbK4U7zrEsl5oTq1nDHiv3mEXtl6KWeUAk9fKp6+TjeLnpupicN4pshgHkLqsugtC/Afg/MgUWQ2eb/v282KT/8k39XbVFleY7krLZsZDfPcQUvLS1Aw5T0oY56hawFS2q0NoCnSpPEFUQMhmAls3iP0zECPH+F/a2xVq22n8/zPffe7blH5/lL37Zkb6nc6wruGBGzw9m7NRaTIhPQpoAOu/3W1S54N3cCxYjKEq/wvz6DNRm/owbUGOLRKSeNfWB4hez+uszLrzUN8cuszHnJq196g==
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⁻¹.
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,
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.
- [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.