Created
November 1, 2016 20:59
-
-
Save roboguy13/8f52a2cdbac3f37ed31fe9662cf088e1 to your computer and use it in GitHub Desktop.
Groups in Coq
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Definition assoc_law {g : Type} (op : g -> g -> g) := | |
forall (x y z : g), | |
op (op x y) z = op x (op y z). | |
Definition left_iden_law {g : Type} (iden : g) (op : g -> g -> g) := | |
forall (x : g), | |
op iden x = x. | |
Definition right_iden_law {g : Type} (iden : g) (op : g -> g -> g) := | |
forall (x : g), | |
op x iden = x. | |
Definition left_inv_law {g : Type} (iden : g) (op : g -> g -> g) (inv : g -> g) := | |
forall (x : g), | |
op (inv x) x = iden. | |
Definition right_inv_law {g : Type} (iden : g) (op : g -> g -> g) (inv : g -> g) := | |
forall (x : g), | |
op x (inv x) = iden. | |
Definition is_group {g : Type} (iden : g) (op : g -> g -> g) (inv : g -> g) := | |
assoc_law op /\ | |
left_iden_law iden op /\ | |
right_iden_law iden op /\ | |
left_inv_law iden op inv /\ | |
right_inv_law iden op inv. | |
(* Prove counterexample is not a group *) | |
Inductive NotAGroup := N0 | N1. | |
Definition counter_iden := N0. | |
Definition counter_op (x y : NotAGroup) := N0. | |
Definition counter_inv (x : NotAGroup) := N0. | |
Theorem NotAGroupThm : | |
not (is_group counter_iden counter_op counter_inv). | |
Proof. | |
unfold not. | |
unfold is_group. | |
intro. | |
(* Split up the conjunction *) | |
destruct H. | |
destruct H0. | |
destruct H1. | |
destruct H2. | |
(* Use the fact that 'op iden N1' does not equal 'N1' *) | |
unfold left_iden_law in H0. | |
unfold counter_op in H0. | |
set (H0' := H0 N1). | |
discriminate. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment