(* IMO 1972/B2, (c) 2006 Pierre Corbineau *)

Require Import Reals.
Set Firstorder Depth 2.
Open Scope R_scope.

(*
Problem B2

f and g are real-valued functions defined on the real line. 
For all x and y, f(x + y) + f(x - y) = 2f(x)g(y). 
f is not identically zero and |f(x)| <= 1 for all x. 
Prove that |g(x)| <= 1 for all x.
*)
 
Theorem B2: forall f g : R -> R , 
(forall x  y, f(x + y) + f (x - y) = 2 * f x * g y) ->
(~ forall x, f x = 0) -> (forall x, Rabs (f x) <= 1) ->
 (forall x, Rabs (g x) <= 1).

(*
Solution

Let k be the least upper bound for |f(x)|. 
Suppose |g(y)| > 1. 
Take any x with |f(x)| > 0, 
then 2k <= |f(x+y)| + |f(x-y)| <= |f(x+y) + f(x-y)| = 2|g(y)||f(x)|, 
so |f(x)| < k/|g(y)|. 
In other words, k/|g(y)| is an upper bound for |f(x)| which is less than k. 
Contradiction.
*)

proof. 

claim bigger_2_0: (2 > 0).
  have (2 > 0)%nat.
  hence (INR 2> INR 0) by lt_INR.
end claim.

let f,g be such that 
    fge : (forall x y : R, f (x + y) + f (x - y) = 2 * f x * g y)
and nzf:(~ (forall x : R, f x = 0))
and bf:(forall x : R, Rabs (f x) <= 1).

define f_abs_image z as (exists x, Rabs (f x) = z). 

let y:R.
per cases of (Rabs (g y) <= 1 \/ 1 < Rabs (g y)) by Rle_or_lt.

suppose (Rabs (g y) <= 1).
  hence thesis.

suppose (1 < Rabs (g y)).
  then hy:(Rabs (g y) > 1).
  
  claim (is_upper_bound f_abs_image 1). 
    given z,x such that e:(Rabs (f x) = z).
    have (Rabs (f x) <= 1) by bf.
    hence thesis by e.
  end claim.
  then hb:(bound f_abs_image).
  have (f_abs_image (Rabs (f 0))) by tactic exists 0;reflexivity.
  then hnv:(exists x, f_abs_image x).
  consider k such that 
    bkf:(is_upper_bound f_abs_image k) and 
    ubkf:(forall l:R, is_upper_bound f_abs_image l -> k <= l)
  from (completeness f_abs_image hb hnv). 

  claim ub:(forall x, Rabs (f x) <= k).
    let x:R.
    have (f_abs_image (Rabs (f x))) by 
    tactic exists x;reflexivity.
    hence thesis by bkf.
  end claim.

  claim new_bound:(forall x, Rabs (f x) <= k / (Rabs (g y))).
    let x:R.
    have b1:(Rabs (f (x+y))<= k) by ub.
    have b2:(Rabs (f (x-y))<= k) by ub.
    have c1:(Rabs (f (x+y)) + Rabs (f (x-y)) <= k + k) 
      by (Rplus_le_compat _ _ _ _ b1 b2).
    have c2:(Rabs (f (x+y) + f (x-y)) <= Rabs (f (x+y)) + Rabs (f (x-y))) 
      by Rabs_triang.
    have c3:(Rabs (f (x+y) + f (x-y)) <= k + k) by Rle_trans,c2,c1 .
    have (Rabs (f (x + y) + f (x - y)) = Rabs (2 * f x * g y)) by fge.
      ~= (Rabs 2 * Rabs (f x) * Rabs (g y)) by Rabs_mult. 
      ~= (2 * Rabs (f x) * Rabs (g y)) by Rabs_pos_eq,bigger_2_0.
    then c4:(2 * Rabs (f x) * Rabs (g y) <= k+k) by c3.
    have (k + k = 2*k) by tactic field.
    then c5:(2 * (Rabs (f x) * Rabs (g y)) <= 2*k) by Rmult_assoc,c4.
    then c6:(Rabs (f x) * Rabs (g y) <= k) by Rmult_le_reg_l,bigger_2_0.
    have hh: (0 <1).
    then nn:(0 < (Rabs (g y))) by Rlt_trans,hy.
    then cc: (0 < /(Rabs (g y))) by Rinv_0_lt_compat.
    then c7:(0 <= /(Rabs (g y))).
    then (Rabs (f x) * Rabs (g y) * / (Rabs (g y)) <= k * / Rabs (g y)) 
      by Rmult_le_compat_r,c6.
    then c8:(Rabs (f x) * (Rabs (g y) * / (Rabs (g y))) <= k * / Rabs (g y)) 
      by Rmult_assoc.
    have nngy:((Rabs (g y))<>0) by Rlt_not_eq,nn.
    then ( Rabs (g y) * / Rabs (g y) = 1) by Rinv_r. 
    then c9:(Rabs (f x)  <= k * / Rabs (g y)) by c8,Rmult_1_r. 
    hence thesis.
  end claim.

  claim nub:(is_upper_bound f_abs_image (k / (Rabs (g y)))).
    given z:R,x:R such that e:(Rabs (f x)=z).
    have (Rabs (f x) <= (k / (Rabs (g y)))) by new_bound.
    hence thesis by e.
  end claim.

  have contra_1:(k <= k / (Rabs (g y))) by (ubkf _ nub). 

  per cases of (k <= 0 \/ 0 < k) by Rlt_le_dec.
  suppose pk: (0 < k).
    have (1<Rabs (g y)) by hy.
    then (/ Rabs (g y) < /1) by Rinv_1_lt_contravar.
    then (k/ Rabs (g y) < k */1) by Rmult_lt_compat_l,pk .
    then contra_2:(k/ Rabs (g y) < k) by Rinv_1,Rmult_1_r. 
    thus thesis by Rle_not_lt,contra_1,contra_2.
  suppose npk: (k <= 0). 
    claim (forall x, f x = 0).
      let x:R.
      claim (f_abs_image (Rabs (f x))).
        take x.
        thus thesis.
      end claim.
      then hh:(Rabs (f x) <= k) by bkf.
      then rn:(Rabs (f x) <= 0) by Rle_trans,npk.
      have rp:(0 <= Rabs (f x)) by Rabs_pos.
      then e:(Rabs (f x) = 0) by Rle_antisym,rn.
      per cases of (f x = 0 \/ f x <> 0) by Req_dec.
      suppose (f x = 0).
        hence thesis.
      suppose (f x <> 0).
        then (Rabs (f x) <> 0) by Rabs_no_R0.
        hence thesis by e.
      end cases.
    end claim.
    hence thesis by nzf.
  end cases.
end cases.
end proof.
Qed.