(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect.
Require Import dataset.
Require Import real.
Require Import realsyntax.
Require Import Setoid.
Require Import realprop.

Set Implicit Arguments.
Unset Strict Implicit.

Section IMO.

Open Scope real_scope.

Variable R : real_model.

(* Because of the limitations of Coq v8.1 Setoid tactics, we need to repeat *)
(* some of the boilerplate from file realprop.v. here.                      *)

Hint Resolve eqr_refl leqrr ltrW.

Let ltr01 := (ltr01 R).
Let ltr02 := (ltr02 R).

Add Relation (real_carrier R) (@eqr R)
  transitivity proved by (@eqr_trans R)
  reflexivity proved by (@eqr_refl R)
  symmetry proved by (@eqr_sym R)
  as eqr_theory_approx.

Add Morphism (@leqr R) with
  signature (@eqr R) ==> (@eqr R) ==> iff as leqr_morphism_approx.
Proof. exact: leqr_morphism. Qed.

Add Morphism (@addr R) with
  signature (@eqr R) ==> (@eqr R) ==> (@eqr R) as addr_morphism_approx.
Proof. exact: addr_morphism. Qed.

Add Morphism (@oppr R) with
  signature (@eqr R) ==> (@eqr R) as oppr_morphism_approx.
Proof. exact: oppr_morphism. Qed.

Add Morphism (@mulr R) with
  signature (@eqr R) ==> (@eqr R) ==> (@eqr R) as mulr_morphism_approx.
Proof. exact: mulr_morphism. Qed.

Add Morphism (@maxr R) with
  signature (@eqr R) ==> (@eqr R) ==> (@eqr R) as maxr_morphism_approx.
Proof. exact: maxr_morphism. Qed.

Definition absr (x : R) := max x (-x).

Add Morphism absr with
  signature (@eqr R) ==> (@eqr R) as absr_morphism.
Proof. by rewrite /absr => ? ? ->. Qed.

Notation "`| x |" := (absr x) (at level 0, x at level 70, format "`| x |").

Lemma leqr_add : forall x1 y1 x2 y2 : R,
  x1 <= x2 -> y1 <= y2 -> x1 + y1 <= x2 + y2.
Proof.
move=> x1 y1 x2 y2; rewrite -(leqr_add2r y1) -(leqr_add2l x2 y1).
exact: leqr_trans.
Qed.

Lemma leqr_0add : forall x y : R, 0 <= x -> 0 <= y -> 0 <= x + y.
Proof.  move=> *; rewrite -(addr0 0); exact: leqr_add. Qed.

Lemma leqr_0mul : forall x y : R, 0 <= x -> 0 <= y -> 0 <= x * y.
Proof.  move=> x *; rewrite -(mulr0 x); exact: (mulr_monotony R). Qed.

Lemma absr_cases : forall x : R, 0 <= x \/ 0 <= -x.
Proof. move=> x; rewrite -(leqr_opp2 _ 0) oppr0; exact: leqr_total. Qed.

Lemma maxrC : forall x y : R, maxr x y == maxr y x.
Proof.
suff: forall x y : R, max x y <= max y x by split.
move=> x y; rewrite leqr_max; split; [exact: leqr_maxr | exact: leqr_maxl].
Qed.

Lemma absr_opp : forall x, `|-x| == `|x|.
Proof. by move=> x; rewrite /absr maxrC oppr_opp. Qed.

Lemma leqr_abs : forall x, x <= `|x|.
Proof. by move=> x; exact: leqr_maxl. Qed.

Lemma leqr_0abs : forall x, 0 <= `|x|.
Proof.
move=> x; wlog ?: x / x >= 0; last exact: leqr_trans (leqr_abs _).
by case: (absr_cases x) => *; last rewrite -absr_opp; auto.
Qed.

Lemma absr_eq : forall x, 0 <= x -> `|x| == x.
Proof.
move=> x Hx; split; [rewrite /absr leqr_max; split=> // | exact: leqr_abs].
by apply: leqr_trans (Hx); rewrite -oppr0 leqr_opp2. 
Qed.

Lemma absr_eq0 : forall x, `|x| == 0 -> x == 0.
Proof.
move=> x; case (absr_cases x); last rewrite -absr_opp; move/absr_eq=> -> //.
by move/oppr_morphism; rewrite oppr_opp oppr0.
Qed.

Lemma absr_mul: forall x y, `|x * y| == `|x| * `|y|.
Proof.
move=> x y; wlog Hx: x / x >= 0 => [Hpos|].
  by case (absr_cases x); move/Hpos; last rewrite mulr_oppl !absr_opp.
wlog Hy: y / y >= 0 => [Hpos|].
  by case (absr_cases y); move/Hpos; last rewrite mulr_oppr !absr_opp.
rewrite !absr_eq //; exact: leqr_0mul.
Qed.

Lemma absr_add: forall x y, `|x + y| <= `|x| + `|y|.
Proof.
move=> x y; wlog Hx: x y / x + y >= 0 => [Hpos|].
  case (absr_cases (x + y)); last rewrite oppr_add; move/Hpos=> //.
  by rewrite -oppr_add !absr_opp.
rewrite absr_eq //; apply: leqr_add; exact: leqr_abs.
Qed.

Implicit Arguments leqr_pmul2l [R x x1 x2].
Implicit Arguments leqr_pmul2r [R x x1 x2].

Lemma pdivrr : forall x : R, x > 0 -> x / x == 1.
Proof. by move=> *; apply divrr => [[Hx _]]; eauto. Qed. 

Lemma pmulrK : forall x y : R, y > 0 -> x * y / y == x.
Proof. by move=> *; rewrite -mulrA pdivrr ?mulr1. Qed.

Lemma pdivrK : forall x y : R, y > 0 -> x / y * y == x.
Proof. by move=> *; rewrite mulrC mulrCA mulrA pmulrK. Qed.

Lemma leqr_pdivr : forall x1 x2 y : R, y > 0 -> 
 (x1 <= x2 / y <-> x1 * y <= x2).
Proof. by move=> ? ? ? Hy; rewrite -(leqr_pmul2r Hy) pdivrK. Qed.

Lemma IMO : forall f g,
  (forall x y : R, f (x + y) + f (x - y) == 2 * f x * g y) ->
  ~ (forall x, f x == 0) ->
  (forall x, `|f x| <= 1) ->
  forall y, `|g y| <= 1.
Proof.
move=> f g Efg Hf0 Hf1 y.
without loss Hgy: / `|g y| > 0.
  case: (leqr_total 1 `|g y|) => // Hy; apply; exact: ltr_leq_trans _ Hy.
pose k := sup {z | exists x, z == `|f x|}.
have{Hf1} Hfk: `|f _| <= k.
  by move=> x; apply: ubr_sup; [exists (1 : R) => _ [? ->] | exists x].
have{Hf0} Hk: k > 0.
  move=> Hk; elim: Hf0 => x; apply: absr_eq0.
  split; [exact: leqr_trans Hk | exact: leqr_0abs].
suffices: k <= k / `|g y| by rewrite leqr_pdivr // mulrC -leqr_pdivr // pdivrr.
suffices: `|f _| <= k / `|g y| => [Hf|x].
  by apply: leqr_sup_ub => [|_ [x ->]]; first by exists `|f y|; exists y.
suffices: `|f x * g y| <= k by rewrite absr_mul -leqr_pdivr.
have{Efg} Ek: `|2 * f x * g y| <= 2 * k.
  rewrite -Efg mul2r; apply: leqr_trans (absr_add _ _) _; exact: leqr_add.
by do [rewrite -mulrA absr_mul absr_eq ?leqr_pmul2l; auto] in Ek.
Qed.

End IMO.