From Coq Require Import FunctionalExtensionality ProofIrrelevance.
From mathcomp Require Import all_ssreflect ssralg.
Require Import isomorphism.

Open Scope R.
Import GRing.Theory.

Section WeilAlgebras.
Variables (R : comRingType).

Record WeilData : Type := {
    Domain : finType;
    Mul : {ffun Domain -> R^o} -> {ffun Domain -> R^o} -> {ffun Domain -> R^o};
    Lin : forall a, linear (Mul a);
    Assoc : associative Mul;
    Comm : commutative Mul;
    Nilpotent : exists T : finType,
        forall (x : {ffun Domain -> R}) (xs : T -> {ffun Domain -> R}),
        \big[Mul/x]_(i : T) (xs i) = 0
}.

Section WeilImpls.

    Variables (W : WeilData).

    Definition weil : Type := R * {ffun (Domain W) -> R^o}.

    Definition wrap (w : R * {ffun Domain W -> R}) : weil := w.
    Definition unwrap (w : weil) : R * {ffun Domain W -> R} := w.
    Lemma wrap_unwrap : cancel wrap unwrap.
        move=> w. by rewrite /wrap /unwrap.
    Qed.

    Canonical weil_eq : eqType := EqType weil (CanEqMixin wrap_unwrap).
    Canonical weil_choice : choiceType := ChoiceType weil (CanChoiceMixin wrap_unwrap).

    Canonical weil_zmodType : zmodType :=
        ZmodType weil (ZmodMixin (@addrA _) (@addrC _) (@add0r _) (@addNr _)).

    Definition weil_mul (x y : weil) : weil :=
        ( fst x * fst y
        , fst x *: snd y + fst y *: snd x + Mul W (snd x) (snd y)
        ).
    Definition weil_one : weil := ( 1 , [ffun=> 0]).
    Fact weil_mulA : associative weil_mul.
    Admitted.
    Fact weil_mulC : commutative weil_mul.
    Admitted.
    Fact weil_mul_1l : left_id weil_one weil_mul.
    Admitted.
    Fact weil_mul_1r : right_id weil_one weil_mul.
    Admitted.
    Fact weil_mul_addl : left_distributive weil_mul +%R.
    Admitted.
    Fact weil_mul_addr : right_distributive weil_mul +%R.
    Admitted.
    Fact weil1_nonzero : weil_one != 0.
    Admitted.

    Canonical weil_ringType : ringType := RingType weil 
        (RingMixin weil_mulA weil_mul_1l weil_mul_1r weil_mul_addl weil_mul_addr weil1_nonzero).

    Canonical weil_comRingType : comRingType := ComRingType weil weil_mulC.

    Definition weil_scale (k : R) (w : weil) : weil
        := (k * fst w, [ffun a => k *: snd w a]).

    Fact weil_scaleA k1 k2 f :
    weil_scale k1 (weil_scale k2 f) = weil_scale (k1 * k2) f.
    Admitted.
    Fact weil_scale1 : left_id 1 weil_scale.
    Admitted.
    Fact weil_scale_addr k : {morph (weil_scale k) : x y / x + y}.
    Admitted.
    Fact weil_scale_addl u : {morph (weil_scale)^~ u : k1 k2 / k1 + k2}.
    Admitted.

    Canonical weil_lmodType : lmodType R := 
        LmodType R weil (LmodMixin weil_scaleA weil_scale1 weil_scale_addr weil_scale_addl).

    Fact weil_scaleAl (a : R) (u v : weil) : a *: (u * v) = (a *: u) * v.
    Admitted.

    Fact weil_scaleAr (a : R) (u v : weil) : a *: (u * v) = u * (a *: v).
    Admitted.

    Canonical weil_lalgType : lalgType R := LalgType R weil weil_scaleAl.
    Canonical weil_algType : algType R := AlgType R weil weil_scaleAr.
    Canonical weil_comAlgType : comAlgType R := [comAlgType R of weil].

End WeilImpls.

End WeilAlgebras.

Definition Weil {R} W := weil_comAlgType R W.





Definition WeilMorph {R} (W : WeilData R) (A : algType R) : Type :=
    {f : {ffun (Domain R W) -> A} 
    | {morph (fun (x : {ffun _ -> R^o}) => \sum_(i : Domain R W) (x i *: f i)) 
        : x y / Mul R W x y >-> x * y
    }}.


Module Export IsoImpl.
(* The proofs below are a mess, but they work. *)

Section reify.

    Context {R} {W : WeilData R} {A : algType R} (m : WeilMorph W A).

    Definition reify : Weil W -> A :=
        let '(exist dom_f morph) := m in
        fun '(x, dx) => x%:A + (\sum_i dx i *: dom_f i).

    Fact reify_is_additive : additive reify.
    Proof.
        rewrite /reify; move: m => [dom_f morph].
        move=> [x dx] [y dy]. simpl.
        rewrite scalerDl -addrA -addrA; f_equal.
        rewrite opprD addrA [_ - y%:A]addrC -addrA scaleNr; f_equal.
        rewrite -sumrB.
        apply: eq_bigr => i _.
        rewrite -scaleNr -scalerDl; f_equal.
        by rewrite {1}/+%R {1}/-%R; simpl; rewrite /ffun_add /ffun_opp ffunE ffunE.
    Qed.

    Canonical reify_additive := Additive reify_is_additive.

    Fact reify_is_multiplicative : multiplicative reify.
    Proof.
        rewrite /reify; move: m => [dom_f morph].
        split.
        - move=> [x dx] [y dy]. simpl.
            rewrite mulrDr mulrDl mulrDl.
            rewrite -morph.
            rewrite -[x%:A*_+_+_]addrA -scalerAl -scalerAr scalerA mulr1; f_equal.
            rewrite mulr_suml mulr_sumr -big_split -big_split; simpl.
            apply: eq_bigr => i _.
            rewrite -scalerAr mulr1 scalerA.
            rewrite -scalerAl mul1r scalerA.
            rewrite -scalerDl -scalerDl addrA; f_equal.
            rewrite {1 2}/+%R {1 2}/*:%R; simpl; rewrite /ffun_add /ffun_scale.
            do 4 rewrite ffunE; f_equal.
            by rewrite addrC /*:%R; simpl.
        - simpl.
            rewrite big1.
            + by rewrite addr0 scale1r.
            + by move=> i _; rewrite ffunE scale0r.
    Qed.

    Canonical reify_multiplicative := AddRMorphism reify_is_multiplicative.

    Fact reify_is_scalable : scalable reify.
    Proof.
        rewrite /reify; move: m => [dom_f morph].
        move=> k [x dx]. simpl.
        rewrite scalerDr scalerA; f_equal.
        rewrite scaler_sumr.
        apply: eq_bigr => i _.
        by rewrite ffunE scalerA.
    Qed.

    Canonical reify_linear := AddLinear reify_is_scalable.

    Definition LR_of_WeilMorph : {lrmorphism (Weil W) -> A}
        := [lrmorphism of reify].

End reify.

Definition unreify {R} {W : WeilData R} {A : algType R}
    (f : {lrmorphism (Weil W) -> A}) : {ffun Domain R W -> A}
    := [ffun i => f (0, [ffun j => if i == j then 1 else 0])].

Lemma unreify_morph {R} {W : WeilData R} {A : algType R}
    (f : {lrmorphism (Weil W) -> A}) :
    { morph 
        (fun x : {ffun Domain R W -> R^o} => \sum_i x i *: (unreify f) i) 
        : x y / Mul R W x y >-> x * y
    }.
Proof.
    move=> x y.

    have: forall (g : Domain R W -> R^o), 
        (\sum_i g i *: (unreify f) i) = f (0, [ffun i => g i]).
    {
        move=> g.
        have: \sum_i g i *: (unreify f) i = \sum_i f (0, [ffun j => if i == j then g i else 0]).
        {
            apply: eq_bigr => i _.
            rewrite /(unreify f) ffunE -linearZ_LR.
            rewrite /*:%R; simpl; rewrite /weil_scale; simpl.
            rewrite mulr0; f_equal; f_equal.
            apply: eq_ffun => j.
            rewrite ffunE.
            case: (i == j).
            + by rewrite /*:%R; simpl; rewrite mulr1.
            + by rewrite scaler0.
        }
        move=>->.
        rewrite -linear_sum.
        apply: f_equal.
        have: \sum_i (0, [ffun j => if i == j then g i else 0])
            = (0, \sum_i [ffun j => if i == j then g i else 0]).
        {
            move=> t.
            elim/big_rec2 : _ => // [i da [b db] _ ->].
            rewrite /+%R; simpl; rewrite /add_pair /ffun_add; simpl.
            rewrite addr0.
            done.
        }
        move=>->.
        f_equal.

        rewrite -ffunP => i.
        rewrite ffunE sum_ffunE.

        have: \sum_k [ffun j => if k == j then g k else 0] i
            = \sum_k if k == i then g k else 0
            by apply: eq_bigr => k _; rewrite ffunE.
        move=>->.

        rewrite -big_mkcond; simpl.
        by rewrite big_pred1_eq.
    }
    move=> lemma; rewrite lemma lemma lemma; clear lemma.
    rewrite -rmorphM.
    rewrite /*%R; simpl; rewrite /weil_mul; simpl.
    rewrite mul0r scale0r scale0r add0r add0r.
    f_equal; f_equal.

    have: forall (g : {ffun Domain R W -> R^o}), [ffun i => g i] = g.
    {
        move=> g.
        apply ffunP => i.
        by rewrite ffunE.
    }
    by move=> lemma; rewrite lemma lemma lemma; clear lemma.
Qed.

Definition WeilMorph_of_LR {R} {W : WeilData R} {A : algType R}
    (f : {lrmorphism (Weil W) -> A}) : WeilMorph W A
    := exist _ (unreify f) (unreify_morph f).

Theorem LR_W_LR {R} {W : WeilData R} {A : algType R}
    : cancel WeilMorph_of_LR (@LR_of_WeilMorph R W A).
    move=> m.
    have: forall w, LR_of_WeilMorph (WeilMorph_of_LR m) w = m w.
    {
        move=> [x dx]. simpl.
        rewrite /unreify.

        have: \sum_i dx i *: [ffun i0 => m (0, [ffun j => if i0 == j then 1 else 0])] i
            = \sum_i m (0, dx i *: [ffun j => if i == j then 1 else 0]).
        {
            apply: eq_bigr => i _; rewrite ffunE -linearZ_LR.
            rewrite {3}/*:%R; simpl; rewrite /weil_scale; simpl.
            rewrite mulr0.
            f_equal; f_equal.
        }
        move=>->.
        rewrite -linear_sum.

        have: \sum_i (0, dx i *: [ffun j => if i == j then 1 : R^o else 0])
            = (0, \sum_i dx i *: [ffun j => if i == j then 1 : R^o else 0]).
        {
            move=> t.
            elim/big_rec2 : _ => // [i da [b db] _ ->].
            rewrite /+%R; simpl; rewrite /add_pair /ffun_add; simpl.
            rewrite addr0.
            done.
        }
        move=>->.

        have: x%:A = m (x%:A) by rewrite linearZ_LR rmorph1.
        move=>->.

        rewrite -linearD.
        rewrite {3}/*:%R; simpl; rewrite /weil_scale; simpl.
        apply: f_equal.
        rewrite pair_equal_spec; split; simpl.
        - by rewrite addr0 mulr1.
        - rewrite -ffunP => i.

            rewrite ffunE ffunE ffunE.
            rewrite scaler0 add0r sum_ffunE.
            have: \sum_k (dx k *: [ffun j => if k == j then 1 : R^o else 0]) i
                = \sum_k (if k == i then dx k else 0).
            {
                apply: eq_bigr => k _.
                rewrite /*:%R; simpl; rewrite /ffun_scale ffunE ffunE.
                rewrite /*:%R; simpl.
                case: (k == i).
                - by rewrite mulr1.
                - by rewrite mulr0.
            }
            move=>->.

            rewrite -big_mkcond; simpl.
            by rewrite big_pred1_eq.
    }
    move /functional_extensionality.

    case: (LR_of_WeilMorph (WeilMorph_of_LR m)) => f1 pf1.
    case: m => f2 pf2.
    simpl.
    move=> eq; move: eq pf1 pf2 => -> pf1 pf2.
    by move: (proof_irrelevance _ pf1 pf2) => ->.
Qed.

Theorem W_LR_W {R} {W : WeilData R} {A : algType R}
    : cancel (@LR_of_WeilMorph R W A) WeilMorph_of_LR.
    move=> [dom_f morph].
    apply: eq_sig; simpl.
    {
        rewrite /unreify; simpl.
        rewrite -ffunP => i.
        rewrite ffunE.
        rewrite scale0r add0r .

        have: \sum_k [ffun j => if i == j then 1 else 0] k *: dom_f k
            = \sum_k if k == i then dom_f k else 0.
        {
            apply: eq_bigr => k _.
            rewrite ffunE.
            rewrite eq_sym.
            case: (k == i).
            - by rewrite scale1r.
            - by rewrite scale0r.
        }
        move=>->.
        rewrite -big_mkcond; simpl.
        by rewrite big_pred1_eq.
    }
    move=> H.
    apply proof_irrelevance.
Qed.

Definition reifyIso {R} {W : WeilData R} {A : algType R} :
    WeilMorph W A <--> {lrmorphism Weil W -> A} := {|
    Forward := LR_of_WeilMorph;
    Backward := WeilMorph_of_LR;
    BF := W_LR_W;
    FB := LR_W_LR;
|}.

End IsoImpl.