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.

From Coq Require Import ssreflect ssrfun FunctionalExtensionality.
Record Isomorphism (A B : Type) := {
    Forward : A -> B;
    Backward : B -> A;
    BF : cancel Forward Backward;
    FB : cancel Backward Forward;
}.
Infix "<-->" := Isomorphism (at level 95, no associativity).
Definition iso_refl {A : Type} : A <--> A := {|
    Forward x := x;
    Backward x := x;
    BF x := eq_refl;
    FB x := eq_refl;
|}.
Definition iso_sym {A B : Type} (α : A <--> B) : B <--> A := {|
    Forward x := Backward _ _ α x;
    Backward x := Forward _ _ α x;
    BF x := FB _ _ α x;
    FB x := BF _ _ α x;
|}.
Definition iso_trans {A B C : Type} (α : A <--> B) (β : B <--> C) : A <--> C.
Proof.
    refine ({|
        Forward x := Forward _ _ β (Forward _ _ α x);
        Backward x := Backward _ _ α (Backward _ _ β x);
        BF x := _;
        FB x := _;
    |}).
    - by rewrite BF BF.
    - by rewrite FB FB.
Qed.
Definition iso_exp {A B C : Type} (α : A <--> B) : (A -> C) <--> (B -> C).
Proof.
    refine ({|
        Forward f x := f (Backward _ _ α x);
        Backward f x := f (Forward _ _ α x);
        BF f := _;
        FB f := _;
    |}).
    - apply functional_extensionality => x.
        by rewrite BF.
    - apply functional_extensionality => x.
        by rewrite FB.
Qed.

(* https://math.stackexchange.com/questions/3802938/computational-type-theory-for-topos-logic *)
From mathcomp Require Export all_ssreflect ssralg.
Require Export isomorphism atomic weil_algebras axioms basic_infinitesimal_spaces.
Definition fiber {E B} (f : E -> B) : B -> Type
    := fun b => {e : E | f e = b}.
Definition bundle {B} (f : B -> Type) : Type
    := {b : B & f b}.
Definition field {B} (f : B -> Type) : Type
    := forall b : B, f b.
Lemma bundle_fiber {E B} (f : E -> B) : bundle (fiber f) <--> E.
Proof.
    refine({|
        Forward '(existT b (exist e _)) := e;
        Backward e := existT _ (f e) (exist _ e erefl);
    |}).
    - move=> [b [e pf]].
        move: b pf.
        by apply: eq_indd.
    - done.
Defined.
Lemma fiber_bundle {B} {F : B -> Type} {b} 
    : fiber (projT1 (P := _) : bundle F -> B) b <--> F b.
Proof.
    refine({|
        Forward '(exist (existT x f) pf) := eq_rect _ F f _ pf;
        Backward f := exist _ (existT _ b f) erefl;
    |}).
    - move=> [[b' f] pf].
        move: b pf.
        by apply: eq_indd.
    - done.
Defined.
Definition tangent_bundle M := 'D_1 -> M.
Definition tangent M := fiber (fun f : tangent_bundle M => f zero).

From mathcomp Require Import all_ssreflect ssralg.
Require Import isomorphism axioms atomic.
Class Zero T := { zero : T }.
(* The nth-order infinitesimals. *)
Definition nilpotent n := {x : R | x ^+ n = 0}.
Definition nilpotent_union := {x : R | exists n, x ^+ n = 0}.
Notation "''D_' n" := (nilpotent (n.+1))
    (at level 8, n at level 2, format "''D_' n").
Notation "''D_-1'" := (nilpotent 0)
    (at level 8, format "''D_-1'").
Notation "''D_∞'" := nilpotent_union
    (at level 8, format "''D_∞'").
Coercion R_of_nilpotent_union (d : nilpotent_union) : R := proj1_sig d.
Coercion union_of_nilpotent {n} : nilpotent n -> 'D_∞.
    move=> [x pf].
    exists x.
    exists n.
    exact pf.
Defined.
Fact higher_power_still_zero {x : R} {m n} (leq : m <= n)
    : x ^+ m = 0 -> x ^+ n = 0.
Proof.
    rewrite -(subnK leq) exprD => ->.
    apply: mulr0.
Qed.
Definition widen_nilpotent {m n} (leq : m <= n) : nilpotent m -> nilpotent n := 
    fun '(exist x pf) => (exist _ x (higher_power_still_zero leq pf)).
#[refine]
Global Instance D_zero {n} : Zero 'D_n := {
    zero := exist _ 0 _
}.
apply: expr0n.
Defined.
Global Instance nilpotent_union_zero : Zero nilpotent_union := {
    zero := (zero : 'D_0)
}.
Definition d_minus_void_iso : 'D_-1 <--> void.
Proof.
    have: 'D_-1 -> void.
    {
        move=>[x pf].
        rewrite expr0 in pf.
        move: (oner_neq0 R).
        by move /eqP.
    }
    move=> fwd.
    refine ({|
        Forward := fwd;
        Backward := of_void _;
        BF x := match fwd x with end;
        FB x := match x with end;
    |}).
Defined.
Definition polynomial {n} (coeffs : 'I_n -> R) (x : R) : R
    := \prod_(i < n) ((x ^+ i) * coeffs i).
(* Implementation at the bottom of the file. *)
Module Type nilpotent_properties_sig.
    Axiom KL_D : forall {n}, (nilpotent n -> R) <--> ('I_n -> R).
    Axiom KL_D_back : forall {n coeffs} {d : nilpotent n},
        Backward _ _ KL_D coeffs d = polynomial coeffs d.
    Axiom atomicD : forall {n}, Atomic 'D_n.
End nilpotent_properties_sig.
(* Spaces of infinitesimal vectors. *)
(* I think this space acts like a walking simplex? *)
Definition Δ n := {x : 'I_n -> R | forall i j, x i * x j = 0}.
Coercion Rn_of_Δ {n} (d : Δ n) : {ffun 'I_n -> R} := finfun (proj1_sig d).
#[refine]
Global Instance Δ_zero {n} : Zero (Δ n) := {
    zero := exist _ (fun=> 0) (fun _ _ => _)
}.
exact (mul0r 0).
Defined.
Lemma eq_Δ {n} {u v : Δ n} (pf : forall i, u i = v i) : u = v.
    move: u v pf => [u pf_u] [v pf_v] pf.
    rewrite /Rn_of_Δ in pf; simpl in pf.
    have: u = v.
    {
        apply: functional_extensionality => i.
        move: (pf i).
        by rewrite ffunE ffunE.
    }
    move=> tmp. move: tmp pf_v pf => <- pf_v _.
    f_equal.
    apply: proof_irrelevance.
Qed.
Definition Δ1_D_iso_fwd : Δ 1 -> 'D_1 :=
    fun '(exist x pf) => 
        exist _ (x ord0) (Logic.eq_trans (expr2 (x ord0)) (pf ord0 ord0)).
Definition Δ1_D_iso_bwd : 'D_1 -> Δ 1.
    refine(fun '(exist x pf) => exist _ (fun=> x) _).
    by rewrite -expr2 pf.
Defined.
Definition Δ1_D_iso : Δ 1 <--> 'D_1.
Proof.
    refine ({|
        Forward := Δ1_D_iso_fwd;
        Backward := Δ1_D_iso_bwd;
    |}).
    - move=> [x pf].
        apply: eq_Δ => i.
        rewrite /Rn_of_Δ ffunE ffunE; simpl.
        by rewrite ord1.
    - move=> [x pf]; simpl.
        f_equal.
        apply: proof_irrelevance.
Defined.
(* Implementation at the bottom of the file. *)
Module Type Δ_properties_sig.
    Axiom KL_Δ : forall {n}, (Δ n -> R) <--> (R * ('I_n -> R)).
    Axiom KL_Δ_back : forall {n coeffs} {d : Δ n},
        Backward _ _ KL_Δ coeffs d = fst coeffs + \sum_i snd coeffs i * d i.
    Axiom atomicΔ : forall {n}, Atomic (Δ n).
End Δ_properties_sig.
(* Implementation details that involve Weil algebras *)
Require Import weil_algebras.
Module Export nilpotent_properties : nilpotent_properties_sig.
    Definition nilpotent_weil_mul n
    (x : {ffun 'I_n -> R^o}) (y : {ffun 'I_n -> R^o}) : {ffun 'I_n -> R^o} :=
    [ffun k : 'I_n => \sum_(i < n) \sum_(j < n) 
        if (i + j + 1 == k)%N then x i * y j else 0
    ].
    Fact nilpotent_weil_mul_linear n z : linear (nilpotent_weil_mul n z).
    Proof.
        move=> a x y.
        rewrite /nilpotent_weil_mul {2}/*:%R {4}/+%R; simpl.
        rewrite /ffun_scale /ffun_add.
        apply: eq_ffun => k.
        do 3 rewrite ffunE.
        rewrite scaler_sumr -big_split; simpl.
        apply: eq_bigr => i _.
        rewrite scaler_sumr -big_split; simpl.
        apply: eq_bigr => j _.
        case: (i + j + 1 == k)%N.
        + rewrite scalerAr -mulrDr.
            rewrite {1}/*:%R {1}/+%R; simpl.
            by rewrite /ffun_scale /ffun_add ffunE ffunE.
        + by rewrite addr0 scaler0.
    Qed.
    Fact nilpotent_weil_mul_assoc n : associative (nilpotent_weil_mul n).
    Proof.
        move=> x y z.
        apply: eq_ffun => k.
        suff: (\sum_(i < n)\sum_(j < n)\sum_(i' < n)\sum_(j' < n)
            if (i + j + 1 == k)%N && (i' + j' + 1 == j)%N then x i * y i' * z j' else 0)
            = (\sum_(i < n)\sum_(j < n)\sum_(i' < n)\sum_(j' < n)
            if (i + j + 1 == k)%N && (i' + j' + 1 == i)%N then x i' * y j' * z j else 0).
        {
            move=> eq.
            apply: Logic.eq_trans; first (apply: Logic.eq_trans; last apply: eq).
            - apply: eq_bigr => i _.
                apply: eq_bigr => j _.
                case: (i + j + 1 == k)%N.
                + rewrite ffunE mulr_sumr.
                    apply: eq_bigr => i' _.
                    rewrite mulr_sumr.
                    apply: eq_bigr => j' _.
                    case: (i' + j' + 1 == j)%N; simpl.
                    * by rewrite mulrA.
                    * by rewrite mulr0.
                + rewrite big1; first done.
                    move=> i' _.
                    by rewrite big1.
            - apply: eq_bigr => i _.
                apply: eq_bigr => j _.
                case: (i + j + 1 == k)%N.
                + rewrite ffunE mulr_suml.
                    apply: eq_bigr => i' _.
                    rewrite mulr_suml.
                    apply: eq_bigr => j' _.
                    case: (i' + j' + 1 == i)%N; simpl.
                    * done.
                    * by rewrite mul0r.
                + rewrite big1; first done.
                    move=> i' _.
                    by rewrite big1.
        }
        have: forall (P : 'I_n -> bool) F, (forall a b, P a -> P b -> a = b)
            -> (\sum_(i | P i) F i) = if [pick x | P x] is Some x then F x else 0.
        {
            move=> t P F eq.
            case pickP.
            - move=> i pf.
                apply: big_pred1.
                move=> j.
                apply/idP/eqP.
                + move=> pf2.
                    by apply: eq.
                + by move=>->.
            - move=> H.
                by apply: big_pred0.
        }
        move=> lemma.
        suff: (\sum_(i < n)\sum_(i' < n)\sum_(j' < n)
            if (i + (i' + j' + 1) + 1 == k)%N then x i * y i' * z j' else 0)
            = (\sum_(j < n)\sum_(i' < n)\sum_(j' < n)
            if ((i' + j' + 1) + j + 1 == k)%N then x i' * y j' * z j else 0).
        {
            move=> eq.
            apply: Logic.eq_trans; first (apply: Logic.eq_trans; last apply: eq).
            - apply: eq_bigr => i _.
                rewrite exchange_big; apply: eq_bigr => i' _.
                rewrite exchange_big; apply: eq_bigr => j' _.
                rewrite -big_mkcond.
                rewrite lemma.
                + case pickP.
                    * move=> j /andP [/eqP <- /eqP <-].
                        by case eqP.
                    * case: eqP; last done.
                        move=> eq2.
                        suff: (i' + j' + 1)%N < n.
                        {
                            move=> less nope.
                            suff: false by [].
                            rewrite -(nope (Ordinal less)) -eq2; simpl.
                            by apply /andP.
                        }
                        apply: leq_ltn_trans; last exact: ltn_ord k.
                        rewrite -eq2.
                        apply: leq_trans; [apply: leq_addl | apply: leq_addr].
                + move=> [a a_pf] [b b_pf] /andP [/eqP <- /eqP ->] /andP [_ /eqP eq2].
                    simpl in eq2.
                    move: eq2 a_pf => -> a_pf.
                    f_equal.
                    apply: proof_irrelevance.
            - apply: Logic.eq_sym.
                rewrite exchange_big; apply: eq_bigr => j _.
                rewrite exchange_big; apply: eq_bigr => i' _.
                rewrite exchange_big; apply: eq_bigr => j' _.
                rewrite -big_mkcond.
                rewrite lemma.
                + case pickP.
                    * move=> i /andP [/eqP <- /eqP <-].
                        by case eqP.
                    * case: eqP; last done.
                        move=> eq2.
                        suff: (i' + j' + 1)%N < n.
                        {
                            move=> less nope.
                            suff: false by [].
                            rewrite -(nope (Ordinal less)) -eq2; simpl.
                            by apply /andP.
                        }
                        apply: leq_ltn_trans; last exact: ltn_ord k.
                        rewrite -eq2.
                        apply: leq_trans; [apply: leq_addr | apply: leq_addr].
                + move=> [a a_pf] [b b_pf] /andP [/eqP <- /eqP ->] /andP [_ /eqP eq2].
                    simpl in eq2.
                    move: eq2 a_pf => -> a_pf.
                    f_equal.
                    apply: proof_irrelevance.
        }
        apply: Logic.eq_sym.
        rewrite exchange_big; apply: eq_bigr => i _.
        rewrite exchange_big; apply: eq_bigr => i' _.
        apply: eq_bigr => j' _.
        suff: (i + i' + 1 + j')%N = (i + (i' + j' + 1))%N by move=>->.
        do 3 rewrite -addnA; f_equal; f_equal.
        apply: addnC.
    Qed.
    Fact nilpotent_weil_mul_comm n : commutative (nilpotent_weil_mul n).
    Proof.
        move=> x y.
        apply: eq_ffun => k.
        rewrite exchange_big.
        apply: eq_bigr => i _.
        apply: eq_bigr => j _.
        move: (addnC j i) => ->.
        move: (mulrC (x j) (y i)) => ->.
        done.
    Qed.
    Fact nilpotent_weil_mul_nilpotent n x (xs : 'I_n -> _) 
        : \big[nilpotent_weil_mul n/x]_i xs i = 0.
    Proof.
        move: xs.
        suff: forall m xs (mn : m <= n) (i : 'I_n), i < m -> 
            (\big[nilpotent_weil_mul n/x]_(j : 'I_m) xs j) i = 0.
        {
            move=> H xs.
            rewrite -ffunP => i.
            rewrite (H n xs (leqnn n) i (ltn_ord i)).
            by rewrite /0; simpl; rewrite /ffun_zero ffunE.
        }
        elim=> [|m IH] xs mn k pf.
        - done.
        - rewrite big_ord_recl ffunE.
            rewrite big1; first done.
            move=> i _.
            rewrite big1; first done.
            move=> j _.
            case eqP; last done.
            move=> eq.
            suff: (\big[nilpotent_weil_mul n/x]_(i0 < m) 
                xs (lift ord0 i0)) j = 0.
            {
                move=>->.
                apply: mulr0.
            }
            apply: IH.
            - by apply: ltnW.
            - rewrite -ltnS.
                apply: leq_ltn_trans; last apply: pf.
                move: eq => <-.
                rewrite addn1.
                apply leq_addl.
    Qed.
    Definition nilpotent_weil (n : nat) : WeilData R := {|
        Domain := [finType of 'I_n];
        Mul := nilpotent_weil_mul n;
        Lin := nilpotent_weil_mul_linear n;
        Assoc := nilpotent_weil_mul_assoc n;
        Comm := nilpotent_weil_mul_comm n;
        Nilpotent := ex_intro _ _ (nilpotent_weil_mul_nilpotent n);
    |}.
    Definition nilpotent_weil_iso {n} : 'D_n <--> Spec R (Weil (nilpotent_weil n)).
        apply: iso_trans; last apply: reifyIso.
        refine({|
            Forward '(exist x pf) := exist _ [ffun i => x] _;
            Backward '(exist f morph) := exist _ (\sum_i f i) _;
        |}).
    Admitted.
    Definition KL_D {n} : (nilpotent n -> R) <--> ('I_n -> R).
    Admitted.
    Theorem KL_D_back {n coeffs} {d : nilpotent n}
        : Backward _ _ KL_D coeffs d = polynomial coeffs d.
    Admitted.
    Definition atomicD {n} : Atomic 'D_n := {|
        Amazing X := { amazing Spec R (Weil (nilpotent_weil n)), X };
        amaze _ _ := iso_trans (iso_exp (iso_exp nilpotent_weil_iso)) amaze;
    |}.
    
End nilpotent_properties.
Global Instance atomicD {n} : Atomic 'D_n := atomicD.
Module Export Δ_properties : Δ_properties_sig.
    Definition Δ_weil (n : nat) : WeilData R.
    Proof.
        refine ({|
            Domain := [finType of 'I_n];
            Mul := fun _ _ => 0;
            Lin := fun _ _ _ _ => Logic.eq_sym (Logic.eq_trans (addr0 _) (scaler0 _ _));
            Assoc := fun _ _ _ => Logic.eq_refl;
            Comm := fun _ _ => Logic.eq_refl;
            Nilpotent := ex_intro _ [finType of 'I_1] _
        |}).
        move=> x xs.
        apply: big_ord_recl.
    Defined.
    Definition KL_Δ {n} : (Δ n -> R) <--> (R * ('I_n -> R)).
    Admitted.
    Theorem KL_Δ_back {n coeffs} {d : Δ n}
        : Backward _ _ KL_Δ coeffs d = fst coeffs + \sum_i snd coeffs i * d i.
    Admitted.
    Definition atomicΔ {n} : Atomic (Δ n).
    Admitted.
End Δ_properties.
Global Instance atomicΔ {n} : Atomic (Δ n) := atomicΔ.
(* Can this be done?
#[refine]
Global Instance atomicD_union : Atomic 'D_∞ := {|
    Amazing X := _;
    amaze _ _ := _;
|}.
Admitted.
*)

From mathcomp Require Import ssralg ssreflect ssrfun.
Require Import weil_algebras atomic.
From Coq Require Export FunctionalExtensionality ProofIrrelevance Description.
Open Scope R.
Export GRing.Theory.
(* The ring of numbers. *)
Parameter R : comUnitRingType.
Section WeilAxioms.
Variable (W : WeilData R).
Definition Spec (R : ringType) (A : algType R) := {lrmorphism A -> R^o}.
(* Axiom 1W, from *Synthetic Differential Geometry*. *)
Definition KL_inv : Weil W -> (Spec R (Weil W) -> R) := fun a f => f a.
Axiom KL : (Spec R (Weil W) -> R) -> Weil W.
Axiom KL_linv : cancel KL_inv KL.
Axiom KL_rinv : cancel KL KL_inv.
(* Axiom 3, from *Synthetic Differential Geometry*. *)
Axiom atomicAxiom : Atomic (Spec R (Weil W)).
End WeilAxioms.
Global Instance iSpec {W} : Atomic (Spec R (Weil W)) := atomicAxiom W.

From Coq Require Import PropExtensionality FunctionalExtensionality ProofIrrelevance ssreflect.
Require Export isomorphism.
Class Atomic (O : Type) := {
    Amazing : Type -> Type;
    amaze : forall {A B}, ((O -> A) -> B) <--> (A -> Amazing B);
}.
Notation "{ 'amazing' O , X }" := (Amazing (O := O) X)
    (at level 0, format "{ 'amazing' O , X }") : type_scope.
    
#[refine]
Global Instance iUnit : Atomic unit := {
    Amazing T := T;
    amaze _ _ := {|
        Forward f t := f (fun 'tt => t);
        Backward f t := f (t tt);
    |}
}.
Proof.
    - move=> f.
        apply: functional_extensionality => x.
        suff: x = fun 'tt => x tt by move=>->.
        apply: functional_extensionality.
        by move=>[].
    - done.
Qed.

theories/isomorphism.v
theories/atomic.v
theories/weil_algebras.v
theories/axioms.v
theories/basic_infinitesimal_spaces.v
theories/common.v
-R theories iris_internal_logic

Experimenting with synthetic differential geometry.
Useful book on the subject:
- Anders Kock, [Synthetic Differential Geometry](home.imf.au.dk/kock/sdg99.pdf), Cambridge University Press 1981, 2006

# KNOWNTARGETS will not be passed along to CoqMakefile
KNOWNTARGETS := CoqMakefile
# KNOWNFILES will not get implicit targets from the final rule, and so
# depending on them won't invoke the submake
# Warning: These files get declared as PHONY, so any targets depending
# on them always get rebuilt
KNOWNFILES   := Makefile _CoqProject
.DEFAULT_GOAL := invoke-coqmakefile
CoqMakefile: Makefile _CoqProject
	$(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile
invoke-coqmakefile: CoqMakefile
	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
.PHONY: invoke-coqmakefile $(KNOWNFILES)
####################################################################
##                      Your targets here                         ##
####################################################################
# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
	@true

.git
.DS_Store
CoqMakefile
CoqMakefile.conf
*.vo
*.vos
*.vok
*.glob
*.aux
*.d