simple_set_example.v

Definition set (M : Type) := M -> Prop.
Definition belongs {M : Type} (x : M) (P : set M) : Prop := P x.
Definition subset {M : Type} (S T : set M) :=
  forall s, belongs s S -> belongs s T.

Definition id {M : Type} (S : set M) (id : M) (bin : M -> M -> M) :=
  forall s, belongs s S -> bin s id = s /\ bin id s = s.
    
Axiom id_belongs : forall {M : Type} (S : set M) (id_ : M) bin,
  id S id_ bin -> belongs id_ S.

Definition identity {M : Type} (S : set M) (bin : M -> M -> M) :=
  exists e, id S e bin.

Definition inverse {M : Type} (S : set M) (s s' : M) (bin : M -> M -> M) :=
    belongs s S ->
    belongs s' S ->
    id S (bin s s') bin /\ id S (bin s' s) bin.

Definition inversible {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
  forall s, exists s', inverse S s s' bin.

Definition associative {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
  forall a b c,
    belongs a S ->
    belongs b S ->
    belongs c S ->
    bin a (bin b c) = bin (bin a b) c.

Definition entire_property {M : Type} (S : set M) (bin : M -> M -> M) : Prop :=
  forall x y, belongs x S -> belongs y S -> belongs (bin x y) S.

Definition magma {M : Type} (S : set M) bin :=
  entire_property S bin.

Definition semigroup {M : Type} (S : set M) bin :=
  magma S bin /\ associative S bin.

Definition monoid {M : Type} (S : set M) bin :=
  semigroup S bin /\ identity S bin.

Axiom monoid_has_id : forall {M:Type} (S : set M) bin,
  monoid S bin -> exists id_S, belongs id_S S /\ id S id_S bin.

Definition group {M : Type} (S : set M) bin :=
  monoid S bin /\ inversible S bin.

Axiom group_inverse_belongs : forall {M:Type} (S : set M) bin,
  forall g g', group S bin -> inverse S g g' bin -> belongs g S /\ belongs g' S.

Definition subgroup {M : Type} (H G : set M) bin :=
  subset H G /\ group H bin /\ group G bin.

Theorem subgroup_eq_condition {M : Type} : forall (H G : set M) bin,
  subset H G ->
  group G bin -> (
    group H bin <-> (
      (forall id_G, id G id_G bin -> belongs id_G H) /\
      entire_property H bin /\
      (forall x, exists x', belongs x H -> inverse H x x' bin) 
    )
  ).
Proof.
  intros H G bin H_subsetHG GisGroup.
  split.
  - (* -> *)
    intros HisGroup.
    split.
    +
      intros id_G H_id_G.
      assert (HisGroup_ := HisGroup).
      unfold group in HisGroup_.
      inversion HisGroup_ as [HisMonoid _]. clear HisGroup_.
      apply monoid_has_id in HisMonoid.
      inversion HisMonoid as [id_H H_identity]. clear HisMonoid.
      (* created id_H *)

      unfold id in H_identity.
      inversion H_identity as [H_idH_in_H H_identity_]. clear H_identity.
      assert (H_idH_in_H_:=H_idH_in_H).
      assert (H_identity__:=H_identity_).
      specialize H_identity_ with id_H.
      apply H_identity_ in H_idH_in_H. clear H_identity_.
      inversion H_idH_in_H as [H_idHidH_eq_idH _]. clear H_idH_in_H.
      (* created bin id_H id_H = id_H *)

      assert (GisGroup_ := GisGroup).
      unfold group,monoid,semigroup,identity,id,inversible in GisGroup_.
      inversion GisGroup_ as [[[_ G_assoc] _] G_inverse]. clear GisGroup_.
      specialize G_inverse with id_H.
      inversion G_inverse as [id_H' G_inverse__]. clear G_inverse.
      (* created id_H' *)

      assert (H_idH'idHidH_eq_idH'idH : bin id_H' (bin id_H id_H) = bin id_H' (id_H))
      by (rewrite H_idHidH_eq_idH; reflexivity).
      (* created bin id_H' (bin id_H id_H) = bin id_H' id_H *)

      assert (G_inverse_:=G_inverse__).
      apply (group_inverse_belongs G bin id_H id_H' GisGroup) in G_inverse__.
      inversion G_inverse__ as [id_H_in_G id_H'_in_G].
      unfold inverse,id in G_inverse_.
      apply (G_inverse_ id_H_in_G) in id_H'_in_G. clear G_inverse_.
      inversion id_H'_in_G as [_ G_inv0]. clear id_H'_in_G.
      specialize G_inv0 with id_G.
      assert (H_id_G__ := H_id_G).
      apply id_belongs in H_id_G__.
      apply G_inv0 in H_id_G__.
      inversion H_id_G__ as [G_inv2_1 G_inv2_2]. clear H_id_G__.
      assert (H_id_G_ := H_id_G).
      unfold id in H_id_G.
      specialize H_id_G with (bin id_H' id_H).
      specialize H_identity__ with id_H'.
      unfold group,monoid,semigroup,magma,entire_property in GisGroup.
      inversion GisGroup as [[[G_entire_prop _] _] _]. clear GisGroup.
      inversion G_inverse__ as [G_inv2 G_inv3].
      assert (G_inv2_:=G_inv2).
      apply (G_entire_prop id_H' id_H G_inv3) in G_inv2.
      apply H_id_G in G_inv2.
      inversion G_inv2 as [_ H_id_G0]. clear G_inv2.
      rewrite H_id_G0 in G_inv2_1.
      rewrite G_inv2_1 in H_idH'idHidH_eq_idH'idH.
      (* created bin id_H' (bin id_H id_H) = id_G *)

      assert (G_inv0_:=G_inv0).
      unfold associative in G_assoc.
      specialize G_assoc with (a:=id_H') (b:=id_H) (c:=id_H).
      assert (G_inv0__:=G_inv0_).
      rewrite (G_assoc G_inv3 G_inv2_ G_inv2_) in H_idH'idHidH_eq_idH'idH.
      (* created bin (bin id_H' id_H) id_H) = id_G *)

      rewrite G_inv2_1 in H_idH'idHidH_eq_idH'idH. 
      (* created bin (bin id_H' id_H) id_H) = id_G *)

      unfold id in H_id_G_.
      specialize H_id_G_ with id_H.
      apply H_id_G_ in id_H_in_G.
      inversion id_H_in_G as [_ idGidH_eq_idH].
      rewrite idGidH_eq_idH in H_idH'idHidH_eq_idH'idH.
      (* created id_H = id_G *)

      rewrite <- H_idH'idHidH_eq_idH'idH.
      assumption.
    +
      split.  
      *
        unfold group,monoid,semigroup,magma in HisGroup.
        inversion HisGroup as [[[H_entire _] _] _].
        assumption.
      *
        intros x_H H_x_H.
        unfold group in HisGroup.
        inversion HisGroup as [_ H_inverse].
        unfold inversible,inverse in H_inverse.
        unfold inverse.
        intros x.
        specialize H_inverse with x.
        inversion H_inverse.
        exists x0.
        intros H1.
        assumption.
  - (* <- *)
    intros H_123.
    unfold group,monoid,semigroup.
    split.
    +
      split.
      *
        split.
        --
           inversion H_123 as [_ [H_entire _]].
           assumption.
        --
           unfold group,monoid,semigroup in GisGroup.
           inversion GisGroup as [[[_ G_assoc] _] _]. clear GisGroup.
           unfold associative in *.
           intros a b c ainH binH cinH.
           specialize G_assoc with a b c.
           apply H_subsetHG in ainH.
           apply H_subsetHG in binH.
           apply H_subsetHG in cinH.
           apply (G_assoc ainH binH) in cinH.
           assumption.
      *
        unfold group,monoid,identity in GisGroup.

        inversion GisGroup as [[_ G_identity] _].
        inversion G_identity as [id_G G_identity_].

        unfold identity.
        exists id_G.

        unfold id in G_identity_.
        unfold id.
        intros s H_s_in_H.
        specialize G_identity_ with s.
        apply H_subsetHG in H_s_in_H.
        apply G_identity_ in H_s_in_H.
        assumption.
    +
      unfold inversible, inverse.
      intros s.
      inversion H_123 as [_ [_ H_3]].
      specialize H_3 with s.
      inversion H_3 as [s'].
      exists s'.
      unfold inverse in H0.
      intros.
      apply (H0 H1 H1 H2).
Qed.