text:
Require Import Reals utils.RealAdd.
Require Import Coquelicot.Hierarchy.
Require Import Morphisms Equivalence.
Require Import Lra.
Require Import utils.Utils.
Require Import List.
(* For const *)
Require Export Program.Basics.
Require Import Coquelicot.Coquelicot.

Set Bullet Behavior "Strict Subproofs".

Local Open Scope R.
Section rels.
  Context {Ts:Type}.

  Definition rv_le :=
    pointwise_relation Ts Rle.

  Global Instance rv_le_pre : PreOrder rv_le.
  Proof.
    unfold rv_le.
    constructor; intros.
    - intros ??; lra.
    - intros ??????.
      eapply Rle_trans; eauto.
  Qed.

  Global Instance rv_le_part : PartialOrder rv_eq rv_le.
  Proof.
    intros ??.
    split; intros eqq.
    - repeat red.
      repeat red in eqq.
      split; intros ?; rewrite eqq; lra.
    - destruct eqq as [le1 le2].
      intros y.
      specialize (le1 y).
      specialize (le2 y).
      lra.
  Qed.

  Definition Rbar_rv_le := pointwise_relation Ts Rbar_le.

  Global Instance Rbar_rv_le_pre : PreOrder Rbar_rv_le.
  Proof.
    unfold Rbar_rv_le.
    constructor; intros.
    - intros ??; apply Rbar_le_refl.
    - intros ??????.
      eapply Rbar_le_trans; eauto.
  Qed.

  Global Instance Rbar_rv_le_part : PartialOrder rv_eq Rbar_rv_le.
  Proof.
    intros ??.
    split; intros eqq.
    - repeat red.
      repeat red in eqq.
      split; intros ?; rewrite eqq; apply Rbar_le_refl.
    - destruct eqq as [le1 le2].
      intros y.
      specialize (le1 y).
      specialize (le2 y).
      now apply Rbar_le_antisym.
  Qed.

End rels.

Section defs.
  Context {Ts:Type}.

  Section funs.

    (* const is defined in Program.Basics *)

    Definition EventIndicator {P : Ts->Prop} (dec:forall x, {P x} + {~ P x}) : Ts -> R
      := fun omega => if dec omega then 1 else 0.

    Definition rvplus (rv_X1 rv_X2 : Ts -> R) :=
      (fun omega =>  (rv_X1 omega) + (rv_X2 omega)).

    Definition rvsum (Xn : nat -> Ts -> R) (n : nat) :=
      (fun omega => sum_n (fun n0 => Xn n0 omega) n).

    Definition rvscale (c:R) (rv_X : Ts -> R) :=
      fun omega => c * (rv_X omega).

    Definition rvopp (rv_X : Ts -> R) := rvscale (-1) rv_X.

    Definition rvminus (rv_X1 rv_X2 : Ts -> R) :=
      rvplus rv_X1 (rvopp rv_X2).

    Definition rvmult (rv_X1 rv_X2 : Ts -> R) :=
      fun omega => (rv_X1 omega) * (rv_X2 omega).

    Definition rvsqr (rv_X : Ts -> R) := fun omega => Rsqr (rv_X omega).
    Definition rvsqrt (rv_X : Ts -> R) := fun omega => sqrt (rv_X omega).

    Definition rvpow (rv_X : Ts -> R) (n:nat) := fun omega => pow (rv_X omega) n.

    Definition rvpower (rv_X1 rv_X2 : Ts -> R) := fun omega => power (rv_X1 omega) (rv_X2 omega).

    Definition rvabs  (rv_X : Ts -> R) := fun omega => Rabs (rv_X omega).

    Definition rvsign (rv_X : Ts -> R) := fun omega => sign(rv_X omega).

    Lemma rvabs_pos (rv_X : Ts -> R) :
      rv_le (const 0) (rvabs rv_X).
    Proof.
      intro x.
      unfold const, rvabs.
      apply Rabs_pos.
    Qed.

    Definition rvchoice (c:Ts -> bool) (rv_X1 rv_X2 : Ts -> R)
      := fun omega => if c omega then  rv_X1 omega else rv_X2 omega.

    Definition Rbar_rvchoice (c:Ts -> bool) (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => if c omega then  rv_X1 omega else rv_X2 omega.

    Definition bvmin_choice (rv_X1 rv_X2:Ts -> R) : Ts -> bool
      := fun omega => if Rle_dec (rv_X1 omega) (rv_X2 omega) then true else false.

    Definition Rbar_bvmin_choice (rv_X1 rv_X2:Ts -> Rbar) : Ts -> bool
      := fun omega => if Rbar_le_dec (rv_X1 omega) (rv_X2 omega) then true else false.

    Definition bvmax_choice (rv_X1 rv_X2:Ts -> R) : Ts -> bool
      := fun omega => if Rle_dec (rv_X1 omega) (rv_X2 omega) then false else true.

    Definition Rbar_bvmax_choice (rv_X1 rv_X2:Ts -> Rbar) : Ts -> bool
      := fun omega => if Rbar_le_dec (rv_X1 omega) (rv_X2 omega) then false else true.

    Definition rvmax  (rv_X1 rv_X2 : Ts -> R)
      := fun omega => Rmax (rv_X1 omega) (rv_X2 omega).

    Definition Rbar_rvmax  (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => Rbar_max (rv_X1 omega) (rv_X2 omega).

    Definition rvmin  (rv_X1 rv_X2 : Ts -> R)
      := fun omega => Rmin (rv_X1 omega) (rv_X2 omega).

    Definition Rbar_rvmin  (rv_X1 rv_X2 : Ts -> Rbar)
      := fun omega => Rbar_min (rv_X1 omega) (rv_X2 omega).

    Definition rvmaxlist (X : nat -> Ts -> R) (N : nat) : Ts -> R :=
      fun (omega : Ts) => Rmax_list_map (List.seq 0 (S N)) (fun n => X n omega).

    Program Definition pos_fun_part {Ts:Type} (f : Ts -> R) : (Ts -> nonnegreal) :=
      fun x => mknonnegreal (Rmax (f x) 0) _.
    Next Obligation.
      apply Rmax_r.
    Defined.

    Program Definition neg_fun_part {Ts:Type} (f : Ts -> R) : (Ts -> nonnegreal) :=
      fun x => mknonnegreal (Rmax (- f x) 0) _.
    Next Obligation.
      apply Rmax_r.
    Defined.

    Definition rvclip {Ts:Type} (f : Ts -> R) (c : nonnegreal) : Ts -> R
      := fun x => if Rgt_dec (f x) c then c else
                    (if Rlt_dec (f x) (-c) then (-c) else f x).

    Lemma rvclip_le_c (rv_X : Ts -> R) (c : nonnegreal) :
      rv_le (rvclip rv_X c) (const c).
    Proof.
      intro x0.
      unfold rvclip, const.
      assert (0 <= c) by apply (cond_nonneg c).
      match_destr; [lra |].
      match_destr; lra.
    Qed.

    Lemma rvclip_negc_le (rv_X : Ts -> R) (c : nonnegreal) :
      rv_le (const (-c)) (rvclip rv_X c).
    Proof.
      intro x0.
      unfold rvclip, const.
      assert (0 <= c) by apply (cond_nonneg c).
      match_destr; [lra |].
      match_destr; lra.
    Qed.

    Lemma rvclip_abs_bounded rv_X c :
      forall omega : Ts, Rabs ((rvclip rv_X c) omega) <= c.
    Proof.
      intros.
      assert (0 <= c) by apply (cond_nonneg c).
      unfold rvclip.
      match_destr.
      rewrite Rabs_pos_eq; lra.
      match_destr.
      rewrite Rabs_Ropp.
      rewrite Rabs_pos_eq; lra.
      apply Rabs_le.
      lra.
    Qed.

    Lemma rvclip_abs_le_c (rv_X : Ts -> R) (c : nonnegreal) :
      rv_le (rvabs (rvclip rv_X c)) (const c).
    Proof.
      intro x.
      unfold rvabs, const.
      apply rvclip_abs_bounded.
    Qed.

  End funs.

  Section eqs.
    Existing Instance rv_eq_equiv.

    Global Instance rvplus_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvplus.
    Proof.
      unfold rv_eq, rvplus, pointwise_relation.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvscale_proper : Proper (eq ==> rv_eq ==> rv_eq ) rvscale.
    Proof.
      unfold rv_eq, rvopp, Proper, rvscale, respectful, pointwise_relation.
      intros ??? x y eqq z.
      subst.
      now rewrite eqq.
    Qed.

    Global Instance rvopp_proper : Proper (rv_eq ==> rv_eq ) rvopp.
    Proof.
      unfold rv_eq, rvopp, Proper, rvscale, respectful, pointwise_relation.
      intros x y eqq z.
      now rewrite eqq.
    Qed.

    Global Instance rvminus_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvminus.
    Proof.
      unfold rv_eq, rvminus, rvplus, rvopp, rvscale, pointwise_relation.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvmult_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvmult.
    Proof.
      unfold rv_eq, rvmult.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvsqr_proper : Proper (rv_eq ==> rv_eq) rvsqr.
    Proof.
      unfold rv_eq, rvsqr, Proper, respectful, pointwise_relation.
      intros x y eqq z.
      unfold Rsqr.
      rewrite eqq.
      trivial.
    Qed.

    Global Instance rvpow_proper : Proper (rv_eq ==> eq ==> rv_eq) rvpow.
    Proof.
      unfold rv_eq, rvpow, Proper, respectful, pointwise_relation.
      intros x y eqq z ???.
      subst.
      rewrite eqq.
      trivial.
    Qed.

    Global Instance rvpower_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvpower.
    Proof.
      unfold rv_eq, rvpower, Proper, respectful, pointwise_relation.
      intros x y eqq1 z ? eqq2 ?.
      subst.
      now rewrite eqq1, eqq2.
    Qed.

    Global Instance rvabs_proper : Proper (rv_eq ==> rv_eq) rvabs.
    Proof.
      unfold rv_eq, rvabs, Proper, respectful, pointwise_relation.
      intros x y eqq z.
      unfold Rabs.
      rewrite eqq.
      trivial.
    Qed.

    Global Instance rvmax_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvmax.
    Proof.
      unfold rv_eq, rvmax.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvmin_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) rvmin.
    Proof.
      unfold rv_eq, rvmin.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance Rbar_rvmax_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) Rbar_rvmax.
    Proof.
      unfold rv_eq, Rbar_rvmax.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance Rbar_rvmin_proper : Proper (rv_eq ==> rv_eq ==> rv_eq) Rbar_rvmin.
    Proof.
      unfold rv_eq, Rbar_rvmin.
      intros ???????.
      now rewrite H, H0.
    Qed.

    Global Instance rvsign_proper : Proper (rv_eq ==> rv_eq) rvsign.
    Proof.
      unfold rvsign.
      intros ????.
      now rewrite H.
    Qed.

    Local Open Scope equiv_scope.
    Lemma rv_pos_neg_id (rv_X:Ts->R) : rv_X === rvplus (pos_fun_part rv_X) (rvopp (neg_fun_part rv_X)).
    Proof.
      intros x.
      unfold rvplus, rvopp, pos_fun_part, neg_fun_part, rvscale; simpl.
      unfold Rmax, Rmin.
      repeat match_destr; lra.
    Qed.

    Lemma rv_pos_neg_abs (rv_X:Ts->R) : rvabs rv_X === rvplus (pos_fun_part rv_X) (neg_fun_part rv_X).
    Proof.
      intros x.
      unfold rvplus, rvabs, pos_fun_part, neg_fun_part; simpl.
      unfold Rabs, Rmax, Rmin.
      repeat match_destr; lra.
    Qed.

    Lemma rvmult_assoc
          (rv_X1 rv_X2 rv_X3 : Ts -> R) :
      (rvmult (rvmult rv_X1 rv_X2) rv_X3) === (rvmult rv_X1 (rvmult rv_X2 rv_X3)).
    Proof.
      intros x.
      unfold rvmult.
      lra.
    Qed.

    Lemma rvmult_comm
          (rv_X1 rv_X2 : Ts -> R) :
      (rvmult rv_X1 rv_X2)  === (rvmult rv_X2 rv_X1).
    Proof.
      intros x.
      unfold rvmult.
      lra.
    Qed.

    Lemma rvmult_rvadd_distr
          (rv_X1 rv_X2 rv_X3 : Ts -> R) :
      (rvmult rv_X1 (rvplus rv_X2 rv_X3)) ===
                                          (rvplus (rvmult rv_X1 rv_X2) (rvmult rv_X1 rv_X3)).
    Proof.
      intros x.
      unfold rvmult, rvplus.
      lra.
    Qed.

    Lemma rvsum_distr_r {n} (X : nat -> Ts -> R) (f : Ts -> R) :
      rv_eq (rvsum (fun j => rvmult (X j) f) n) (rvmult (rvsum X n) f).
    Proof.
      intro x; unfold rvsum, rvmult.
      induction n.
      - rewrite sum_O.
        now rewrite sum_O.
      - rewrite sum_Sn.
        rewrite sum_Sn.
        unfold plus; simpl.
        rewrite IHn.
        lra.
    Qed.

    Lemma pos_fun_part_le rv_X : rv_le (fun x : Ts => pos_fun_part rv_X x) (rvabs rv_X).
    Proof.
      intros ?.
      unfold rvabs, pos_fun_part, Rabs, Rmax; simpl.
      repeat match_destr; lra.
    Qed.

    Lemma neg_fun_part_le rv_X : rv_le (fun x : Ts => (neg_fun_part rv_X x)) (rvabs rv_X).
    Proof.
      intros ?.
      unfold rvabs, rvopp, rvscale, neg_fun_part, Rabs, Rmax; simpl.
      repeat match_destr; lra.
    Qed.

    Lemma rv_le_pos_fun_part rv_X1 rv_X2 :
      rv_le rv_X1 rv_X2 ->
      rv_le (fun x : Ts => pos_fun_part rv_X1 x) (fun x : Ts => pos_fun_part rv_X2 x).
    Proof.
      intros le12 a.
      simpl.
      now apply Rle_max_compat_r.
    Qed.

    Lemma rv_le_neg_fun_part rv_X1 rv_X2 :
      rv_le rv_X1 rv_X2 ->
      rv_le (fun x : Ts => neg_fun_part rv_X2 x) (fun x : Ts => neg_fun_part rv_X1 x).
    Proof.
      intros le12 a.
      simpl.
      replace 0 with (- 0) by lra.
      repeat rewrite Rcomplements.Rmax_opp_Rmin.
      apply Ropp_le_contravar.
      now apply Rle_min_compat_r.
    Qed.

    Lemma rvmax_unfold (f g:Ts->R) :
      rvmax f g === rvscale (/2) (rvplus (rvplus f g) (rvabs (rvminus f g))).
    Proof.
      intro x.
      unfold rvmax, rvminus, rvscale, rvabs, rvopp, rvscale, rvplus.
      unfold Rmax, Rabs.
      repeat match_destr; lra.
    Qed.

    Lemma rvmin_unfold (f g:Ts->R) :
      rvmin f g === rvscale (/2) (rvminus (rvplus f g) (rvabs (rvminus f g))).
    Proof.
      intro x.
      unfold rvmin, rvminus, rvscale, rvabs, rvopp, rvscale, rvplus.
      unfold Rmin, Rabs.
      repeat match_destr; try lra.
    Qed.

    Lemma rvmult_unfold (f g:Ts->R) :
      rvmult f g === rvscale (1/4) (rvminus (rvsqr (rvplus f g))
                                            (rvsqr (rvminus f g))).
    Proof.
      intros x.
      unfold rvmult, rvminus, rvplus,rvsqr, rvopp, rvscale.
      replace (1 / 4 * ((f x + g x)² + -1 * (f x + -1 * g x)²)) with ((f x)*(g x)) by (unfold Rsqr; lra).
      intuition.
    Qed.

    Lemma rvsqr_unfold (f:Ts->R) :
      rvsqr f === rvpow f 2.
    Proof.
      intros x.
      unfold rvpow, rvsqr, Rsqr; simpl.
      lra.
    Qed.

    Lemma rvsqr_rvsign_nonzero (f : Ts -> R):
      (forall omega, 0 <> f omega) -> rvsqr (rvsign f) === const 1.
    Proof.
      intros H omega.
      unfold rvsqr,rvsign,const.
      destruct (Rle_dec (f omega) 0).
      + destruct r as [H1 | H2].
        -- generalize (sign_eq_m1 _ H1); intros; (rewrite H0).
           unfold Rsqr; lra.
        -- rewrite H2. specialize (H omega). congruence.
      + apply Rnot_le_gt in n.
        generalize (sign_eq_1 _ n); intros; rewrite H0.
        unfold Rsqr; lra.
    Qed.

    Lemma rvpower_abs2_unfold (f:Ts->R) :
      rvpower (rvabs f) (const 2) === rvsqr f.
    Proof.
      intros x.
      apply power_abs2_sqr.
    Qed.

    Lemma rvpower_abs_scale c (X:Ts->R) n :
      rvpower (rvscale (Rabs c) (rvabs X)) (const n) === rvscale (power (Rabs c) n) (rvpower (rvabs X) (const n)).
    Proof.
      intros x.
      unfold rvpower, rvscale.
      rewrite power_mult_distr; trivial.
      - apply Rabs_pos.
      - apply rvabs_pos.
    Qed.

    Lemma rv_abs_abs (rv_X:Ts->R) :
      rv_eq (rvabs (rvabs rv_X)) (rvabs rv_X).
    Proof.
      intros a.
      unfold rvabs.
      now rewrite Rabs_Rabsolu.
    Qed.

    Lemma rvpowabs_choice_le c (rv_X1 rv_X2 : Ts -> R) p :
      rv_le (rvpower (rvabs (rvchoice c rv_X1 rv_X2)) (const p))
            (rvplus (rvpower (rvabs rv_X1) (const p)) (rvpower (rvabs rv_X2) (const p))).
    Proof.
      intros a.
      unfold rvpower, rvabs, rvchoice, rvplus, const; simpl.
      match_destr.
      - assert (0 <= power (Rabs (rv_X2 a)) p) by apply power_nonneg.
        lra.
      - assert (0 <= power (Rabs (rv_X1 a)) p) by apply power_nonneg.
        lra.
    Qed.

    Lemma pos_fun_part_unfold (f : Ts->R) :
      (fun x => nonneg (pos_fun_part f x)) === rvmax f (const 0).
    Proof.
      intros x.
      reflexivity.
    Qed.

    Lemma neg_fun_part_unfold (f : Ts->R) :
      (fun x => nonneg (neg_fun_part f x)) === rvmax (rvopp f) (const 0).
    Proof.
      intros x.
      unfold neg_fun_part, rvopp, const, rvscale, rvmax; simpl.
      f_equal.
      lra.
    Qed.

    Lemma rvmin_choice (rv_X1 rv_X2 : Ts -> R)
      : rvmin rv_X1 rv_X2 === rvchoice (bvmin_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold rvmin, rvchoice, bvmin_choice, Rmin.
      match_destr.
    Qed.

    Lemma Rbar_rvmin_choice (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rvmin rv_X1 rv_X2 === Rbar_rvchoice (Rbar_bvmin_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold Rbar_rvmin, Rbar_rvchoice, Rbar_bvmin_choice, Rbar_min, Rmin.
      destruct (Rbar_le_dec (rv_X1 a) (rv_X2 a))
      ; destruct (rv_X1 a)
      ; destruct (rv_X2 a)
      ; simpl; repeat match_destr; simpl in *; trivial; try lra.
    Qed.

    Lemma rvmax_choice (rv_X1 rv_X2 : Ts -> R)
      : rvmax rv_X1 rv_X2 === rvchoice (bvmax_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold rvmax, rvchoice, bvmax_choice, Rmax.
      match_destr.
    Qed.

    Lemma Rbar_rvmax_choice (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rvmax rv_X1 rv_X2 === Rbar_rvchoice (Rbar_bvmax_choice rv_X1 rv_X2) rv_X1 rv_X2.
    Proof.
      intros a.
      unfold Rbar_rvmax, Rbar_rvchoice, Rbar_bvmax_choice, Rbar_max, Rmax.
      destruct (Rbar_le_dec (rv_X1 a) (rv_X2 a))
      ; destruct (rv_X1 a)
      ; destruct (rv_X2 a)
      ; simpl; repeat match_destr; simpl in *; trivial; try lra.
    Qed.

    Lemma rvchoice_le_max (c:Ts->bool) (rv_X1 rv_X2 : Ts -> R)
      : rv_le (rvchoice c rv_X1 rv_X2) (rvmax rv_X1 rv_X2).
    Proof.
      intros a.
      unfold rvchoice, rvmax, Rmax.
      repeat match_destr; lra.
    Qed.

    Lemma Rbar_rvchoice_le_max (c:Ts->bool) (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rv_le (Rbar_rvchoice c rv_X1 rv_X2) (Rbar_rvmax rv_X1 rv_X2).
    Proof.
      intros a.
      unfold Rbar_rvchoice, Rbar_rvmax, Rbar_max, Rmax.
      repeat match_destr; trivial; try lra
      ; try apply Rbar_le_refl.
      apply Rbar_not_le_lt in n.
      now apply Rbar_lt_le.
    Qed.

    Lemma rvchoice_le_min (c:Ts->bool) (rv_X1 rv_X2 : Ts -> R)
      : rv_le (rvmin rv_X1 rv_X2) (rvchoice c rv_X1 rv_X2).
    Proof.
      intros a.
      unfold rvchoice, rvmin, Rmin.
      repeat match_destr; lra.
    Qed.

    Lemma Rbar_rvchoice_le_min (c:Ts->bool) (rv_X1 rv_X2 : Ts -> Rbar)
      : Rbar_rv_le (Rbar_rvmin rv_X1 rv_X2) (Rbar_rvchoice c rv_X1 rv_X2).
    Proof.
      intros a.
      unfold Rbar_rvchoice, Rbar_rvmin, Rbar_min, Rmin.
      repeat match_destr; simpl in *; trivial; try lra
      ; try apply Rbar_le_refl.
    Qed.

    Lemma rvminus_self (x:Ts->R) : rv_eq (rvminus x x) (const 0).
    Proof.
      intros a.
      unfold rvminus, rvplus, rvopp, rvscale, const.
      lra.
    Qed.

    Lemma rvminus_unfold (x y : Ts -> R)
      : rv_eq (rvminus x y)  (fun a => x a - y a).
    Proof.
      unfold rvminus, rvplus, rvopp, rvscale.
      intros a.
      lra.
    Qed.

    Lemma rvabs_rvminus_sym (x y : Ts -> R) :
      rv_eq (rvabs (rvminus x y)) (rvabs (rvminus y x)).
    Proof.
      repeat rewrite rvminus_unfold.
      unfold rvabs.
      intros a.
      apply Rabs_minus_sym.
    Qed.

    Lemma rvabs_pow1 (x:Ts->R) : rv_eq (rvpower (rvabs x) (const 1)) (rvabs x).
    Proof.
      intros a.
      unfold rvpower, rvabs, const.
      apply power_1.
      apply Rabs_pos.
    Qed.

    Lemma rv_abs_scale_eq (c:R) (rv_X:Ts->R) :
      rv_eq (rvabs (rvscale c rv_X)) (rvscale (Rabs c) (rvabs rv_X)).
    Proof.
      intros a.
      unfold rvabs, rvscale.
      apply Rabs_mult.
    Qed.

    Lemma rv_abs_const_eq (c:R)  :
      rv_eq (Ts:=Ts) (rvabs (const c)) (const (Rabs c)).
    Proof.
      intros a.
      reflexivity.
    Qed.

    Lemma rvpow_mult_distr (x y:Ts->R) n :
      rv_eq (rvpow (rvmult x y) n) (rvmult (rvpow x n) (rvpow y n)).
    Proof.
      intros a.
      unfold rvpow, rvmult.
      apply Rpow_mult_distr.
    Qed.

    Lemma rvpow_scale c (X:Ts->R) n :
      rv_eq (rvpow (rvscale c X) n) (rvscale (pow c n) (rvpow X n)).
    Proof.
      intros x.
      unfold rvpow, rvscale.
      apply Rpow_mult_distr.
    Qed.

    Lemma rvpow_const c n :
      rv_eq (Ts:=Ts) (rvpow (const c) n) (const (pow c n)).
    Proof.
      intros x.
      reflexivity.
    Qed.

    Lemma rvpower_const b e :
      rv_eq (Ts:=Ts) (rvpower (const b) (const e)) (const (power b e)).
    Proof.
      reflexivity.
    Qed.

    Lemma fold_right_rvplus c (l:list (Ts->R)) (a:Ts) :
      fold_right rvplus (const c) l a =
      fold_right Rplus c (map (fun x => x a) l).
    Proof.
      unfold rvplus, const.
      induction l; simpl; trivial.
      now rewrite IHl.
  Qed.

      Lemma rvabs_bound (rv_X : Ts -> R) :
    rv_le (rvabs rv_X) (rvplus (rvsqr rv_X) (const 1)).
  Proof.
    assert (forall x, 0 <= (rvsqr (rvplus (rvabs rv_X) (const (-1)))) x) by (intros; apply Rle_0_sqr).

    assert (rv_eq (rvsqr (rvplus (rvabs rv_X) (const (-1))))
                  (rvplus
                     (rvplus (rvsqr (rvabs rv_X)) (rvscale (-2) (rvabs rv_X)))
                     (const 1))).
    {
      intro x.
      unfold rvsqr, rvplus, rvscale, rvabs, const, Rsqr.
      now ring_simplify.
    }
    intros x.
    specialize (H x).
    rewrite H0 in H.
    unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, rvabs, const in *.
    rewrite Rsqr_abs.
    unfold Rsqr in *.
    apply Rplus_le_compat_l with (r := 2 * Rabs (rv_X x)) in H.
    ring_simplify in H.
    generalize (Rabs_pos (rv_X x)); intros.
    lra.
  Qed.

  Lemma rvabs_sqr (rv_X : Ts -> R) :
    rv_eq (rvabs (rvsqr rv_X)) (rvsqr rv_X).
    Proof.
      intro x.
      unfold rvabs, rvsqr.
      apply Rabs_pos_eq.
      apply Rle_0_sqr.
    Qed.

  Lemma rvsqr_abs (rv_X : Ts -> R) :
    rv_eq (rvsqr (rvabs rv_X)) (rvsqr rv_X).
    Proof.
      intro x.
      unfold rvabs, rvsqr.
      now rewrite <- Rsqr_abs.
    Qed.

    Lemma rvmult_abs (rv_X1 rv_X2 : Ts -> R):
      rv_eq (rvabs (rvmult rv_X1 rv_X2)) (rvmult (rvabs rv_X1) (rvabs rv_X2)).
    Proof.
      intro x.
      unfold rvmult, rvabs.
      apply Rabs_mult.
    Qed.

    Lemma rvprod_bound (rv_X1 rv_X2 : Ts->R) :
      rv_le (rvscale 2 (rvmult rv_X1 rv_X2))
            (rvplus (rvsqr rv_X1) (rvsqr rv_X2)).
    Proof.
      assert (forall x, 0 <= (rvsqr (rvminus rv_X1 rv_X2)) x) by (intros; apply Rle_0_sqr).
      assert (rv_eq (rvsqr (rvminus rv_X1 rv_X2))
                  (rvplus (rvplus (rvsqr rv_X1) (rvopp (rvscale 2 (rvmult rv_X1 rv_X2))))
                          (rvsqr rv_X2))).
    {
      intro x.
      unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr.
      now ring_simplify.
    }
    intros x; specialize (H x).
    rewrite H0 in H; clear H0.
    unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr in *.
    lra.
  Qed.

  Lemma rvprod_abs_bound (rv_X1 rv_X2 : Ts->R) :
    rv_le (rvscale 2 (rvabs (rvmult rv_X1 rv_X2)))
                          (rvplus (rvsqr rv_X1) (rvsqr rv_X2)).
  Proof.
    generalize (rvprod_bound (rvabs rv_X1) (rvabs rv_X2)); intros.
    do 2 rewrite rvsqr_abs in H.
    now rewrite rvmult_abs.
  Qed.

  Lemma rvsum_sqr_bound (rv_X1 rv_X2 : Ts->R) :
    rv_le (rvsqr (rvplus rv_X1 rv_X2))
                          (rvscale 2 (rvplus (rvsqr rv_X1) (rvsqr rv_X2))).
  Proof.
    assert (forall x, 0 <= (rvsqr (rvminus rv_X1 rv_X2)) x) by (intros; apply Rle_0_sqr).
    assert (rv_eq (rvsqr (rvminus rv_X1 rv_X2))
                  (rvplus (rvplus (rvsqr rv_X1) (rvopp (rvscale 2 (rvmult rv_X1 rv_X2))))
                          (rvsqr rv_X2))).
    {
      intro x.
      unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr.
      now ring_simplify.
    }
    intros x; specialize (H x).
    rewrite H0 in H; clear H0.
    unfold rvsqr, rvminus, rvplus, rvmult, rvopp, rvscale, Rsqr in *.
    apply Rplus_le_compat_l with (r:= ((rv_X1 x + rv_X2 x) * (rv_X1 x + rv_X2 x))) in H.
    ring_simplify in H.
    ring_simplify.
    apply H.
  Qed.

  Lemma rvsqr_eq (x:Ts->R): rv_eq (rvsqr x) (rvmult x x).
  Proof.
    intros ?.
    reflexivity.
  Qed.

  Lemma rvprod_abs1_bound (rv_X1 rv_X2 : Ts->R) :
    rv_le (rvabs (rvmult rv_X1 rv_X2))
                          (rvplus (rvsqr rv_X1) (rvsqr rv_X2)).
  Proof.
    generalize (rvprod_abs_bound rv_X1 rv_X2).
    unfold rv_le, rvscale, rvabs, rvmult, rvsqr, Rsqr; intros H x.
    specialize (H x).
    assert (Rabs (rv_X1 x * rv_X2 x) <= 2 * Rabs (rv_X1 x * rv_X2 x)).
    apply Rplus_le_reg_l with (r := - Rabs(rv_X1 x * rv_X2 x)).
    ring_simplify.
    apply Rabs_pos.
    lra.
  Qed.

    Lemma Rbar_Rabs_lim_sum_le0 (f : nat -> Ts -> R) (x : Ts) :
    is_finite (Lim_seq (sum_n (fun n=> Rabs (f n x)))) ->
    Rbar_le
      (Rbar_abs (Lim_seq (fun n => (rvsum f) n x)))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    intros.
    apply series_abs_bounded in H.
    generalize H; intros HH.
    generalize (ex_series_Rabs (fun n => (f n x)) H); intros.
    generalize (Series_Rabs (fun n => (f n x)) H); intros.
    unfold rvsum, rvabs.
    apply ex_series_Lim_seq in H.
    apply ex_series_Lim_seq in H0.
    replace (Lim_seq
               (fun n : nat => sum_n (fun n0 : nat => f n0 x) n))
      with (Finite ( Series (fun n : nat => f n x))).
    replace (Lim_seq
          (fun n : nat =>
             sum_n (fun n0 : nat => Rabs (f n0 x)) n))
      with (Finite (Series (fun n : nat => Rabs (f n x)))).
    simpl.
    apply Rge_le.
    rewrite Rabs_right.
    apply Rle_ge, H1.
    apply Rle_ge, Series_nonneg; trivial.
    intros.
    apply Rabs_pos.
  Qed.

  Lemma Rabs_lim_sum_le0 (f : nat -> Ts -> R) (x : Ts) :
    is_finite (Lim_seq (sum_n (fun n=> Rabs (f n x)))) ->
    Rbar_le
      (Rbar_abs (Finite (real (Lim_seq (fun n => (rvsum f) n x)))))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    intros.
    apply series_abs_bounded in H.
    generalize H; intros HH.
    generalize (ex_series_Rabs (fun n => (f n x)) H); intros.
    generalize (Series_Rabs (fun n => (f n x)) H); intros.
    unfold rvsum, rvabs.
    apply ex_series_Lim_seq in H.
    apply ex_series_Lim_seq in H0.
    replace (Lim_seq
               (fun n : nat => sum_n (fun n0 : nat => f n0 x) n))
      with (Finite ( Series (fun n : nat => f n x))).
    replace (Lim_seq
          (fun n : nat =>
             sum_n (fun n0 : nat => Rabs (f n0 x)) n))
      with (Finite (Series (fun n : nat => Rabs (f n x)))).
    simpl.
    apply Rge_le.
    rewrite Rabs_right.
    apply Rle_ge, H1.
    apply Rle_ge, Series_nonneg; trivial.
    intros.
    apply Rabs_pos.
  Qed.

    Lemma Rbar_Rabs_lim_sum_le (f : nat -> Ts -> R) (x : Ts) :
    Rbar_le
      (Rbar_abs (Lim_seq (fun n => (rvsum f) n x)))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    case_eq (Lim_seq
          (fun n : nat =>
           rvsum (fun n0 : nat => rvabs (f n0)) n x)); intros.
    - rewrite <- H.
      apply Rbar_Rabs_lim_sum_le0.
      unfold rvsum, rvabs in H.
      replace  (Lim_seq (sum_n (fun n : nat => Rabs (f n x))))
        with
           (Lim_seq
              (fun n : nat =>
                 sum_n (fun n0 : nat => Rabs (f n0 x)) n)).
      now rewrite H.
      apply Lim_seq_ext.
      intros; trivial.
    - destruct (Lim_seq (fun n : nat => rvsum f n x)); now simpl.
    - assert (Rbar_le 0 (Lim_seq
        (fun n : nat =>
         rvsum (fun n0 : nat => rvabs (f n0)) n x))).
      + apply Lim_seq_pos.
        intros.
        unfold rvsum, rvabs.
        apply sum_n_nneg.
        intros.
        apply Rabs_pos.
      + rewrite H in H0.
        now simpl in H0.
  Qed.

  Lemma Rabs_lim_sum_le (f : nat -> Ts -> R) (x : Ts) :
    Rbar_le
      (Rbar_abs (Finite (real (Lim_seq (fun n => (rvsum f) n x)))))
      (Rbar_abs (Lim_seq (fun n => (rvsum (fun n0 => (rvabs (f n0))) n x)))).
  Proof.
    case_eq (Lim_seq
          (fun n : nat =>
           rvsum (fun n0 : nat => rvabs (f n0)) n x)); intros.
    - rewrite <- H.
      apply Rabs_lim_sum_le0.
      unfold rvsum, rvabs in H.
      replace  (Lim_seq (sum_n (fun n : nat => Rabs (f n x))))
        with
           (Lim_seq
              (fun n : nat =>
                 sum_n (fun n0 : nat => Rabs (f n0 x)) n)).
      now rewrite H.
      apply Lim_seq_ext.
      intros; trivial.
    - destruct (Lim_seq (fun n : nat => rvsum f n x)); now simpl.
    - assert (Rbar_le 0 (Lim_seq
        (fun n : nat =>
         rvsum (fun n0 : nat => rvabs (f n0)) n x))).
      + apply Lim_seq_pos.
        intros.
        unfold rvsum, rvabs.
        apply sum_n_nneg.
        intros.
        apply Rabs_pos.
      + rewrite H in H0.
        now simpl in H0.
  Qed.

  End eqs.
End defs.

Ltac rv_unfold := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax,
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvminus,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult in *.

Ltac rv_unfold'_in_star := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax,
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult in *; repeat rewrite rvminus_unfold in *.

Tactic Notation "rv_unfold'" "in" "*" := rv_unfold'_in_star.

Ltac rv_unfold'_goal := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax,
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult; repeat rewrite rvminus_unfold.

Tactic Notation "rv_unfold'" := rv_unfold'_goal.

Ltac rv_unfold'_in_hyp H := unfold
                    const,
                  id,
                  compose,
                  EventIndicator,
                  rvsqr,
                  rvpow,
                  rvpower,
                  rvsign,
                  rvabs,
                  rvmax,
                  rvmin,
                  rvchoice,
                  bvmin_choice,
                  bvmax_choice,
                  pos_fun_part,
                  neg_fun_part,
                  rvopp,
                  rvscale,
                  rvplus,
                  rvmult in H; repeat rewrite rvminus_unfold in H.

Tactic Notation "rv_unfold'" "in" hyp(H) := rv_unfold'_in_hyp H.

author: IBM

repo: FormalML

save_path: github-repos/coq/IBM-FormalML


text:
Require Import TestSuite.admit.
Module FirstComment.
  Set Implicit Arguments.
  Generalizable All Variables.
  Set Asymmetric Patterns.
  Set Universe Polymorphism.

  Reserved Notation "x # y" (at level 40, left associativity).
  Reserved Notation "x #m y" (at level 40, left associativity).

  Delimit Scope object_scope with object.
  Delimit Scope morphism_scope with morphism.
  Delimit Scope category_scope with category.

  Record Category (obj : Type) :=
    {
      Object :> _ := obj;
      Morphism : obj -> obj -> Type;

      Identity : forall x, Morphism x x;
      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
    }.

  Bind Scope object_scope with Object.
  Bind Scope morphism_scope with Morphism.

  Arguments Object {obj%type} C%category / : rename.
  Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
  Arguments Identity {obj%type} [!C%category] x%object : rename.
  Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.

  Bind Scope category_scope with Category.

  Record Functor
         `(C : @Category objC)
         `(D : @Category objD)
    := {
        ObjectOf :> objC -> objD;
        MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
      }.

  Record NaturalTransformation
         `(C : @Category objC)
         `(D : @Category objD)
         (F G : Functor C D)
    := {
        ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
      }.

  Definition ProductCategory
             `(C : @Category objC)
             `(D : @Category objD)
  : @Category (objC * objD)%type.
    refine (@Build_Category _
                            (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
                            (fun o => (Identity (fst o), Identity (snd o)))
                            (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).

  Defined.

  Infix "*" := ProductCategory : category_scope.

  Record IsomorphismOf `{C : @Category objC} {s d} (m : C.(Morphism) s d) :=
    {
      IsomorphismOf_Morphism :> C.(Morphism) s d := m;
      Inverse : C.(Morphism) d s
    }.

  Record NaturalIsomorphism
         `(C : @Category objC)
         `(D : @Category objD)
         (F G : Functor C D)
    := {
        NaturalIsomorphism_Transformation :> NaturalTransformation F G;
        NaturalIsomorphism_Isomorphism : forall x : objC, IsomorphismOf (NaturalIsomorphism_Transformation x)
      }.

  Section PreMonoidalCategory.
    Context `(C : @Category objC).

    Variable TensorProduct : Functor (C * C) C.

    Let src {C : @Category objC} {s d} (_ : Morphism C s d) := s.
    Let dst {C : @Category objC} {s d} (_ : Morphism C s d) := d.

    Local Notation "A # B" := (TensorProduct (A, B)).
    Local Notation "A #m B" := (TensorProduct.(MorphismOf) ((@src _ _ _ A, @src _ _ _ B)) ((@dst _ _ _ A, @dst _ _ _ B)) (A, B)%morphism).

    Let TriMonoidalProductL_ObjectOf (abc : C * C * C) : C :=
      (fst (fst abc) # snd (fst abc)) # snd abc.

    Let TriMonoidalProductR_ObjectOf (abc : C * C * C) : C :=
      fst (fst abc) # (snd (fst abc) # snd abc).

    Let TriMonoidalProductL_MorphismOf (s d : C * C * C) (m : Morphism (C * C * C) s d) :
      Morphism C (TriMonoidalProductL_ObjectOf s) (TriMonoidalProductL_ObjectOf d).
    Admitted.

    Let TriMonoidalProductR_MorphismOf (s d : C * C * C) (m : Morphism (C * C * C) s d) :
      Morphism C (TriMonoidalProductR_ObjectOf s) (TriMonoidalProductR_ObjectOf d).
    Admitted.

    Definition TriMonoidalProductL : Functor (C * C * C) C.
      refine (Build_Functor (C * C * C) C
                            TriMonoidalProductL_ObjectOf
                            TriMonoidalProductL_MorphismOf).
    Defined.

    Definition TriMonoidalProductR : Functor (C * C * C) C.
      refine (Build_Functor (C * C * C) C
                            TriMonoidalProductR_ObjectOf
                            TriMonoidalProductR_MorphismOf).
    Defined.

    Variable Associator : NaturalIsomorphism TriMonoidalProductL TriMonoidalProductR.

    Section AssociatorCoherenceCondition.
      Variables a b c d : C.

      (* going from top-left *)
      Let AssociatorCoherenceConditionT0 : Morphism C (((a # b) # c) # d) ((a # (b # c)) # d)
        := Associator (a, b, c) #m Identity (C := C) d.
      Let AssociatorCoherenceConditionT1 : Morphism C ((a # (b # c)) # d) (a # ((b # c) # d))
        := Associator (a, b # c, d).
      Let AssociatorCoherenceConditionT2 : Morphism C (a # ((b # c) # d)) (a # (b # (c # d)))
        := Identity (C := C) a #m Associator (b, c, d).
      Let AssociatorCoherenceConditionB0 : Morphism C (((a # b) # c) # d) ((a # b) # (c # d))
        := Associator (a # b, c, d).
      Let AssociatorCoherenceConditionB1 : Morphism C ((a # b) # (c # d)) (a # (b # (c # d)))
        := Associator (a, b, c # d).

      Definition AssociatorCoherenceCondition' :=
        Compose AssociatorCoherenceConditionT2 (Compose AssociatorCoherenceConditionT1 AssociatorCoherenceConditionT0)
        = Compose AssociatorCoherenceConditionB1 AssociatorCoherenceConditionB0.
    End AssociatorCoherenceCondition.

    Definition AssociatorCoherenceCondition := Eval unfold AssociatorCoherenceCondition' in
                                                forall a b c d : C, AssociatorCoherenceCondition' a b c d.
  End PreMonoidalCategory.

  Section MonoidalCategory.
    Variable objC : Type.

    Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.

    Record MonoidalCategory :=
      {
        MonoidalUnderlyingCategory :> @Category objC;
        TensorProduct : Functor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory;
        IdentityObject : objC;
        Associator : NaturalIsomorphism (TriMonoidalProductL TensorProduct) (TriMonoidalProductR TensorProduct);
        AssociatorCoherent : AssociatorCoherenceCondition' Associator
      }.
  End MonoidalCategory.

  Section EnrichedCategory.
    Context `(M : @MonoidalCategory objM).
    Let x : M := IdentityObject M.
    (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report.  *)
  End EnrichedCategory.
End FirstComment.

Module SecondComment.
  Set Implicit Arguments.
  Set Universe Polymorphism.
  Generalizable All Variables.

  Record prod (A B : Type) := pair { fst : A; snd : B }.
  Arguments fst {A B} _.
  Arguments snd {A B} _.
  Infix "*" := prod : type_scope.
  Notation " ( x , y ) " := (@pair _ _ x y).
  Record Category (obj : Type) :=
    Build_Category {
        Object :> _ := obj;
        Morphism : obj -> obj -> Type;

        Identity : forall x, Morphism x x;
        Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
      }.

  Arguments Identity {obj%type} [!C] x : rename.
  Arguments Compose {obj%type} [!C s d d'] m1 m2 : rename.

  Record > Category' :=
    {
      LSObject : Type;

      LSUnderlyingCategory :> @Category LSObject
    }.

  Section Functor.
    Context `(C : @Category objC).
    Context `(D : @Category objD).

    Record Functor :=
      {
        ObjectOf :> objC -> objD;
        MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
      }.
  End Functor.

  Arguments MorphismOf {objC%type} [C] {objD%type} [D] F [s d] m : rename, simpl nomatch.

  Section FunctorComposition.
    Context `(C : @Category objC).
    Context `(D : @Category objD).
    Context `(E : @Category objE).

    Definition ComposeFunctors (G : Functor D E) (F : Functor C D) : Functor C E.
    Admitted.
  End FunctorComposition.

  Section IdentityFunctor.
    Context `(C : @Category objC).

    Definition IdentityFunctor : Functor C C.
      refine {| ObjectOf := (fun x => x);
                MorphismOf := (fun _ _ x => x)
             |}.
    Defined.
  End IdentityFunctor.

  Section ProductCategory.
    Context `(C : @Category objC).
    Context `(D : @Category objD).

    Definition ProductCategory : @Category (objC * objD)%type.
      refine (@Build_Category _
                              (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
                              (fun o => (Identity (fst o), Identity (snd o)))
                              (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).
    Defined.
  End ProductCategory.

  Definition OppositeCategory `(C : @Category objC) : Category objC :=
    @Build_Category objC
                    (fun s d => Morphism C d s)
                    (Identity (C := C))
                    (fun _ _ _ m1 m2 => Compose m2 m1).

  Parameter FunctorCategory : forall `(C : @Category objC) `(D : @Category objD), @Category (Functor C D).

  Parameter TerminalCategory : Category unit.

  Section ComputableCategory.
    Variable I : Type.
    Variable Index2Object : I -> Type.
    Variable Index2Cat : forall i : I, @Category (@Index2Object i).

    Local Coercion Index2Cat : I >-> Category.

    Definition ComputableCategory : @Category I.
      refine (@Build_Category _
                              (fun C D : I => Functor C D)
                              (fun o : I => IdentityFunctor o)
                              (fun C D E : I => ComposeFunctors (C := C) (D := D) (E := E))).
    Defined.
  End ComputableCategory.

  Section SmallCat.
    Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory.
  End SmallCat.

  Section CommaCategory.
    Context `(A : @Category objA).
    Context `(B : @Category objB).
    Context `(C : @Category objC).
    Variable S : Functor A C.
    Variable T : Functor B C.

    Record CommaCategory_Object := { CommaCategory_Object_Member :> { ab : objA * objB & C.(Morphism) (S (fst ab)) (T (snd ab)) } }.

    Let SortPolymorphic_Helper (A T : Type) (Build_T : A -> T) := A.

    Definition CommaCategory_ObjectT := Eval hnf in SortPolymorphic_Helper Build_CommaCategory_Object.
    Definition Build_CommaCategory_Object' (mem : CommaCategory_ObjectT) := Build_CommaCategory_Object mem.
    Global Coercion Build_CommaCategory_Object' : CommaCategory_ObjectT >-> CommaCategory_Object.

    Definition CommaCategory : @Category CommaCategory_Object.
    Admitted.
  End CommaCategory.

  Definition SliceCategory_Functor `(C : @Category objC) (a : C) : Functor TerminalCategory C
    := {| ObjectOf := (fun _ => a);
          MorphismOf := (fun _ _ _ => Identity a)
       |}.

  Definition SliceCategoryOver
  : forall (objC : Type) (C : Category objC) (a : C),
      Category
        (CommaCategory_Object (IdentityFunctor C)
                              (SliceCategory_Functor C a)).
    admit.
  Defined.

  Section CommaCategoryProjectionFunctor.
    Context `(A : Category objA).
    Context `(B : Category objB).
    Context `(C : Category objC).

    Variable S : (OppositeCategory (FunctorCategory A C)).
    Variable T : (FunctorCategory B C).

    Definition CommaCategoryProjection : Functor (CommaCategory S T) (ProductCategory A B).
    Admitted.

    Definition CommaCategoryProjectionFunctor_ObjectOf
    : @SliceCategoryOver _ LocallySmallCat (ProductCategory A B)
      :=
        existT _
               ((CommaCategory S T) : Category', tt)
               (CommaCategoryProjection) :
          CommaCategory_ObjectT (IdentityFunctor _)
                                (SliceCategory_Functor LocallySmallCat
                                                       (ProductCategory A B)).
    (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *)
    (* Toplevel input, characters 110-142:
Error:
In environment
objA : Type
A : Category objA
objB : Type
B : Category objB
objC : Type
C : Category objC
S : OppositeCategory (FunctorCategory A C)
T : FunctorCategory B C
The term "ProductCategory A B:Category (objA * objB)" has type
 "Category (objA * objB)" while it is expected to have type
 "Object LocallySmallCat".
 *)
  End CommaCategoryProjectionFunctor.
End SecondComment.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Require Import init.

Require Import set.
Require Import order_minmax.

Require Export analysis_algebraic.
Require Import analysis_func_order.

(* begin hide *)
Section AnalysisDerivative.

Context {U V} `{
    UP : Plus U,
    UZ : Zero U,
    UN : Neg U,
    @PlusComm U UP,
    @PlusAssoc U UP,
    @PlusLid U UP UZ,
    @PlusLinv U UP UZ UN,

    USM : ScalarMult real U,
    @ScalarId real U real_one USM,
    @ScalarLdist real U UP USM,
    @ScalarRdist real U real_plus UP USM,
    @ScalarComp real U real_mult USM,

    UA : AbsoluteValue U,
    @AbsDefinite U UA UZ,
    @AbsNeg U UA UN,
    @AbsTriangle U UA UP,
    @AbsPositive U UA,
    @AbsScalar U UA USM,
    NotTrivial U,

    VP : Plus V,
    VZ : Zero V,
    VN : Neg V,
    @PlusComm V VP,
    @PlusAssoc V VP,
    @PlusLid V VP VZ,
    @PlusLinv V VP VZ VN,

    VSM : ScalarMult real V,
    @ScalarId real V real_one VSM,
    @ScalarLdist real V VP VSM,
    @ScalarRdist real V real_plus VP VSM,

    VA : AbsoluteValue V,
    @AbsDefinite V VA VZ,
    @AbsNeg V VA VN,
    @AbsTriangle V VA VP,
    @AbsPositive V VA,
    @AbsScalar V VA VSM
}.
Existing Instance abs_metric.

(* end hide *)
Definition frechet_derivative_at
    (O : set_type (open (U := U)))
    (f : set_type [O|] → V)
    (a : set_type [O|])
    (A : set_type (bounded_linear_map (U := U) (V := V)))
    := func_lim
        (λ x, |f x - f a - linear_map_f [A|] ([x|] - [a|])| / |[x|] - [a|]|)
        [a|]
        0.

Definition frechet_differentiable_at
    (O : set_type (open (U := U)))
    (f : set_type [O|] → V)
    (a : set_type [O|])
    := ∃ A, frechet_derivative_at O f a A.

Context (O : set_type (open (U := U))).
Context (f g : set_type [O|] → V).

Existing Instance subspace_metric.

Theorem frechet_derivative_unique : ∀ a A B,
    frechet_derivative_at O f a A → frechet_derivative_at O f a B → A = B.
Proof.
    clear g.
    intros a [A A_bound] [B B_bound] [Oa A_dif] [Oa' B_dif]; clear Oa'.
    apply set_type_eq; cbn.
    apply linear_map_eq.
    intros x.
    classic_case (0 = x) as [x_z|x_nz].
    {
        subst x.
        do 2 rewrite linear_map_zero.
        reflexivity.
    }
    assert (0 ≠ |x|) as x_nz'.
    {
        intros contr.
        rewrite abs_def in contr.
        contradiction.
    }
    unfold frechet_derivative_at in *; cbn in *.
    clear A_bound B_bound.
    assert (func_lim_base (λ x, | -f x + f a + linear_map_f B ([x|] - [a|])|
        / |[x|] - [a|]|) [a|] 0) as B_dif'.
    {
        apply (func_lim_eq _ _ _ _ _ B_dif).
        intros y y_neq.
        rewrite <- abs_neg.
        do 2 rewrite neg_plus.
        do 2 rewrite neg_neg.
        reflexivity.
    }
    pose proof (func_lim_plus _ _ _ _ _ _ A_dif B_dif') as lim1.
    clear A_dif B_dif B_dif'.
    cbn in lim1.
    rewrite plus_rid in lim1.
    assert (func_lim_base (λ x : set_type [O|],
        |linear_map_f B ([x|] - [a|]) - linear_map_f A ([x|] - [a|])|
        / |[x|] - [a|]|) [a|] 0) as lim2.
    {
        pose proof (constant_func_lim [O|] [a|] (zero (U := real))) as lim2.
        eapply (func_squeeze _ _ _ _ _ _ _ lim2 lim1).
        Unshelve.
        intros y y_neq; cbn.
        assert (0 < |[y|] - [a|]|) as ya_pos.
        {
            split; [>apply abs_pos|].
            intros contr.
            rewrite abs_def in contr.
            rewrite plus_0_anb_b_a in contr.
            contradiction.
        }
        split.
        -   apply le_mult.
            +   apply abs_pos.
            +   apply div_pos.
                exact ya_pos.
        -   rewrite <- rdist.
            apply le_rmult_pos; [>apply div_pos; exact ya_pos|].
            apply (trans2 (abs_tri _ _)).
            rewrite <- (plus_assoc (f y)).
            rewrite (plus_comm (f y)).
            do 2 rewrite plus_assoc.
            rewrite <- (plus_assoc _ (f y)).
            rewrite plus_rinv, plus_rid.
            rewrite (plus_comm (-f a)).
            rewrite plus_rlinv.
            rewrite plus_comm.
            apply refl.
    }
    clear lim1.
    pose proof [|O] as O_open.
    rewrite open_all_balls in O_open.
    specialize (O_open [a|] [|a]) as [[ε ε_pos] sub].
    pose (εS (t : real) := 0 ≠ t ∧ |t| < ε / |x|).
    pose (g' (t : set_type εS) := [a|] + [t|] · x).
    assert (∀ t, [O|] (g' t)) as g_in.
    {
        intros [t [t_nz t_lt]].
        apply sub.
        unfold open_ball, g'; cbn.
        rewrite neg_plus.
        rewrite plus_lrinv.
        rewrite abs_neg.
        rewrite abs_scalar.
        rewrite lt_mult_lrmove_pos.
        -   exact t_lt.
        -   split; [>apply abs_pos|exact x_nz'].
    }
    pose (g t := [_|g_in t]).
    assert (limit_point εS 0) as εS0.
    {
        assert (0 < ε / |x|) as ε'_pos.
        {
            apply lt_mult.
            -   exact ε_pos.
            -   apply div_pos.
                split; [>apply abs_pos|exact x_nz'].
        }
        assert (limit_point (open_ball (zero (U := real)) [_|ε'_pos]) 0)
            as εS0.
        {
            apply norm_open_limit_point.
            -   apply open_ball_open.
            -   unfold open_ball; cbn.
                rewrite neg_zero, plus_rid, <- abs_zero.
                exact ε'_pos.
        }
        eapply (limit_point_sub _ _ _ _ εS0).
        Unshelve.
        intros y [y_lt y_nz].
        split.
        -   exact y_nz.
        -   unfold open_ball in y_lt; cbn in y_lt.
            rewrite plus_lid, abs_neg in y_lt.
            exact y_lt.
    }
    assert (func_lim_base g 0 a) as g_lim.
    {
        unfold g, g'.
        rewrite <- metric_subspace_topology.
        apply func_lim_set; cbn.
        rewrite <- (plus_rid [a|]) at 1.
        apply func_lim_plus.
        -   apply constant_func_lim.
        -   rewrite <- (scalar_lanni x).
            apply (func_lim_scalar2 εS (λ n, [n|])).
            +   apply func_lim_id.
            +   apply constant_func_lim.
    }
    rewrite <- metric_subspace_topology in g_lim.
    epose proof (func_lim_compose2 _ _ _ _ _ _ _ _ g_lim lim2) as lim3.
    Unshelve.
    2: {
        intros [t [t_nz t_lt]] contr.
        unfold g, g' in contr; cbn in contr.
        apply set_type_eq in contr; cbn in contr.
        rewrite <- plus_0_a_b_ba in contr.
        rewrite <- (scalar_lanni x) in contr.
        apply scalar_rcancel in contr; [>|exact x_nz].
        contradiction.
    }
    clear lim2.
    cbn in lim3.
    unfold g' in lim3.
    pose proof (constant_func_lim εS 0 (|x|)) as lim4.
    pose proof (func_lim_mult _ _ _ _ _ _ lim3 lim4) as lim5.
    cbn in lim5.
    clear lim3 lim4 g_lim.
    rewrite mult_lanni in lim5.
    assert (func_lim_base (λ _ : set_type εS,
        |linear_map_f B x - linear_map_f A x|) 0 0) as lim6.
    {
        apply (func_lim_eq _ _ _ _ _ lim5).
        intros y y_nz.
        rewrite (plus_comm [a|]).
        rewrite plus_rrinv.
        do 2 rewrite linear_map_scalar.
        rewrite <- scalar_rneg.
        rewrite <- scalar_ldist.
        do 2 rewrite abs_scalar.
        assert (0 ≠ |[y|]|) as y_nz'.
        {
            intros contr.
            rewrite abs_def in contr.
            contradiction.
        }
        rewrite div_mult by assumption.
        rewrite mult_assoc.
        rewrite mult_rlinv by exact x_nz'.
        rewrite (mult_comm (|[y|]|)).
        apply mult_rrinv.
        exact y_nz'.
    }
    pose proof (constant_func_lim εS 0 (|linear_map_f B x - linear_map_f A x|))
        as lim7.
    pose proof (func_lim_unique _ _ _ _ εS0 lim6 lim7) as eq.
    rewrite abs_def in eq.
    rewrite plus_0_anb_b_a in eq.
    exact eq.
Qed.

Theorem frechet_differentiable_continuous : ∀ a,
    frechet_differentiable_at O f a → continuous_at f a.
Proof.
    intros a [A [Aa A_lim]].
    rewrite <- metric_subspace_topology.
    rewrite func_lim_continuous by exact Aa.
    pose (bf (x : set_type [O|]) := |[x|] - [a|]|).
    assert (func_lim_base bf [a|] 0) as bf_lim.
    {
        unfold bf.
        rewrite (abs_zero (U := U)).
        apply abs_func_lim.
        rewrite <- (plus_rinv [a|]).
        apply (func_lim_plus [O|] (λ x, [x|])).
        -   apply func_lim_id.
        -   apply constant_func_lim.
    }
    pose proof (func_lim_mult _ _ _ _ _ _ A_lim bf_lim) as lim.
    unfold bf in lim; cbn in lim.
    rewrite mult_lanni in lim.
    destruct A as [A A_bounded]; cbn in *.
    assert (func_lim_base
        (λ x, |f x - f a - linear_map_f A ([x|] - [a|])|) [a|] 0) as lim1.
    {
        apply (func_lim_eq _ _ _ _ _ lim).
        intros x x_neq.
        apply mult_rlinv.
        intros contr.
        rewrite abs_def in contr.
        rewrite plus_0_anb_b_a in contr.
        contradiction.
    }
    clear A_lim lim.
    apply func_lim_zero in lim1.
    assert (func_lim_base (λ x : set_type [O|],
        linear_map_f A [x|] - linear_map_f A [a|]) [a|] 0) as lim2.
    {
        rewrite <- (plus_rinv (linear_map_f A [a|])).
        apply func_lim_plus.
        -   apply bounded_uniformly_continuous in A_bounded.
            apply unformly_implies_continuous in A_bounded.
            specialize (A_bounded [a|]).
            pose (A' (x : set_type [O|]) := linear_map_f A [x|]).
            assert (continuous_at A' a) as A'_cont.
            {
                unfold A'.
                rewrite <- metric_subspace_topology.
                apply continuous_subspace.
                exact A_bounded.
            }
            rewrite <- metric_subspace_topology in A'_cont.
            rewrite func_lim_continuous in A'_cont by exact Aa.
            exact A'_cont.
        -   apply constant_func_lim.
    }
    pose proof (func_lim_plus _ _ _ _ _ _ lim1 lim2) as lim3; clear lim1 lim2.
    cbn in lim3.
    rewrite plus_rid in lim3.
    pose proof (constant_func_lim [O|] [a|] (f a)) as lim4.
    pose proof (func_lim_plus _ _ _ _ _ _ lim3 lim4) as lim5; clear lim3 lim4.
    cbn in lim5.
    rewrite plus_lid in lim5.
    apply (func_lim_eq _ _ _ _ _ lim5).
    intros x x_neq.
    rewrite (plus_comm [x|]).
    rewrite linear_map_plus, linear_map_neg.
    rewrite neg_plus, neg_neg.
    do 2 rewrite plus_assoc.
    rewrite plus_rlinv.
    rewrite plus_rrinv.
    apply plus_rlinv.
Qed.

Theorem frechet_derivative_linear : ∀ (F : set_type bounded_linear_map) a,
    frechet_derivative_at [_|all_open] (λ x, linear_map_f [F|] [x|]) a F.
Proof.
    intros [F F_bound] [a a_in].
    unfold frechet_derivative_at; cbn.
    clear F_bound a_in.
    assert (limit_point all a) as a_lim.
    {
        apply norm_open_limit_point.
        -   apply all_open.
        -   exact true.
    }
    split; [>exact a_lim|].
    pose proof (constant_func_lim all a (zero (U := real))) as lim.
    apply (func_lim_eq _ _ _ _ _ lim).
    intros [x x_in] x_neq; cbn in *.
    clear x_in.
    rewrite linear_map_plus.
    rewrite linear_map_neg.
    rewrite neg_plus, neg_neg.
    rewrite (plus_comm (linear_map_f F x)).
    rewrite plus_assoc.
    rewrite plus_rrinv.
    rewrite plus_linv.
    rewrite <- abs_zero.
    rewrite mult_lanni.
    reflexivity.
Qed.

Theorem frechet_derivative_constant : ∀ x a,
    frechet_derivative_at [_|all_open] (λ _, x) a
        [zero_linear_map|zero_linear_bounded].
Proof.
    intros x [a a_in].
    unfold frechet_derivative_at; cbn.
    clear a_in.
    assert (limit_point all a) as a_lim.
    {
        apply norm_open_limit_point.
        -   apply all_open.
        -   exact true.
    }
    split; [>exact a_lim|].
    pose proof (constant_func_lim all a (zero (U := real))) as lim.
    apply (func_lim_eq _ _ _ _ _ lim).
    intros [y y_in] y_neq; cbn in *.
    clear y_in.
    rewrite neg_zero, plus_rid.
    rewrite plus_rinv.
    rewrite <- abs_zero.
    rewrite mult_lanni.
    reflexivity.
Qed.

Theorem frechet_derivative_plus : ∀ a A B,
    frechet_derivative_at O f a A → frechet_derivative_at O g a B →
    frechet_derivative_at O (λ x, f x + g x) a
        [plus_linear_map [A|] [B|] | plus_linear_bounded A B].
Proof.
    intros a A B [Oa f_lim] [Oa' g_lim]; clear Oa'.
    pose proof (func_lim_plus _ _ _ _ _ _ f_lim g_lim) as lim1.
    clear f_lim g_lim.
    cbn in lim1.
    rewrite plus_rid in lim1.
    pose proof (constant_func_lim [O|] [a|] (zero (U := real))) as lim2.
    split; [>exact Oa|].
    eapply (func_squeeze _ _ _ _ _ _ _ lim2 lim1).
    Unshelve.
    intros x x_neq.
    cbn.
    assert (0 < |[x|] - [a|]|) as xa_pos.
    {
        split; [>apply abs_pos|].
        intros contr.
        rewrite abs_def in contr.
        rewrite plus_0_anb_b_a in contr.
        contradiction.
    }
    split.
    -   apply le_mult.
        +   apply abs_pos.
        +   apply div_pos.
            exact xa_pos.
    -   rewrite <- rdist.
        apply le_rmult_pos; [>apply div_pos; exact xa_pos|].
        apply (trans2 (abs_tri _ _ )).
        do 2 rewrite neg_plus.
        plus_bring_left (g x).
        plus_bring_left (-g a).
        rewrite (plus_comm (-linear_map_f _ _)).
        apply refl.
Qed.

(* begin hide *)
End AnalysisDerivative.

Section ChainRule.

Context {U V W} `{
    UP : Plus U,
    UZ : Zero U,
    UN : Neg U,
    @PlusComm U UP,
    @PlusAssoc U UP,
    @PlusLid U UP UZ,
    @PlusLinv U UP UZ UN,

    USM : ScalarMult real U,
    @ScalarId real U real_one USM,
    @ScalarLdist real U UP USM,
    @ScalarRdist real U real_plus UP USM,
    @ScalarComp real U real_mult USM,

    UA : AbsoluteValue U,
    @AbsDefinite U UA UZ,
    @AbsNeg U UA UN,
    @AbsTriangle U UA UP,
    @AbsPositive U UA,
    @AbsScalar U UA USM,
    NotTrivial U,

    VP : Plus V,
    VZ : Zero V,
    VN : Neg V,
    @PlusComm V VP,
    @PlusAssoc V VP,
    @PlusLid V VP VZ,
    @PlusLinv V VP VZ VN,

    VSM : ScalarMult real V,
    @ScalarId real V real_one VSM,
    @ScalarLdist real V VP VSM,
    @ScalarRdist real V real_plus VP VSM,

    VA : AbsoluteValue V,
    @AbsDefinite V VA VZ,
    @AbsNeg V VA VN,
    @AbsTriangle V VA VP,
    @AbsPositive V VA,
    @AbsScalar V VA VSM,

    WP : Plus W,
    WZ : Zero W,
    WN : Neg W,
    @PlusComm W WP,
    @PlusAssoc W WP,
    @PlusLid W WP WZ,
    @PlusLinv W WP WZ WN,

    WSM : ScalarMult real W,
    @ScalarId real W real_one WSM,
    @ScalarLdist real W WP WSM,
    @ScalarRdist real W real_plus WP WSM,

    WA : AbsoluteValue W,
    @AbsDefinite W WA WZ,
    @AbsNeg W WA WN,
    @AbsTriangle W WA WP,
    @AbsPositive W WA,
    @AbsScalar W WA WSM
}.

Existing Instance abs_metric.
Existing Instance subspace_metric.

(* end hide *)
Theorem frechet_derivative_compose :
    ∀ (O1 : set_type (open (U := U))) (O2 : set_type (open (U := V)))
    (f : set_type [O2|] → W) (g : set_type [O1|] → set_type [O2|]) f' g' a,
    frechet_derivative_at O2 f (g a) f' →
    frechet_derivative_at O1 (λ x, [g x|]) a g' →
    frechet_derivative_at O1 (λ x, f (g x)) a
        [linear_map_compose [f'|] [g'|] |
            linear_map_compose_bounded [f'|] [g'|] [|f'] [|g']].
Proof.
    intros O1 O2 f g [f' f'_bound] [g' g'_bound] a f'_lim g'_lim.
    assert (continuous_at g a) as g_cont.
    {
        rewrite <- (metric_subspace_topology [O2|]).
        apply continuous_subspace2.
        apply frechet_differentiable_continuous.
        exists [g'|g'_bound].
        exact g'_lim.
    }
    destruct g'_lim as [O1a g'_lim].
    destruct f'_lim as [O2ga f'_lim].
    split; [>exact O1a|].
    cbn in *.
    assert (func_lim_base (λ x, |linear_map_f f'
        ([g x|] - [g a|] - linear_map_f g' ([x|] - [a|]))| / |[x|] - [a|]|)
        [a|] 0) as lim1.
    {
        destruct f'_bound as [M M_bound].
        apply (func_lim_constant _ _ M) in g'_lim.
        rewrite mult_ranni in g'_lim.
        pose proof (constant_func_lim [O1|] [a|] (zero (U := real))) as lim1.
        eapply (func_squeeze _ _ _ _ _ _ _ lim1 g'_lim).
        Unshelve.
        intros x x_neq; cbn.
        assert (0 < |[x|] - [a|]|) as xa_pos.
        {
            split; [>apply abs_pos|].
            intros contr.
            rewrite abs_def in contr.
            rewrite plus_0_anb_b_a in contr.
            contradiction.
        }
        split.
        -   apply le_mult.
            +   apply abs_pos.
            +   apply div_pos.
                exact xa_pos.
        -   rewrite mult_assoc.
            apply le_rmult_pos; [>apply div_pos; exact xa_pos|].
            apply M_bound.
    }
    assert (func_bounded_around (λ x, |[g x|] - [g a|]| / |[x|] - [a|]|) [a|])
        as g_bound.
    {
        assert (func_bounded_around (λ x, (/ |[x|] - [a|]|) ·
                ([g x|] - [g a|] - linear_map_f g' ([x|] - [a|]))) [a|])
                as bound1.
        {
            apply (func_lim_bounded_around _ _ _ 0).
            apply func_lim_zero.
            apply (func_lim_eq _ _ _ _ _ g'_lim).
            intros x x_neq.
            assert (0 < |[x|] - [a|]|) as xa_pos.
            {
                split; [>apply abs_pos|].
                intros contr.
                rewrite abs_def in contr.
                rewrite plus_0_anb_b_a in contr.
                contradiction.
            }
            rewrite abs_scalar.
            rewrite mult_comm.
            apply rmult.
            rewrite <- abs_div by apply xa_pos.
            rewrite abs_abs.
            reflexivity.
        }
        assert (func_bounded_around (λ x : set_type [O1|],
            (/ |[x|] - [a|]|) · linear_map_f g' ([x|] - [a|])) [a|]) as bound2.
        {
            destruct g'_bound as [M M_bound].
            exists [1|one_pos], M.
            intros x x_neq x_lt.
            assert (0 < |[x|] - [a|]|) as xa_pos.
            {
                split; [>apply abs_pos|].
                intros contr.
                rewrite abs_def in contr.
                rewrite plus_0_anb_b_a in contr.
                contradiction.
            }
            rewrite abs_scalar.
            rewrite <- abs_div by apply xa_pos.
            rewrite abs_abs.
            rewrite <- le_mult_rlmove_pos by apply xa_pos.
            rewrite mult_comm.
            apply M_bound.
        }
        pose proof (func_bounded_around_plus _ _ _ _ bound1 bound2)
            as [[ε ε_pos] [M M_bound]].
        exists [ε|ε_pos], M.
        intros x x_neq x_lt.
        assert (0 < |[x|] - [a|]|) as xa_pos.
        {
            split; [>apply abs_pos|].
            intros contr.
            rewrite abs_def in contr.
            rewrite plus_0_anb_b_a in contr.
            contradiction.
        }
        specialize (M_bound x x_neq x_lt).
        apply (trans2 M_bound).
        rewrite <- scalar_ldist.
        rewrite abs_mult.
        rewrite abs_scalar.
        rewrite mult_comm.
        rewrite <- abs_div by apply xa_pos.
        do 2 rewrite abs_abs.
        apply le_lmult_pos; [>apply div_pos; exact xa_pos|].
        rewrite plus_rlinv.
        apply refl.
    }
    assert (func_lim_base (λ x,
        |f (g x) - f (g a) - linear_map_f f' ([g x|] - [g a|])|
        / |[x|] - [a|]|) [a|] 0) as lim2.
    {
        apply func_lim_forget.
        cbn.
        apply (func_lim_eq _ (λ x, let x' := [[x|] | land [|x]] in
            (|[g x'|] - [g a|]| / |[x|] - [a|]|) *
            (|f (g x') - f (g a) - linear_map_f f' ([g x'|] - [g a|])|
                / |[g x'|] - [g a|]|))).
        -   apply func_lim_zero_mult.
            +   eapply (func_bounded_around_subset _ _ _ _ _ _ _ g_bound).
                Unshelve.
                Unshelve.
                *   intros x [O1x x_nz].
                    exact O1x.
                *   cbn.
                    intros [x [O1x x_nz]]; cbn.
                    rewrite (proof_irrelevance _ O1x).
                    reflexivity.
            +   rewrite <- metric_subspace_topology in g_cont.
                rewrite func_lim_continuous in g_cont.
                rewrite <- metric_subspace_topology in g_cont.
                assert (func_lim_base (λ x : set_type
                    (λ x, [O1|] x ∧ (∀ H, |f (g [x|H]) - f (g a) -
                        linear_map_f f' ([g [x|H]|] - [g a|])| /
                        |x - [a|]| ≠ 0)),
                    g [[x|] | land [|x]]) [a|] (g a)) as lim2.
                {
                    rewrite <- metric_subspace_topology.
                    eapply (func_lim_subset _ _ _ _ _ _ _ _ g_cont).
                    Unshelve.
                    Unshelve.
                    -   intros x [O1x C0].
                        exact O1x.
                    -   cbn.
                        intros [x [O1x x_neq]]; cbn.
                        apply f_equal.
                        apply f_equal.
                        apply proof_irrelevance.
                }
                rewrite <- metric_subspace_topology in lim2.
                eapply (func_lim_compose2 _ _
                    (λ x, |f x - f (g a) - linear_map_f f' ([x|] - [g a|])| /
                        |[x|] - [g a|]|)_ _ _ _ _ lim2).
                Unshelve.
                *   exact f'_lim.
                *   cbn.
                    intros [x [O1x x_neq]]; cbn.
                    rewrite (proof_irrelevance _ O1x).
                    specialize (x_neq O1x).
                    intros contr.
                    rewrite <- contr in x_neq.
                    do 2 rewrite plus_rinv in x_neq.
                    rewrite linear_map_zero in x_neq.
                    rewrite neg_zero, plus_rid in x_neq.
                    rewrite <- abs_zero in x_neq.
                    rewrite mult_lanni in x_neq.
                    contradiction.
        -   intros [x [O1x x_nz]] x_neq; cbn.
            rewrite (proof_irrelevance _ O1x).
            rewrite mult_comm.
            rewrite <- mult_assoc.
            apply lmult.
            apply mult_llinv.
            intros contr.
            rewrite abs_def in contr.
            cbn in x_neq.
            specialize (x_nz O1x).
            apply x_nz.
            rewrite plus_0_anb_a_b in contr.
            apply set_type_eq in contr.
            rewrite contr.
            do 2 rewrite plus_rinv.
            rewrite linear_map_zero.
            rewrite neg_zero, plus_rid.
            rewrite <- abs_zero.
            apply mult_lanni.
    }
    pose proof (func_lim_plus _ _ _ _ _ _ lim1 lim2) as lim3.
    cbn in lim3.
    rewrite plus_rid in lim3.
    pose proof (constant_func_lim [O1|] [a|] (zero (U := real))) as lim4.
    eapply (func_squeeze _ _ _ _ _ _ _ lim4 lim3).
    Unshelve.
    intros [x O1x] x_neq; cbn in *.
    assert (0 < |x - [a|]|) as xa_pos.
    {
        split; [>apply abs_pos|].
        intros contr.
        rewrite abs_def in contr.
        rewrite plus_0_anb_b_a in contr.
        contradiction.
    }
    split.
    -   apply le_mult.
        +   apply abs_pos.
        +   apply div_pos.
            exact xa_pos.
    -   rewrite <- rdist.
        apply le_rmult_pos; [>apply div_pos; exact xa_pos|].
        apply (trans2 (abs_tri _ _ )).
        rewrite (linear_map_plus f').
        rewrite (plus_comm (linear_map_f f' _ + _)).
        rewrite plus_assoc.
        rewrite plus_rlinv.
        rewrite linear_map_neg.
        apply refl.
Qed.
(* begin hide *)

End ChainRule.
(* end hide *)

author: sudgy

repo: math-from-nothing


text:
Require Export cpt2induction.

Module NatList.

  (* Working with Structured Data - Lists *)

  (* Pairs of numbers *)

  (* Inductive type definition
   * each constructor can take any number of arguments
   * none, one, more than one, etc. *)

Inductive natprod : Type :=
  pair : nat -> nat -> natprod.
(* "There is just one way to construct a pair of numbers:
    by applying the constructor pair to two arguments of type nat" *)

(* element of natprod *)
Check (pair 3 5).

(* function definition for extracting the first and second componenets
   of a pair *)

Definition fst (p : natprod) : nat :=
  match p with
    | pair x y => x
  end.
Definition snd (p : natprod) : nat :=
  match p with
    | pair x y => y
  end.

Eval compute in (fst (pair 3 5)).

(* tell Coq to allow mathematical notation *)
Notation "( x , y )" := (pair x y).

Eval compute in (fst (3,5)).

(* Notation can be used in expressions and pattern matches! *)
Definition fst' (p : natprod) : nat :=
  match p with
    | (x,y) => x
  end.
Definition and' (p : natprod) : nat :=
  match p with
    | (x,y) => y
  end.
Definition swap_pair (p : natprod) : natprod :=
  match p with
    | (x,y) => (y,x)
  end.

(* Proving simple facts about pairs *)
Theorem surjective_pairing' : forall(n m : nat),
                                (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity.
Qed.

(* reflexivity is not enough if we state the lemma in a natural way *)
Theorem surjective_pairing_stuck: forall (p:natprod),
                                    p = (fst p, snd p).
Proof.
  simpl. (* Doesn't reduce anything *)
Abort.

(* have to expose the structure of p so that simpl can perform the
   pattern match in fst and snd! Use destruct *)
Theorem surjective_pairing : forall (p : natprod),
                               p = (fst p, snd p).
Proof.
  intros p.
  destruct p as [n m].
  simpl.
  reflexivity.
Qed.

(* Exercise snd_fst_is_swap *)
Theorem snd_fst_is_swap : forall (p : natprod),
                            (snd p, fst p) = swap_pair p.
Proof.
  intros p.
  destruct p as [n m].
  simpl.
  reflexivity.
Qed.

(* Exercise fst_swap_is_snd *)
Theorem fst_swap_is_snd : forall (p : natprod),
                            fst(swap_pair p) = snd p.
Proof.
  intros p.
  destruct p as [n m].
  simpl.
  reflexivity.
Qed.

(* List of Numbers *)

(* We can describe the type of lists of numbers *)
(* A List is either the empty list or else a pair of number and another list *)

Inductive natlist : Type :=
    | nil : natlist
    | cons : nat -> natlist -> natlist.

(* Example: 3 element list *)
Definition mylist := cons 1 (cons 2 (cons 3 nil)).

(* more convenient to write lists in familiar programming notation  *)
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Check [1,2,3].
Check 1::2::3::nil.
Check (cons 1 (cons 2 (cons 3 nil))).
(* These three mean the same thing *)

Fixpoint repeat (n count : nat) : natlist  :=
  match count with
    | O => []
    | S count' => n::(repeat n count')
  end.

(* Length *)
Fixpoint length (l : natlist) : nat :=
  match l with
    | nil => O
    | h :: t => S (length t)
  end.

(* append *)
Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | h :: t => h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4,5] = [4,5].
Proof. reflexivity. Qed.
Example test_app3: [1,2,3] ++ nil = [1,2,3].
Proof. reflexivity. Qed.

(* Head with default and Tail *)

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil => default
  | h :: t => h
  end.

Definition tl (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => t
  end.

Example test_hd1: hd 0 [1,2,3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1,2,3] = [2,3].
Proof. reflexivity. Qed.

(* Exercise list_funs *)
Fixpoint nonzeros (l:natlist) : natlist :=
  match l with
    | [] => []
    | 0 :: t => nonzeros t
    | h :: t => h :: (nonzeros t)
  end.

Example test_nonzeros: nonzeros [0,1,0,2,3,0,0] = [1,2,3].
Proof.
  reflexivity.
Qed.

Fixpoint oddnumbers (l:natlist) : natlist :=
  match l with
    | [] => []
    | h :: t => match (oddb h) with
                    | true => h::(oddnumbers t)
                    |false => oddnumbers t
  end
end.

Example test_oddnumbers: oddnumbers [0,1,0,2,3,0,0] = [1,3].
Proof.
  reflexivity.
Qed.

Fixpoint countoddnumbers (l:natlist) : nat :=
  match l with
    | [] => 0
    | h :: t => match (oddb h) with
                  | true => S (countoddnumbers t)
                  | false => countoddnumbers t
                end
  end.

Example test_countoddmembers1: countoddnumbers [1,0,3,1,4,5] = 4.
Proof.
  reflexivity.
Qed.

Example test_countoddmembers2: countoddnumbers [0,2,4] = 0.
Proof.
  reflexivity.
Qed.
Example test_countoddnumbers3: countoddnumbers nil = 0.
Proof.
  reflexivity.
Qed.

(* Exercise alternate *)
Fixpoint alternate (l1 l2 : natlist) : natlist :=
  match l2 with
    | [] => l1
    | h2::t2 => match l1 with
                  | [] => l2
                  | h1::t1 => h1::h2 :: (alternate t1 t2)
                end
  end.
Example test_alternate1: alternate [1,2,3] [4,5,6] = [1,4,2,5,3,6].
Proof.
  reflexivity.
Qed.
Example test_alternate2: alternate [1] [4,5,6] = [1,4,5,6].
Proof.
  reflexivity.
Qed.
Example test_alternate3: alternate [1,2,3] [4] = [1,4,2,3].
Proof.
  reflexivity.
Qed.
Example test_alternate4: alternate [] [20,30] = [20,30].
Proof.
  reflexivity.
Qed.

(* Bags via Lists *)
(* Bag or a multiset is like a set, but each element can appear multiple times
 instead of just once *)
Definition bag := natlist.

(* Ex. bag_functions *)
Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
    | [] => 0
    | h::t => if beq_nat v h then S (count v t) else count v t
  end.

Example test_count1: count 1 [1,2,3,1,4,1] = 3.
Proof.
  reflexivity.
Qed.

Example test_count2: count 6 [1,2,3,1,4,1] = 0.
Proof.
  reflexivity.
Qed.

(* su is similar to union *)

Definition sum : bag -> bag -> bag := app.
Example test_sum1: count 1 (sum [1,2,3] [1,4,1]) = 3.
Proof.
  reflexivity.
Qed.

Definition add (v:nat) (b:bag) := cons v b.

Example test_add1: count 1 (add 1 [1,4,1]) = 3.
reflexivity.
Qed.

Example test_add2: count 5 (add 1 [1,4,1]) = 0.
reflexivity.
Qed.

Definition member (v:nat) (s:bag) : bool :=
  negb (beq_nat (count v s) O).

Example test_member1: member 1 [1,4,1] = true.
reflexivity.
Qed.

Example test_member2: member 2 [1,4,1] = false.
  reflexivity.
Qed.
Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
    | [] => []
    | h::t => if (beq_nat h v) then t else h::(remove_one v t)
  end.

Example test_remove_one1: count 5 (remove_one 5 [2,1,5,4,1]) = 0.
reflexivity.
Qed.
Example test_remove_one2: count 5 (remove_one 5 [2,1,4,1]) = 0.
reflexivity.
Qed.
Example test_remove_one3: count 4 (remove_one 5 [2,1,4,5,1,4]) = 2.
reflexivity.
Qed.
Example test_remove_one4:
  count 5 (remove_one 5 [2,1,5,4,5,1,4]) = 1.
reflexivity.
Qed.

Fixpoint remove_all (v:nat) (s:bag) : bag :=
  match s with
    | [] => []
    | h::t => if (beq_nat h v) then (remove_all v t) else h::(remove_all v t)
  end.

Example test_remove_all1: count 5 (remove_all 5 [2,1,5,4,1]) = 0.
reflexivity.
Qed.

Example test_remove_all2: count 5 (remove_all 5 [2,1,4,1]) = 0.
reflexivity.
Qed.

Example test_remove_all3: count 4 (remove_all 5 [2,1,4,5,1,4]) = 2.
reflexivity.
Qed.

Example test_remove_all4: count 5 (remove_all 5 [2,1,5,4,5,1,4,5,1,4]) = 0.
reflexivity.
Qed.

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
    | [] => true
    | h::t => if (member h s2) then (subset t (remove_one h s2)) else false
  end.

Example test_subset1: subset [1,2] [2,1,4,1] = true.
Proof.
reflexivity.
Qed.

Example test_subset2: subset [1,2,2] [4,1] = false.
reflexivity.
Qed.

Example test_subset3: subset [1,2,2] [2,1,2] = true.
reflexivity.
Qed.

(* Reasoning about Lists *)

Theorem nil_app : forall l:natlist,
  [] ++ l = l.
Proof.
  reflexivity.
Qed.

Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
  Proof.
    destruct l as [| n l'].
    reflexivity.
    reflexivity.
  Qed.

Theorem app_assoc : forall l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3.
  induction l1 as [| n l1'].
  Case "l1 = nil".
  reflexivity.
  Case "l1 = cons n l1'".
  simpl.
  rewrite -> IHl1'.
  reflexivity.
Qed.

Theorem app_length : forall l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  intros l1 l2.
  induction l1 as [|n l'].
  reflexivity.
  simpl.
  rewrite -> IHl'.
  reflexivity.
Qed.

Fixpoint snoc (l:natlist) (v:nat) : natlist :=
  match l with
    | nil => [v]
    | h :: t => h :: (snoc t v)
  end.
Fixpoint rev (l:natlist) : natlist :=
  match l with
    | [] => []
    | h :: t => (snoc (rev t) h)
  end.

Lemma length_snoc: forall (l:natlist) (n:nat),
  length (snoc l n) = S (length l).
Proof.
  intros l n.
  induction l as [| n' l' ].
  reflexivity.
  simpl.
  rewrite -> IHl'.
  reflexivity.
Qed.

Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intro l.
  induction l as [| n l'].
  reflexivity.
  simpl.
  rewrite -> length_snoc.
  rewrite -> IHl'.
  reflexivity.
Qed.

Theorem app_nil_end : forall l : natlist,
  l ++ [] = l.
Proof.
  intro l.
  induction l as [|n l'].
  reflexivity.
  simpl.
  rewrite -> IHl'.
  reflexivity.
Qed.

Theorem rev_snoc : forall (n:nat) (l:natlist),
  rev (snoc l n)   = n :: (rev l).
Proof.
  intros n l.
  induction l as [| n' l'].
  reflexivity.
  simpl.
  rewrite -> IHl'.
  reflexivity.
Qed.
Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
  Proof.
    intro l.
    induction l as [| n l'].
    reflexivity.
    simpl.
    rewrite -> rev_snoc.
    rewrite IHl'.
    reflexivity.
  Qed.

(* Homework *)
Lemma snoc_app: forall (l1 l2:natlist) (n:nat),
 snoc (l1 ++ l2) n = l1 ++ snoc l2 n.
Proof.
  intros l1 l2 n.
  induction l1.
  reflexivity.
  simpl.
  rewrite IHl1.
  reflexivity.
Qed.

Theorem distr_rev : forall l1 l2 : natlist,
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
  intros l1 l2.
  induction l1 as [| n l1'].
  simpl.
  rewrite -> app_nil_end.
  reflexivity.
  simpl.
  rewrite -> IHl1'.
  rewrite -> snoc_app.
  reflexivity.
Qed.

Theorem snoc_append : forall (l:natlist) (n:nat),
  snoc l n = l ++ [n].
Proof.
  intros l n.
  induction l.
  reflexivity.
  simpl.
  rewrite IHl.
  reflexivity.
Qed.

Theorem app_ass4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
  Proof.
    intros l1 l2 l3 l4.
    rewrite <- app_assoc.
    rewrite <- app_assoc.
    reflexivity.
  Qed.

Lemma nonzeros_length : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  intros l1 l2.
  induction l1 as [| n l1'].
  reflexivity.
  destruct n as [| n'].
  simpl.
  rewrite -> IHl1'.
  reflexivity.
  simpl.
  rewrite -> IHl1'.
  reflexivity.
Qed.

Theorem count_member_nonzero : forall (s : bag),
  ble_nat 1 (count 1 (1 :: s)) = true.
Proof.
  intro s.
  reflexivity.
Qed.

Theorem ble_n_Sn : forall n,
  ble_nat n (S n) = true.
Proof.
  intro n.
  induction n as [| n'].
  reflexivity.
  simpl.
  rewrite IHn'.
  reflexivity.
Qed.

Theorem remove_decreases_count: forall (s : bag),
  ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
  intros s.
  induction s as [| n s' ].
  reflexivity.
  destruct n.
  simpl.
  rewrite ble_n_Sn.
  reflexivity.
  simpl.
  rewrite IHs'.
  reflexivity.
Qed.

(* natoption is a way of returning "error codes" from functions *)
Fixpoint index_bad (n:nat) (l:natlist) : nat :=
  match l with
    | nil => 42 (* arbitrary *)
    | a :: l' => match beq_nat n O with
                   | true => a
                   | false => index_bad (pred n) l'
                 end
  end.

Inductive natoption : Type :=
| None : natoption
| Some : nat -> natoption.

Fixpoint index (n:nat) (l:natlist) : natoption :=
  match l with
  | nil => None
  | a :: l' => match beq_nat n O with
               | true => Some a
               | false => index (pred n) l'
               end
  end.

Definition foo (l:natlist) : bool :=
  match index 5 l with
    | Some 3 => true
    | _ => false
  end.

Fixpoint index' (n:nat) (l:natlist) : natoption :=
  match l with
  | nil => None
  | a :: l' => if beq_nat n O then Some a else index (pred n) l'
  end.

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.

Definition hd_opt (l : natlist) : natoption :=
  match l with
    | [] => None
    | h :: t => Some h
  end.

Theorem option_elim_hd : forall (l:natlist) (default:nat),
  hd default l = option_elim default (hd_opt l).
Proof.
  intros l default.
  destruct l.
  reflexivity.
  reflexivity.
Qed.

Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
  match l1, l2 with
    | [], [] => true
    | h1 :: t1, h2 :: t2 => if beq_nat h1 h2 then beq_natlist t1 t2 else false
    | _, _ => false
  end.

End NatList.

author: soojison

repo: Software-Foundations


text:
(*
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *)

(* Unary operators *)

Require Import Bool.
Require Import EquivDec.
Require Import String.
Require Import List.
Require Import ZArith.
Require Import Utils.
Require Import FloatAdd.
Require Import ListAdd.
Require Import Lift.
Require Import Assoc.
Require Import Bindings.
Require Import ForeignEJson.
Require Import EJson.

Section EJsonOperators.

  Import ListNotations.

  Inductive ejson_op :=
  | EJsonOpNot : ejson_op                          (* unary_op_not *)              (* !v *)
  | EJsonOpNeg : ejson_op                          (* unary_op_neg *)              (* -v *)
  | EJsonOpAnd : ejson_op                          (* binary_op_and *)             (* v1 && v2 *)
  | EJsonOpOr : ejson_op                           (* binary_op_or *)              (* v1 || v2 *)
  | EJsonOpLt : ejson_op                           (* binary_op_lt *)              (* v1 < v2 *)
  | EJsonOpLe : ejson_op                           (* binary_op_le *)              (* v1 <= v2 *)
  | EJsonOpGt : ejson_op                           (* binary_op_gt *)              (* v1 > v2 *)
  | EJsonOpGe : ejson_op                           (* binary_op_ge *)              (* v1 >= v2 *)
  | EJsonOpAddString : ejson_op                    (* binary_op_add *)             (* v1 + v2 *)
  | EJsonOpAddNumber : ejson_op                    (* binary_op_add *)             (* v1 + v2 *)
  | EJsonOpSub : ejson_op                          (* binary_op_sub *)             (* v1 - v2 *)
  | EJsonOpMult : ejson_op                         (* binary_op_mult *)            (* v1 * v2 *)
  | EJsonOpDiv : ejson_op                          (* binary_op_div *)             (* v1 / v2 *)
  | EJsonOpStrictEqual : ejson_op                  (* binary_op_strict_equal *)    (* v1 === v2 *)
  | EJsonOpStrictDisequal : ejson_op               (* binary_op_strict_disequal *) (* v1 !== v2 *)
  (* Array Stuff *)
  | EJsonOpArray : ejson_op                        (* expr_array *)                (* [ v1, ...vn ] *)
  | EJsonOpArrayLength : ejson_op                  (* expr_member *)               (* v.length *)
  | EJsonOpArrayPush : ejson_op                    (* array_push *)                (* var v' = v.slice(); v'.push(v2) XXX Does not actually claim to be mutable from a semantic stand-point *)
  | EJsonOpArrayAccess : ejson_op                  (* array_get *)                 (* v[i] *)
  (* Object Stuff *)
  | EJsonOpObject : list string -> ejson_op        (* expr_object *)               (* { a1:v1, ...an:vn } *)
  | EJsonOpAccess : string -> ejson_op             (* expr_member *)               (* v['a'] *)
  | EJsonOpHasOwnProperty : string -> ejson_op     (* object_hasOwnProperty *)     (* v.hasOwnProperty('a') *)
  (* Math stuff *)
  | EJsonOpMathMin : ejson_op                      (* expr_call *)                 (* Math.min(e1, e2) *)
  | EJsonOpMathMax : ejson_op                      (* expr_call *)                 (* Math.max(e1, e2) *)
  | EJsonOpMathPow : ejson_op                      (* expr_call *)                 (* Math.pow(e1, e2) *)
  | EJsonOpMathExp : ejson_op                      (* expr_call *)                 (* Math.exp(e) *)
  | EJsonOpMathAbs : ejson_op                      (* expr_call *)                 (* Math.abs(e) *)
  | EJsonOpMathLog : ejson_op                      (* expr_call *)                 (* Math.log2(e) *)
  | EJsonOpMathLog10 : ejson_op                    (* expr_call *)                 (* Math.log10(e) *)
  | EJsonOpMathSqrt : ejson_op                     (* expr_call *)                 (* Math.sqrt(e) *)
  | EJsonOpMathCeil : ejson_op                     (* expr_call *)                 (* Math.ceil(e) *)
  | EJsonOpMathFloor : ejson_op                    (* expr_call *)                 (* Math.floor(e) *)
  | EJsonOpMathTrunc : ejson_op                    (* expr_call *)                 (* Math.trunc(e) *)
  .

  Section Evaluation.
    Context {foreign_ejson_model:Set}.
    Context {fejson:foreign_ejson foreign_ejson_model}.

    Definition ejson_op_eval (op:ejson_op) (j:list (@ejson foreign_ejson_model)) : option ejson :=
      match op with
      | EJsonOpNot =>
        match j with
        | [ejbool b] => Some (ejbool (negb b))
        | _ => None
        end
      | EJsonOpNeg =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_neg n))
        | _ => None
        end
      | EJsonOpAnd =>
        match j with
        | [ejbool b1; ejbool b2] => Some (ejbool (andb b1 b2))
        | _ => None
        end
      | EJsonOpOr =>
        match j with
        | [ejbool b1; ejbool b2] => Some (ejbool (orb b1 b2))
        | _ => None
        end
      | EJsonOpLt =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_lt n1 n2))
        | _ => None
        end
      | EJsonOpLe =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_le n1 n2))
        | _ => None
        end
      | EJsonOpGt =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_gt n1 n2))
        | _ => None
        end
      | EJsonOpGe =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejbool (float_ge n1 n2))
        | _ => None
        end
      | EJsonOpAddString =>
        match j with
        | [ejstring s1; ejstring s2] => Some (ejstring (s1 ++ s2))
        | _ => None
        end
      | EJsonOpAddNumber =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_add n1 n2))
        | _ => None
        end
      | EJsonOpSub =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_sub n1 n2))
        | _ => None
        end
      | EJsonOpMult =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_mult n1 n2))
        | _ => None
        end
      | EJsonOpDiv =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_div n1 n2))
        | _ => None
        end
      | EJsonOpStrictEqual =>
        (* XXX Only defined on atomic values, is this right? *)
        match j with
        | [ejnull; ejnull] => Some (ejbool true)
        | [ejbool b1; ejbool b2] => Some (ejbool (if bool_dec b1 b2 then true else false))
        | [ejnumber n1; ejnumber n2] => Some (ejbool (if float_eq_dec n1 n2 then true else false))
        | [ejbigint n1; ejbigint n2] => Some (ejbool (if Z.eq_dec n1 n2 then true else false))
        | [ejstring s1; ejstring s2] => Some (ejbool (if string_dec s1 s2 then true else false))
        | _ => Some (ejbool false)
        end
      | EJsonOpStrictDisequal =>
        (* XXX Only defined on atomic values, is this right? *)
        match j with
        | [ejnull; ejnull] => Some (ejbool false)
        | [ejbool b1; ejbool b2] => Some (ejbool (if bool_dec b1 b2 then false else true))
        | [ejnumber n1; ejnumber n2] => Some (ejbool (if float_eq_dec n1 n2 then false else true))
        | [ejbigint n1; ejbigint n2] => Some (ejbool (if Z.eq_dec n1 n2 then false else true))
        | [ejstring s1; ejstring s2] => Some (ejbool (if string_dec s1 s2 then false else true))
        | _ => Some (ejbool false)
        end
      | EJsonOpArray => Some (ejarray j)
      | EJsonOpArrayLength =>
        match j with
        | [ejarray ja] => Some (ejbigint (Z_of_nat (List.length ja)))
        | _ => None
        end
      | EJsonOpArrayPush =>
        match j with
        | [ejarray ja; je] => Some (ejarray (ja ++ [je]))
        | _ => None
        end
      | EJsonOpArrayAccess =>
        match j with
        | [ejarray ja; ejbigint n] =>
          let natish := ZToSignedNat n in
          if (fst natish) then
            match List.nth_error ja (snd natish) with
            | None => None
            | Some d => Some d
            end
          else None
        | _ => None
        end
      | EJsonOpObject atts =>
        lift ejobject (zip atts j)
      | EJsonOpAccess att =>
        match j with
        | [ejobject jl] =>
          edot jl att
        | _ => None
        end
      | EJsonOpHasOwnProperty a =>
        match j with
        | [ejobject jl] =>
          if in_dec string_dec a (domain jl)
          then Some (ejbool true)
          else Some (ejbool false)
        | _ => None
        end
      | EJsonOpMathMin =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_min n1 n2))
        | _ => None
        end
      | EJsonOpMathMax =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_max n1 n2))
        | _ => None
        end
      | EJsonOpMathExp =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_exp n))
        | _ => None
        end
      | EJsonOpMathPow =>
        match j with
        | [ejnumber n1; ejnumber n2] => Some (ejnumber (float_pow n1 n2))
        | _ => None
        end
      | EJsonOpMathAbs =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_absolute n))
        | _ => None
        end
      | EJsonOpMathLog =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_log n))
        | _ => None
        end
      | EJsonOpMathLog10 =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_log10 n))
        | _ => None
        end
      | EJsonOpMathSqrt =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_sqrt n))
        | _ => None
        end
      | EJsonOpMathCeil =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_ceil n))
        | _ => None
        end
      | EJsonOpMathFloor =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_floor n))
        | _ => None
        end
      | EJsonOpMathTrunc =>
        match j with
        | [ejnumber n] => Some (ejnumber (float_of_int (float_truncate n))) (* XXX yields a number to be consistent with JS semantics *)
        | _ => None
        end
      end.
  End Evaluation.

End EJsonOperators.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert


text:
From QuickChick Require Import QuickChick.

Require Import TestingCommon.
Require Import Reachability.
Require Import SSNI.
Require Import SanityChecks.
Require Import ZArith.
(* Require Import Generation. *)
From mathcomp Require Import ssreflect eqtype seq.
Import LabelEqType.

#[local] Instance FuzzyZ : Fuzzy Z :=
  {| fuzz n := choose (n - 5, n + 5)%Z |}.

Derive (Arbitrary, Fuzzy) for BinOpT.
Derive (Arbitrary, Fuzzy) for Instr.
Derive (Arbitrary, Fuzzy) for Pointer.
Derive (Arbitrary, Fuzzy) for Value.
Derive (Arbitrary, Fuzzy) for Atom.
Derive (Arbitrary, Fuzzy) for Ptr_atom.
Derive (Arbitrary, Fuzzy) for StackFrame.
Derive (Arbitrary, Fuzzy) for Stack.
Derive (Arbitrary, Fuzzy) for SState.
Derive (Arbitrary, Fuzzy) for Variation.

(*
ManualExtract BinOpT.
ManualExtract Instr.
ManualExtract Pointer.
ManualExtract Value.
ManualExtract Atom.
ManualExtract Ptr_atom.
ManualExtract StackFrame.
ManualExtract Stack.
ManualExtract SState.
ManualExtract Variation. *)

Definition test_propSSNI_smart (v: @Variation SState) :=
    propSSNI_smart default_table v.

Axiom num_tests : nat. Extract Constant num_tests => "max_int".

Definition test_propSSNI_smart_fuzzer :=
  fun (u : unit) => fuzzLoopWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) arbitrary fuzz show test_propSSNI_smart.

(*! FuzzChick test_propSSNI_smart (test_propSSNI_smart_fuzzer tt). *)

  (* gen_variation_SState
  gen_variation_copy: fuzzy
  gen_variation_naive == arbitrary/random
  gen_variation_naive: fuzzy *)

repo: etna

sha: master


text:
From Tweetnacl Require Import Libs.Export.
From Tweetnacl Require Import ListsOp.Export.
From stdpp Require Import list.
Require Import Recdef.

(*
sv pack25519(u8 *o,const gf n)
{
  int i,j,b;
  gf m,t;
  FOR(i,16) t[i]=n[i];
  car25519(t);
  car25519(t);
  car25519(t);
  FOR(j,2) {
    m[0]=t[0]-0xffed;

    for(i=1;i<15;i++) {
      m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
      m[i-1]&=0xffff;
    }

    for(i=1;i<15;i++) {
      m[i]=t[i]-0xffff;
    }
    for(i=1;i<15;i++) {
      m[i]=m[i]-((m[i-1]>>16)&1);
      m[i-1]&=0xffff;
    }

    m[15]=t[15]-0x7fff-((m[14]>>16)&1);
    b=(m[15]>>16)&1;
    m[14]&=0xffff;
    sel25519(t,m,1-b);
  }
  FOR(i,16) {
    o[2*i]=t[i]&0xff;
    o[2*i+1]=t[i]>>8;
  }
}
*)

Open Scope Z.
(*
0xffff = 65535
0xffed = 65517
0x7fff = 32767
*)

Definition subst_0xffed t := t - 65517.
Definition subst_0x7fffc t m := t - 32767 - (Z.land (Z.shiftr m 16) 1).
Definition subst_0x7fff t := t - 32767.

Definition subst_0xffffc t m := t - 65535 - (Z.land (Z.shiftr m 16) 1).
Definition mod0xffff m := Z.land m 65535.

Definition sub_step (a:Z) (m t:list Z) : list Z :=
    let m' := nth (Z.to_nat (a - 1)) m 0 in
    let t' := nth (Z.to_nat a) t 0 in
      upd_nth (Z.to_nat (a-1)) (upd_nth (Z.to_nat a) m (subst_0xffffc t' m')) (mod0xffff m').

Lemma nth_i_1_substep: forall i m t,
  Zlength m = Zlength t ->
  0 < i < Zlength m ->
  nth (Z.to_nat (i - 1)) (sub_step i m t) 0 = mod0xffff (nth (Z.to_nat (i - 1)) m 0).
Proof.
  intros i m t Hmt Him.
  unfold sub_step, mod0xffff.
  rewrite upd_nth_same_Zlength ; try reflexivity.
  split ; try omega ; rewrite upd_nth_Zlength ; rewrite Z2Nat.id ; try omega.
Qed.

Lemma nth_i_substep: forall i m t,
  Zlength m = Zlength t ->
  0 < i < Zlength m ->
  nth (Z.to_nat (i)) (sub_step i m t) 0 = subst_0xffffc (nth (Z.to_nat i) t 0) (nth (Z.to_nat (i - 1)) m 0).
Proof.
  intros i m t Hmt Him.
  unfold sub_step.
  rewrite upd_nth_diff_Zlength.
  2: split ; try omega ; rewrite upd_nth_Zlength ; rewrite Z2Nat.id ; try omega.
  2: split ; try omega ; rewrite upd_nth_Zlength ; rewrite Z2Nat.id ; try omega.
  2: intros H ; apply (f_equal Z.of_nat) in H ; rewrite ?Z2Nat.id in H ; omega.
  rewrite upd_nth_same_Zlength ; try reflexivity.
  rewrite Z2Nat.id ; try omega.
Qed.

Lemma nth_i_1_substep_bounds: forall i m t,
  Zlength m = Zlength t ->
  0 < i < Zlength m ->
  0 <= nth (Z.to_nat (i - 1)) (sub_step i m t) 0 < 2^16.
Proof.
  intros.
  rewrite nth_i_1_substep ; auto.
  unfold mod0xffff.
  change 65535 with (Z.ones 16).
  rewrite Z.land_ones ; try omega.
  apply Z_mod_lt.
  apply pown0 ; omega.
Qed.

Lemma nth_i_substep_bounds: forall i m t,
  Zlength m = Zlength t ->
  0 < i < Zlength m ->
  Forall (fun x => 0 <= x < 2^16) t ->
  -2^16 <= nth (Z.to_nat i) (sub_step i m t) 0 <= 0.
Proof.
intros i m t Hmt Him HPt.
rewrite nth_i_substep ; auto.
unfold subst_0xffffc.
assert(HP0: 0 ≤ 0 ∧ 0 < 2 ^ 16) by (split ; try omega ; apply Z.gt_lt ; apply pown0 ; omega).
assert(0 ≤ (nth (Z.to_nat i) t 0) ∧ (nth (Z.to_nat i) t 0) < 2 ^ 16).
apply Forall_nth_d; assumption.
assert(HZlandminmax:= and_0_or_1 (nth (Z.to_nat (i - 1)) m 0 ≫ 16)).
assert(HZland: Z.land (nth (Z.to_nat (i - 1)) m 0 ≫ 16) 1 = 0 \/ Z.land (nth (Z.to_nat (i - 1)) m 0 ≫ 16) 1 = 1) by omega.
destruct HZland as [HZland|HZland]; rewrite HZland.
all: change (2^16) with 65536 in * ; omega.
Qed.

Lemma subst_select_step_Zlength : forall i m t,
  0 < i < Zlength m->
  Zlength (sub_step i m t) = Zlength m.
Proof.
  intros.
  unfold sub_step.
  assert(0 < Z.to_nat i /\ Z.to_nat i < Zlength m) by (rewrite ?Z2Nat.id ; omega).
  assert(Z.of_nat (Z.to_nat (i - 1)) = (Z.of_nat (Z.to_nat i)) - 1) by (rewrite ?Z2Nat.id ; omega).
  repeat rewrite ?upd_nth_Zlength ; try omega.
Qed.

Local Lemma sub_fn_rev_Zlength_ind_step : forall i m t,
  0 < i < Zlength m ->
  Zlength (sub_fn_rev 1 sub_step i m t) = Zlength m ->
  Zlength (sub_fn_rev 1 sub_step (i+1) m t) = Zlength m.
Proof.
intros i m t Him Hind.
rewrite sub_fn_rev_equation.
flatten.
replace ( i + 1 - 1) with i by omega.
rewrite <- Hind.
apply subst_select_step_Zlength.
rewrite Hind.
assumption.
Qed.

Lemma sub_fn_rev_Zlength : forall i m t,
  Zlength m = 16 ->
  0 < i < Zlength m ->
  Zlength (sub_fn_rev 1 sub_step i m t) = Zlength m.
Proof.
intros.
change(Zlength (sub_fn_rev 1 sub_step i m t) = Zlength m) with
  ((fun x => Zlength (sub_fn_rev 1 sub_step x m t) = Zlength m) i).
apply P016_impl.
by rewrite sub_fn_rev_1.
intros ; apply sub_fn_rev_Zlength_ind_step.
2: apply H2.
all: omega.
Qed.

Close Scope Z.

author: ildyria

repo: coq-verif-tweetnacl