Skip to content

Instantly share code, notes, and snippets.

@roboguy13
Created November 1, 2016 20:59
Show Gist options
  • Save roboguy13/8f52a2cdbac3f37ed31fe9662cf088e1 to your computer and use it in GitHub Desktop.
Save roboguy13/8f52a2cdbac3f37ed31fe9662cf088e1 to your computer and use it in GitHub Desktop.
Groups in Coq
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