Require Import Arith ZArith.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac gcd prime binomial sums.

Set Implicit Arguments.

Set Default Proof Using "Type".

Section rings.

  Variable (R : Type) (Rzero Rone : R) (Rplus Rmult Rminus : R R R) (Ropp : R R)
           (R_is_ring : ring_theory Rzero Rone Rplus Rmult Rminus Ropp eq).

  Infix "⊕" := Rplus (at level 50, left associativity).
  Infix "⊗" := Rmult (at level 40, left associativity).

  Notation z := Rzero.
  Notation o := Rone.
  Notation "∸" := Ropp.



  Add Ring Rring : R_is_ring.



  Definition := (R * R * R * R)%type.
  Definition : := (o,z,z,o).
  Definition : := (z,z,z,z).

  Definition : .
  Proof using Rplus.
    intros (((a,b),c),d) (((a',b'),c'),d').
    exact (aa',bb',
           cc',dd').
  Defined.


  Local Infix "⊞" := (at level 50, left associativity).

  Definition : .
  Proof using Ropp.
    intros (((a,b),c),d).
    exact (a,b,
           c,d).
  Defined.


  Local Notation "⊟" := .

  Fact M22_equal (a b c d a' b' c' d' : R) : a = a' b = b' c = c' d = d' (a,b,c,d) = (a',b',c',d').
  Proof. intros; subst; trivial. Qed.

  Fact M22plus_zero : m, m = m.
  Proof using R_is_ring.
    intros (((a,b),c),d); apply M22_equal; ring.
  Qed.


  Fact M22plus_comm : x y, x y = y x.
  Proof using R_is_ring.
    intros (((a,b),c),d) (((a',b'),c'),d'); apply M22_equal; ring.
  Qed.


  Fact M22plus_assoc : x y u, x (y u) = x y u.
  Proof using R_is_ring.
    intros (((a,b),c),d) (((a',b'),c'),d') (((a'',b''),c''),d''); simpl; apply M22_equal; ring.
  Qed.


  Fact M22minus : x, x x = .
  Proof using R_is_ring.
    intros (((a,b),c),d); apply M22_equal; ring.
  Qed.


  Fact M22plus_cancel : x a b, x a = x b a = b.
  Proof using R_is_ring.
    intros x a b H.
    rewrite (M22plus_zero a), (M22minus x), (M22plus_comm x),
             M22plus_assoc, H, M22plus_assoc,
            (M22plus_comm _ x), M22minus, M22plus_zero.
    trivial.
  Qed.


  Theorem M22plus_monoid : monoid_theory .
  Proof using R_is_ring.
    exists.
    + apply M22plus_zero.
    + intro; rewrite M22plus_comm; apply M22plus_zero.
    + intros; apply M22plus_assoc.
  Qed.


  Definition : .
  Proof using Rplus Rmult.
    intros (((a,b),c),d) (((a',b'),c'),d').
    exact (aa' bc' , ab' bd',
           ca' dc' , cb' dd' ).
  Defined.


  Local Infix "⊠" := (at level 40, left associativity).

  Tactic Notation "myauto" integer(n) := do n intros (((?&?)&?)&?); apply M22_equal; ring.

  Fact M22mult_one_l : x, x = x.
  Proof using R_is_ring. myauto 1. Qed.

  Fact M22mult_one_r : x, x = x.
  Proof using R_is_ring. myauto 1. Qed.

  Fact M22mult_assoc : x y u, x (y u) = x y u.
  Proof using R_is_ring. myauto 3. Qed.

  Fact M22_mult_distr_l : x y u, x (yu) = xy xu.
  Proof using R_is_ring. myauto 3. Qed.

  Fact M22_mult_distr_r : x y u, (yu) x = yx ux.
  Proof using R_is_ring. myauto 3. Qed.

  Theorem M22mult_monoid : monoid_theory .
  Proof using R_is_ring.
    exists.
    + apply M22mult_one_l.
    + apply M22mult_one_r.
    + apply M22mult_assoc.
  Qed.


  Fact M22_opp_mult_l : x y, ( x) y = (x y).
  Proof using R_is_ring. myauto 2. Qed.

  Fact M22_opp_mult_r : x y, x (y) = (x y).
  Proof using R_is_ring. myauto 2. Qed.

  Definition M22scal (k : R) : .
  Proof using Rmult.
    intros (((u,v),w),z).
    exact (ku,kv,kw,kz).
  Defined.


  Fact M22scal_mult k1 k2 : x, M22scal (M22scal x) = M22scal () x.
  Proof using R_is_ring. myauto 1. Qed.

  Fact M22scal_PL22 k : x y, M22scal k (x y) = M22scal k x M22scal k y.
  Proof using R_is_ring. myauto 2. Qed.

  Fact M22scal_MI22 : x, M22scal (o) x = x.
  Proof using R_is_ring. myauto 1. Qed.

  Fact M22scal_zero : x, M22scal z x = .
  Proof using R_is_ring. myauto 1. Qed.

  Fact M22scal_MU22_l k : x y, M22scal k (x y) = M22scal k x y.
  Proof using R_is_ring. myauto 2. Qed.

  Fact M22scal_MU22_r k : x y, M22scal k (x y) = x M22scal k y.
  Proof using R_is_ring. myauto 2. Qed.

  Fact mscal_M22scal n x : mscal n x = M22scal (mscal Rplus Rzero n Rone) x.
  Proof using R_is_ring.
    induction n as [ | n IHn ].
    + do 2 rewrite mscal_0; revert x; myauto 1.
    + do 2 rewrite mscal_S.
      rewrite IHn; clear IHn.
      revert x; myauto 1.
  Qed.




  Definition : R.
  Proof using Rplus Rmult Ropp.
    intros (((a,b),c),d).
    exact (ad ∸(bc)).
  Defined.


  Fact Det22_scal k : x, (M22scal k x) = (k k) x.
  Proof using R_is_ring. intros (((?,?),?),?); simpl; ring. Qed.

  Fact Det22_mult : x y, (xy) = x y.
  Proof using R_is_ring. intros (((?,?),?),?) (((?,?),?),?); simpl; ring. Qed.

  Notation expo22 := (mscal ).
  Notation expoR := (mscal Rmult o).

  Fact expo22_scal k n U : expo22 n (M22scal k U) = M22scal (expoR n k) (expo22 n U).
  Proof using R_is_ring.
    induction n as [ | n IHn ].
    + do 3 rewrite mscal_0; apply M22_equal; ring.
    + do 3 rewrite mscal_S.
      rewrite IHn.
      rewrite M22scal_MU22_l, M22scal_MU22_r.
      rewrite M22scal_mult; auto.
  Qed.


  Fact Det22_expo n x : (expo22 n x) = expoR n ( x).
  Proof using R_is_ring.
    induction n as [ | n IHn ].
    + do 2 rewrite mscal_0; simpl; ring.
    + do 2 rewrite mscal_S.
      rewrite Det22_mult, IHn; ring.
  Qed.


  Fact Diag22_expo n x y : expo22 n (x,z,z,y) = (expoR n x,Rzero,Rzero,expoR n y).
  Proof using R_is_ring.
    induction n as [ | n IHn ]; try (simpl; auto; fail).
    do 3 rewrite mscal_S; rewrite IHn.
    apply M22_equal; ring.
  Qed.


  Fact MU22_Diag22 a b c d x y : (a,b,c,d) (x,z,z,y) = (ax,by,cx,dy).
  Proof using R_is_ring. apply M22_equal; ring. Qed.


  Fact M22_proj12 a1 b1 c1 d1 a2 b2 c2 d2 : (,,,) = (,,,) :> = .
  Proof. inversion 1; auto. Qed.

End rings.

Section ring_morphism.

  Variable (X : Type) (zX oX : X) (pX mX : X X X) (oppX : X X)
           (Y : Type) (zY oY : Y) (pY mY : Y Y Y) (oppY : Y Y).

  Variable : X Y.

  Local Notation "〚 x 〛" := ( x).

  Record ring_morphism : Prop := mk_ring_morph {
    morph_z : zX = zY;
    morph_o : oX = oY;
    morph_plus : x y, pX x y = pY x 〛〚 y ;
    morph_mult : x y, mX x y = mY x 〛〚 y ;
    morph_opp : x, oppX x = oppY x ;
  }.

  Hypothesis Hphi : ring_morphism.

  Definition : X Y.
  Proof using .
    intros (((a,b),c),d).
    exact ( a , b ,
            c , d ).
  Defined.


  Tactic Notation "myauto" integer(n) := do n intros (((?&?)&?)&?); apply M22_equal; ring.

  Fact PL22_morph : x y, ( pX x y) = pY ( x) ( y).
  Proof using Hphi.
    destruct Hphi.
    do 2 intros (((?&?)&?)&?); apply M22_equal; auto.
  Qed.


  Fact MU22_morph : x y, ( pX mX x y) = pY mY ( x) ( y).
  Proof using Hphi.
    destruct Hphi as [ ].
    do 2 intros (((?&?)&?)&?); apply M22_equal;
      repeat rewrite ; repeat rewrite ; auto.
  Qed.


  Fact MI22_morph : x, ( oppX x) = oppY ( x).
  Proof using Hphi.
    destruct Hphi as [ ].
    do 1 intros (((?&?)&?)&?); apply M22_equal;
      repeat rewrite ; repeat rewrite ; auto.
  Qed.


  Fact M22scal_morph : k x, (M22scal mX k x) = M22scal mY k ( x).
  Proof using Hphi.
    destruct Hphi as [ ].
    intros k (((?&?)&?)&?); apply M22_equal; auto.
  Qed.


  Fact Det22_morph : x, pX mX oppX x = pY mY oppY ( x).
  Proof using Hphi.
    destruct Hphi as [ ].
    intros (((?&?)&?)&?); simpl.
    rewrite , , , ; auto.
  Qed.


  Fact expo22_morph n x : (mscal ( pX mX) ( zX oX) n x)
                        = mscal ( pY mY) ( zY oY) n ( x).
  Proof using Hphi.
    destruct Hphi as [ ].
    induction n as [ | n IHn ].
    + do 2 rewrite mscal_0; apply M22_equal; auto.
    + do 2 rewrite mscal_S.
      rewrite MU22_morph, IHn; auto.
  Qed.


End ring_morphism.