Require Export Coq.Classes.RelationClasses. Require Import Coq.Logic.Description. Require Export Basic. Require Export BoolExt.
Require Export List. Import ListNotations.
Require Export Lia Lra.
Require Export Ring Field.
Require Import Arith ZArith QArith Qcanon Reals.

Open Scope nat_scope.
Open Scope A_scope.

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable Variables A Aadd Azero Aopp Amul Aone Ainv Adiv Alt.

Ltac split_intro :=
  repeat (try split; try intro).

Fixpoint iterate {A} (f : A -> A) (n : nat) (a0 : A) : A :=
  match n with
  | O => a0
  | S n' => f (iterate f n' a0)
  end.

Section test.
  Context {A} {f : A -> A} (Azero : A).
End test.

Section Instances.
End Instances.

Section Theory.
End Theory.

Section Examples.
End Examples.

Class Dec {A:Type} (Acmp:A->A->Prop) := {
    dec : forall (a b : A), {Acmp a b} + {~(Acmp a b)};
  }.

Arguments dec {A} _ {_} : simpl never.


Definition Aeqdec {A} {AeqDec:Dec (@eq A)} := @dec _ (@eq A) AeqDec.

Section Instances.
  Import Arith ZArith Reals.

  #[export] Instance Dec_list `{Dec _ (@eq A)} : Dec (@eq (list A)).
  Proof. constructor. intros. apply list_eq_dec. apply Aeqdec. Defined.

  Lemma prod_eq_iff : forall {A B} (z1 z2 : A * B),
      z1 = z2 <-> fst z1 = fst z2 /\ snd z1 = snd z2.
  Proof.
    intros A B (a1,b1) (a2,b2). split; intros H; inv H; auto.
    simpl in *; subst. auto.
  Qed.

  Lemma prod_neq_iff : forall {A B} {AeqDec:Dec (@eq A)} {BeqDec:Dec (@eq B)}
                         (z1 z2 : A * B),
      z1 <> z2 <-> fst z1 <> fst z2 \/ snd z1 <> snd z2.
  Proof.
    intros. rewrite prod_eq_iff. split; intros.
    apply not_and_or in H; auto.
    apply or_not_and in H; auto.
  Qed.

End Instances.

Section Dec_theory.

  Context `(HDec: Dec).

  Definition Acmpb (a b : A) : bool := if dec Acmp a b then true else false.

  Lemma Acmpb_true : forall a b, Acmpb a b = true <-> Acmp a b.
  Proof.
    intros. unfold Acmpb. destruct dec; split; intros; auto. easy.
  Qed.

  Lemma Acmpb_false : forall a b, Acmpb a b = false <-> ~(Acmp a b).
  Proof. intros. rewrite <- Acmpb_true. split; solve_bool. Qed.

  Lemma Acmp_reflect : forall a b : A, reflect (Acmp a b) (Acmpb a b).
  Proof. intros. unfold Acmpb. destruct (dec Acmp a b); constructor; auto. Qed.

End Dec_theory.

Hint Resolve
  Nat.add_wd Nat.mul_wd
  : wd.

Class Injective {A B} (phi: A -> B) := {
    injective : forall a1 a2 : A, a1 <> a2 -> phi a1 <> phi a2
  }.

Section theory.
  Context {A B : Type}.

  Definition injective_form2 (phi: A -> B) :=
    forall a1 a2, phi a1 = phi a2 -> a1 = a2.

  Lemma injective_eq_injective_form2 (phi: A -> B) :
    Injective phi <-> injective_form2 phi.
  Proof.
    split; intros.
    - hnf. destruct H as [H]. intros.
      specialize (H a1 a2). apply imply_to_or in H. destruct H.
      + apply NNPP in H. auto.
      + easy.
    - hnf in H. constructor. intros. intro. apply H in H1. easy.
  Qed.

  Lemma injective_preserve_eq : forall (f : A -> B),
      Injective f -> (forall a1 a2, f a1 = f a2 -> a1 = a2).
  Proof.
    intros. apply injective_eq_injective_form2 in H. apply H. auto.
  Qed.

End theory.

Class Surjective {A B} (phi: A -> B) := {
    surjective : forall b, (exists a, phi a = b)
  }.

Class Bijective {A B} (phi: A -> B) := {
    bijInjective :: Injective phi;
    bijSurjective :: Surjective phi
  }.
Coercion bijInjective : Bijective >-> Injective.
Coercion bijSurjective : Bijective >-> Surjective.

Section theory.
  Context {A B : Type}.

  Lemma bij_inverse_exist : forall (phi : A -> B) (Hbij: Bijective phi),
    {psi : B -> A | (forall a : A, psi (phi a) = a) /\ (forall b : B, phi (psi b) = b)}.
  Proof.
    intros. destruct Hbij as [Hinj [Hsurj]].
    apply injective_eq_injective_form2 in Hinj. hnf in *.
    assert (H : forall b, exists! a, phi a = b).
    { intros b.
      destruct (Hsurj b) as [a Ha]. exists a. repeat split; auto.
      intros a' Ha'. apply Hinj. rewrite Ha. auto. }
    apply constructive_definite_description.
    exists (fun b => proj1_sig (constructive_definite_description _ (H b))). split.
    - split.
      + intros a. destruct (constructive_definite_description). simpl. auto.
      + intros b. destruct (constructive_definite_description). simpl. auto.
    - intro psi; intros. apply functional_extensionality.
      intros b. destruct (constructive_definite_description). simpl.
      destruct H0. rewrite <- e. auto.
  Defined.

  Lemma bijective_preserve_eq : forall (f : A -> B),
      Bijective f -> (forall (a1 a2 : A), f a1 = f a2 -> a1 = a2).
  Proof.
    intros. destruct H as [Hinj Hsurj].
    apply injective_preserve_eq in H0; auto.
  Qed.

End theory.

Class Homomorphic {A B}
  (fa : A -> A -> A) (fb : B -> B -> B) (phi: A -> B) := {
    homomorphic : forall (a1 a2 : A), phi (fa a1 a2) = fb (phi a1) (phi a2)
  }.

Class Homomorphism {A B} (fa : A -> A -> A) (fb : B -> B -> B) := {
    homomorphism : exists (phi: A -> B), Homomorphic fa fb phi /\ Surjective phi
  }.

Class Homomorphism2 {A B} (fa ga : A -> A -> A) (fb gb : B -> B -> B) := {
    homomorphism2 : exists (phi: A -> B),
      Homomorphic fa fb phi /\ Homomorphic ga gb phi /\ Surjective phi
  }.

Class Isomorphism {A B} (fa : A -> A -> A) (fb : B -> B -> B) := {
    isomorphism : exists (phi: A -> B), Homomorphic fa fb phi /\ Bijective phi
  }.

Class Isomorphism2 {A B} (fa ga : A -> A -> A) (fb gb : B -> B -> B) := {
    isomorphism2 : exists (phi: A -> B),
      Homomorphic fa fb phi /\ Homomorphic ga gb phi /\ Bijective phi
  }.

Class Subset (C P : Type) := {
    sub_phi : C -> P;
    sub_phi_inj : Injective sub_phi
  }.

Section Instances.

  Instance nat_Z_Subset : Subset nat Z.
  Proof.
    refine (@Build_Subset _ _ Z.of_nat _).
    rewrite injective_eq_injective_form2. hnf. apply Nat2Z.inj.
  Qed.

End Instances.

Section Theory.
End Theory.

Section Examples.
End Examples.

Class Associative {A} (Aop : A -> A -> A) := {
    associative : forall a b c, Aop (Aop a b) c = Aop a (Aop b c);
  }.

#[export] Instance Assoc_NatAdd : Associative Nat.add.
constructor. auto with arith. Defined.

Goal forall a b c : nat, (a + (b + c) = (a + b) + c).
  intros. rewrite associative; auto. Qed.

Goal forall a b c : nat, ((a + b) + c = a + (b + c)).
  apply associative. Qed.

Class Commutative {A} (Aop : A -> A -> A) := {
    commutative : forall a b, Aop a b = Aop b a
  }.

#[export] Instance Comm_NatAdd : Commutative Nat.add.
constructor. auto with arith. Defined.

#[export] Instance Comm_NatMul : Commutative Nat.mul.
constructor. auto with arith. Defined.

Goal forall a b : nat, (a + b = b + a)%nat.
  apply commutative. Qed.

Goal forall a b : nat, (a * b = b * a)%nat.
  apply commutative. Qed.

Class IdentityLeft {A} (Aop : A -> A -> A) (Ae : A) := {
    identityLeft : forall a, Aop Ae a = a
  }.

Class IdentityRight {A} (Aop : A -> A -> A) (Ae : A) := {
    identityRight : forall a, Aop a Ae = a
  }.

Class InverseLeft {A} (Aop : A -> A -> A) (Ae : A) (Aopinv : A -> A)
  := {
    inverseLeft : forall a, Aop (Aopinv a) a = Ae
  }.

Class InverseRight {A} (Aop : A -> A -> A) (Ae : A) (Aopinv : A -> A)
  := {
    inverseRight : forall a, Aop a (Aopinv a) = Ae
  }.

Class DistributiveLeft {A} (Aadd Amul : A -> A -> A) := {
    distributiveLeft : forall a b c,
      Amul a (Aadd b c) = Aadd (Amul a b) (Amul a c)
  }.

Class DistributiveRight {A} (Aadd Amul : A -> A -> A) := {
    distributiveRight : forall a b c,
      Amul (Aadd a b) c = Aadd (Amul a c) (Amul b c)
  }.

Class Order {A} (Alt Ale : A -> A -> Prop) (Altb Aleb : A -> A -> bool) := {
    
    lt_le_cong : forall a b : A, Ale a b <-> (Alt a b \/ a = b);
    
    lt_irrefl : forall a : A, ~ (Alt a a);
    
    lt_antisym : forall a b : A, Alt a b -> Alt b a -> a = b;
    
    lt_trans : forall a b c : A, Alt a b -> Alt b c -> Alt a c;
    
    lt_cases : forall a b : A, {Alt a b} + {Alt b a} + {a = b};
    
    ltb_reflect : forall a b : A, reflect (Alt a b) (Altb a b);
    
    leb_reflect : forall a b : A, reflect (Ale a b) (Aleb a b);
  }.

Section theories.
  Context `{HOrder : Order}.

  Notation "a > b" := (Alt b a).
  Notation "a >= b" := (Ale b a).
  Infix "<" := Alt.
  Infix "<=" := Ale.
  Infix "<?" := Altb.
  Infix "<=?" := Aleb.

  Lemma lt_dec : forall a b, {a < b} + {~(a < b)}.
  Proof.
    intros. destruct (lt_cases a b) as [[H1|H1]|H1]; auto.
    - right. intro. pose proof (lt_trans H1 H). apply lt_irrefl in H0; auto.
    - right. subst. apply lt_irrefl.
  Qed.

  #[export] Instance lt_Dec : Dec Alt.
  Proof. constructor. intro. apply lt_dec. Qed.


  #[export] Instance order_EqDec : Dec (@eq A).
  Proof.
    constructor.
    intros; destruct (lt_cases a b) as [[H1|H1]|H1]; auto.
    - right; intro; subst. apply lt_irrefl in H1; auto.
    - right; intro; subst. apply lt_irrefl in H1; auto.
  Qed.

  Lemma lt_connected : forall a b : A, Alt a b \/ Alt b a \/ a = b.
  Proof. intros. destruct (lt_cases a b) as [[H1|H1]|H1]; auto. Qed.

  Lemma le_if_lt : forall a b : A, a < b -> a <= b.
  Proof. intros. apply lt_le_cong. auto. Qed.

  Lemma lt_if_le_and_neq : forall a b : A, a <= b -> a <> b -> a < b.
  Proof. intros. apply lt_le_cong in H. destruct H; auto. easy. Qed.

  Lemma lt_not_eq : forall a b : A, a < b -> a <> b.
  Proof. intros. intro. subst. apply lt_irrefl in H; auto. Qed.

  Lemma le_refl : forall a : A, a <= a.
  Proof. intros. apply lt_le_cong. right. auto. Qed.

  Lemma le_antisym : forall a b : A, a <= b -> b <= a -> a = b.
  Proof.
    intros. apply lt_le_cong in H, H0. destruct H, H0; subst; auto.
    apply lt_antisym; auto.
  Qed.

  Lemma le_trans : forall a b c : A, a <= b -> b <= c -> a <= c.
  Proof.
    intros. apply lt_le_cong in H, H0. apply lt_le_cong.
    destruct H, H0; subst; auto. left. apply lt_trans with b; auto.
  Qed.

  Lemma lt_trans_lt_le : forall a b c : A, a < b -> b <= c -> a < c.
  Proof.
    intros. pose proof (le_if_lt H). pose proof (le_trans H1 H0).
    apply lt_if_le_and_neq; auto.
    intro. subst. pose proof (le_antisym H0 H1). subst. apply lt_irrefl in H; auto.
  Qed.

  Lemma lt_trans_le_lt : forall a b c : A, a <= b -> b < c -> a < c.
  Proof.
    intros. pose proof (le_if_lt H0). pose proof (le_trans H H1).
    apply lt_if_le_and_neq; auto.
    intro. subst. pose proof (le_antisym H H1). subst. apply lt_irrefl in H0; auto.
  Qed.

  Lemma lt_gt_contr : forall a b : A, a < b -> b < a -> False.
  Proof.
    intros. apply lt_trans with (a:=a) in H0; auto. apply lt_irrefl in H0; auto.
  Qed.

  Lemma lt_imply_neq : forall a b : A, a < b -> a <> b.
  Proof. intros. intro. subst. apply lt_irrefl in H. auto. Qed.

  Lemma lt_not_lt : forall a b : A, a < b -> ~ (b < a).
  Proof. intros. intro. apply lt_gt_contr in H; auto. Qed.

  Lemma lt_not_le : forall a b : A, a < b -> ~ (b <= a).
  Proof.
    intros. rewrite lt_le_cong. apply and_not_or. split.
    apply lt_not_lt; auto. symmetry. apply lt_not_eq; auto.
  Qed.

  Lemma not_le_lt : forall a b : A, ~ (a <= b) -> b < a.
  Proof.
    intros. rewrite lt_le_cong in H. apply not_or_and in H. destruct H.
    destruct (lt_cases a b) as [[H1|H1]|H1]; try easy.
  Qed.

  Lemma le_not_lt : forall a b : A, a <= b -> ~ (b < a).
  Proof.
    intros. rewrite lt_le_cong in H. destruct H.
    apply lt_not_lt; auto. subst. apply lt_irrefl.
  Qed.

  Lemma not_lt_le : forall a b : A, ~ (a < b) -> b <= a.
  Proof.
    intros. apply lt_le_cong.
    destruct (lt_cases a b) as [[H1|H1]|H1]; auto; try easy.
  Qed.

  Lemma le_ge_eq : forall a b : A, a <= b -> b <= a -> a = b.
  Proof.
    intros. apply le_not_lt in H,H0.
    destruct (lt_cases a b) as [[H1|H1]|H1]; easy.
  Qed.

  Lemma le_dec : forall a b : A, {a <= b} + {~(a <= b)}.
  Proof.
    intros. destruct (lt_dec b a); auto.
    - right. apply lt_not_le; auto.
    - left. apply not_lt_le; auto.
  Qed.

  #[export] Instance le_Dec : Dec Ale.
  Proof. constructor; intros. apply le_dec. Qed.

  Lemma le_connected : forall a b : A, a <= b \/ b < a.
  Proof. intros. destruct (le_dec a b); auto. apply not_le_lt in n. auto. Qed.


  Lemma leb_refl : forall a : A, a <=? a = true.
  Proof. intros. destruct (leb_reflect a a); auto. destruct n. apply le_refl. Qed.

End theories.

Class SGroup {A} (Aadd : A -> A -> A) := {
    sgroupAssoc :: Associative Aadd;
  }.

Section Instances.

  #[export] Instance nat_add_SGroup : SGroup Nat.add.
  repeat constructor; auto with wd; try apply eq_equivalence; intros; ring. Qed.

  #[export] Instance nat_mul_SGroup : SGroup Nat.mul.
  repeat constructor; auto with wd; try apply eq_equivalence; intros; ring. Qed.

End Instances.

Ltac sgroup_head f :=
  rewrite ?associative;
  repeat
    (match goal with
     | |- f ?a _ = f ?a _ => apply f_equal2; [reflexivity|]
     end;
     auto).

Ltac sgroup_tail f :=
  rewrite <- ?associative;
  repeat
    (match goal with
     | |- f _ ?a = f _ ?a => apply f_equal2; [|reflexivity]
     end;
     auto).

Ltac sgroup_only f :=
  try (progress (sgroup_head f));
  try (progress (sgroup_tail f)).
Ltac sgroup :=
  match goal with
  | SG : SGroup ?f |- _ => sgroup_only f
  end.

Section test.
  Context `{HSGroup : SGroup}. Infix "+" := Aadd.

  Variable a b c d e f g h i j k : A.

  Goal a + b = a + k. progress sgroup. Abort.
  Goal a + b = k + b. progress sgroup. Abort.

  Goal a + b + c = a + k. progress sgroup. Abort.
  Goal a + b + c = a + b + k. progress sgroup. Abort.
  Goal a + b + c = k + c. progress sgroup. Abort.
  Goal (a + b) + c = k + (b + c). progress sgroup. Abort.

  Goal a + b + c + d = a + k. progress sgroup. Abort.
  Goal a + b + c + d = a + b + k. progress sgroup. Abort.
  Goal a + b + c + d = a + b + c + k. progress sgroup. Abort.
  Goal a + b + c + d = k + d. progress sgroup. Abort.
  Goal a + b + c + d = k + c + d. progress sgroup. Abort.
  Goal a + b + c + d = k + b + c + d. progress sgroup. Abort.

  Goal a + b + c + d + e = a + k. progress sgroup. Abort.
  Goal a + b + c + d + e = a + b + k. progress sgroup. Abort.
  Goal a + b + c + d + e = a + b + c + k. progress sgroup. Abort.
  Goal a + b + c + d + e = a + b + c + d + k. progress sgroup. Abort.
  Goal a + b + c + d + e = k + e. progress sgroup. Abort.
  Goal a + b + c + d + e = k + d + e. progress sgroup. Abort.
  Goal a + b + c + d + e = k + c + d + e. progress sgroup. Abort.
  Goal a + b + c + d + e = k + b + c + d + e. progress sgroup. Abort.
End test.

Class ASGroup {A} (Aadd : A -> A -> A) := {
    asgroupSGroup :: SGroup Aadd;
    asgroupComm :: Commutative Aadd
  }.

Section Instances.

  #[export] Instance nat_add_ASGroup : ASGroup Nat.add.
  repeat constructor; auto with wd; try apply eq_equivalence; intros; ring. Qed.

  #[export] Instance nat_mul_ASGroup : SGroup Nat.mul.
  repeat constructor; auto with wd; try apply eq_equivalence; intros; ring. Qed.

End Instances.

Ltac move2h c :=
  rewrite <- ?associative;
  try rewrite (commutative _ c);
  rewrite ?associative.

Ltac move2t c :=
  rewrite ?associative;
  try rewrite (commutative c);
  rewrite <- ?associative.

Section test.
  Context `{HASGroup : ASGroup}. Infix "+" := Aadd.
  Variable a0 a1 a2 a3 a4 a5 a6 : A.

  Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1.
  Proof. do 2 move2h a0. do 2 move2h a1. do 2 move2h a2. do 2 move2h a3. auto. Qed.

  Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1.
  Proof. do 2 move2t a0. do 2 move2t a1. do 2 move2t a2. do 2 move2t a3. auto. Qed.
End test.

Section try1.

  Ltac elimh1 :=
    rewrite ?associative;
    match goal with
    
    | |- ?f ?c ?a = ?f ?c ?b => f_equal
    end.

  Ltac elimt1 :=
    rewrite <- ?associative;
    match goal with
    | |- ?f ?a ?c = ?f ?b ?c => f_equal
    end.

  Ltac elimh :=
    rewrite ?associative;
    repeat match goal with
      | |- ?aeq (?f ?c _) (?f _ _) => move2h c; elimh1
      | |- ?aeq (?f ?c _) (?f _ _) => move2h c; elimh1
      end.

  Ltac elimt :=
    rewrite <- ?associative;
    repeat match goal with
      | |- ?aeq (?f _ ?c) (?f _ _) => move2t c; elimt1
      end.

  Ltac asgroup :=
    elimh; elimt;
    symmetry;
    elimh; elimt.
  Section test.
    Context `{HASGroup : ASGroup}. Infix "+" := Aadd.
    Variable a0 a1 a2 a3 a4 a5 a6 b1 b2 c1 c2 : A.

    Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1.
    Proof.
      do 2 move2h a0; elimh1.
      do 2 move2h a1; elimh1.
      do 2 move2h a2; elimh1.
    Qed.

    Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1.
    Proof.
      do 2 move2t a0; elimt1.
      do 2 move2t a1; elimt1.
      do 2 move2t a2; elimt1.
    Qed.

    Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1. Proof. elimh. Qed.
    Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1. Proof. elimt. Qed.
    Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1. Proof. symmetry. elimh. Qed.
    Goal a0 + (a1 + a2) + a3 = a3 + (a0 + a2) + a1. Proof. symmetry. elimt. Qed.

    Let eq2 : Prop := a0 + (a1 + a2 + a3) + a4 + a5 = a2 + a0 + a6 + a3 + a4.

    Goal eq2. unfold eq2. elimh. Abort.
    Goal eq2. unfold eq2. elimt. Abort.
    Goal eq2. unfold eq2. symmetry. elimh. Abort.
    Goal eq2. unfold eq2. symmetry. elimt. Abort.
    Goal eq2. unfold eq2. asgroup. Abort.

    Goal b1 + a0 + a1 + b2 = c1 + a1 + a0 + c2.
    Proof.
      progress asgroup.
      progress asgroup.
      progress asgroup.
    Abort.

    Goal b1 + a0 + a1 + b2 = c1 + a1 + a0 + c2.
    Proof.
      intros.
      do 2 move2h a0. asgroup.
      do 2 move2h a1. asgroup.
    Abort.
  End test.

End try1.

Section try2.

  Ltac asgroup :=
    
    rewrite <- ?associative;
    
    repeat
      (match goal with
       
       | |- ?f ?a _ = ?f ?a _ => f_equal
       | |- ?f _ ?a = ?f _ ?a => f_equal
       | |- ?f ?a _ = ?f _ ?a => move2t a
       | |- ?f _ ?a = ?f ?a _ => move2t a
       
       | |- ?f (?f ?a _) _ = ?f ?a _ => move2t a
       | |- ?f (?f ?a _) _ = ?f _ ?a => move2t a
       | |- ?f (?f _ ?a) _ = ?f ?a _ => move2t a
       | |- ?f (?f _ ?a) _ = ?f _ ?a => move2t a
       | |- ?f ?a _ = ?f (?f ?a _) _ => move2t a
       | |- ?f ?a _ = ?f (?f _ ?a) _ => move2t a
       | |- ?f _ ?a = ?f (?f ?a _) _ => move2t a
       | |- ?f _ ?a = ?f (?f _ ?a) _ => move2t a
       | |- ?f (?f ?a _) _ = ?f (?f ?a _) _ => move2t a
       | |- ?f (?f ?a _) _ = ?f (?f _ ?a) _ => move2t a
       | |- ?f (?f _ ?a) _ = ?f (?f ?a _) _ => move2t a
       | |- ?f (?f _ ?a) _ = ?f (?f _ ?a) _ => move2t a
       | |- ?f (?f ?a _) _ = ?f _ (?f ?a _) => move2t a
       | |- ?f (?f ?a _) _ = ?f _ (?f _ ?a) => move2t a
       | |- ?f (?f _ ?a) _ = ?f _ (?f ?a _) => move2t a
       | |- ?f (?f _ ?a) _ = ?f _ (?f _ ?a) => move2t a
       end;
       auto).


  Section test.
    Context `{HASGroup : ASGroup}. Infix "+" := Aadd.
    Variable a0 a1 a2 a3 a4 a5 a6 b1 b2 c1 c2 : A.

    Goal b1 + a0 + b2 = c1 + a0 + c2.
    Proof. asgroup. Abort.
  End test.
End try2.


Ltac asgroup_only f :=
  
  rewrite <- ?associative;
  repeat
    (match goal with
     | |- ?A = ?B =>
         
         match A with
         | context [f ?a ?b] =>
             
             match B with
             | context [f a _] => do 2 move2t a; f_equal
             | context [f _ a] => do 2 move2t a; f_equal
             | context [f b _] => do 2 move2t b; f_equal
             | context [f _ b] => do 2 move2t b; f_equal
             end
         end
     end;
    auto).

Ltac asgroup :=
  match goal with
  | ASG : ASGroup ?f |- _ => asgroup_only f
  end.

Section test.
  Context `{HASGroup : ASGroup}. Infix "+" := Aadd.

  Variable a b c d e f g h i j k : A.

  Goal a + b = a + k. progress asgroup. Abort.
  Goal b + a = k + a. progress asgroup. Abort.
  Goal a + b = k + a. progress asgroup. Abort.
  Goal b + a = a + k. progress asgroup. Abort.

  Goal a + b + c = a + k. progress asgroup. Abort.
  Goal a + b + c = k + a. progress asgroup. Abort.
  Goal a + b + c = b + k. progress asgroup. Abort.
  Goal a + b + c = k + b. progress asgroup. Abort.

  Goal a + b + c + d = a + k. progress asgroup. Abort.
  Goal a + b + c + d = k + a. progress asgroup. Abort.
  Goal a + b + c + d = b + k. progress asgroup. Abort.
  Goal a + b + c + d = k + b. progress asgroup. Abort.

  Goal a + b + c + d + e = a + k. progress asgroup. Abort.
  Goal a + b + c + d + e = k + a. progress asgroup. Abort.
  Goal a + b + c + d + e = b + k. progress asgroup. Abort.
  Goal a + b + c + d + e = k + b. progress asgroup. Abort.

  Goal a + b + c + d + e + f = a + k. progress asgroup. Abort.
  Goal a + b + c + d + e + f = k + a. progress asgroup. Abort.
  Goal a + b + c + d + e + f = b + k. progress asgroup. Abort.
  Goal a + b + c + d + e + f = k + b. progress asgroup. Abort.

  Goal a + k = a + b + c + d + e + f. progress asgroup. Abort.
  Goal k + a = a + b + c + d + e + f. progress asgroup. Abort.
  Goal b + k = a + b + c + d + e + f. progress asgroup. Abort.
  Goal k + b = a + b + c + d + e + f. progress asgroup. Abort.

  Goal forall x1 x2 y1 y2 : A, x1 + a + b + c + x2 = y1 + c + (b + a) + y2.
  Proof. intros. progress asgroup. Abort.
End test.

Class Monoid {A} (Aadd : A -> A -> A) (Azero : A) := {
    monoidAssoc :: Associative Aadd;
    monoidIdL :: IdentityLeft Aadd Azero;
    monoidIdR :: IdentityRight Aadd Azero;
    monoidSGroup :: SGroup Aadd
  }.

Section Instances.

  Import Arith ZArith Qcanon Reals.

  #[export] Instance Monoid_NatAdd : Monoid Nat.add 0%nat.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_NatMul : Monoid Nat.mul 1%nat.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_ZAdd : Monoid Z.add 0%Z.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_ZMul : Monoid Z.mul 1%Z.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_QcAdd : Monoid Qcplus 0.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_QcMul : Monoid Qcmult 1.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_RAdd : Monoid Rplus 0%R.
  repeat constructor; intros; ring. Qed.

  #[export] Instance Monoid_RMul : Monoid Rmult 1%R.
  repeat constructor; intros; ring. Qed.

End Instances.

Section Theory.
  Context `{HMonoid : Monoid}.
  Notation "0" := Azero : A_scope.
  Infix "+" := Aadd : A_scope.

End Theory.

Ltac monoid_only f e :=
  repeat
    (match goal with
     
     | [M:Monoid f e |- context [f ?a e]] => rewrite (identityRight a) at 1
     | [M:Monoid f e, H:context [f ?a e] |- _] => rewrite (identityRight a) in H at 1
     
     | [M:Monoid f e |- context [f e ?a]] => rewrite (identityLeft a) at 1
     | [M:Monoid f e, H:context [f e ?a] |- _] => rewrite (identityLeft a) in H at 1
     end;
     auto).

Ltac monoid :=
  try match goal with
    | M:Monoid ?f ?e |- _ =>
        monoid_only f e;
        try pose proof (@monoidSGroup _ f e M) as HSGroup; sgroup
    end;
  try match goal with
    | SG : SGroup ?f |- _ => sgroup
    end;
  auto.

Section Examples.
  Context `{HMonoid : Monoid}.
  Notation "0" := Azero : A_scope.
  Infix "+" := Aadd : A_scope.

  Goal forall a b c d : A, 0 + a + 0 + (b + 0 + c) = a + (0 + b) + (c + 0).
  Proof. intros. monoid. Qed.

End Examples.