Help to criate my first proof

Using Coq
1

Hi

I what to proof this proposition:

But I’m facing difficult to finish the coq code.

someone can help me?

regards

Require Import Reals.
Open Scope R_scope.

(*f(xj) is non-linear*)
(*/\ represent 'and'*)
Definition additive (f : R -> R) := forall x y : R, f (x + y) = f x + f y.
Definition homogeneous_deg_one (f : R -> R) := forall x a : R, f (a * x) = a * f x.
Definition linear (f : R -> R) := additive f /\ homogeneous_deg_one f.
Definition non_linear (f : R -> R) := ~ linear f.
                                                                           
(*f(xj)>0*)
Definition positive_for_all (f : R -> R) := forall xj : R, f xj > 0.

(*f′(xj)<0*)
Definition derivative (f : R -> R) (x : R) := (f (x + 1/1000) - f x) / 1/1000.                              
Definition decreasing_at (f f' : R -> R) (xj : R) := f' xj < 0.
                                              
(*f′(xj)=f′(xi), such that j and i are different*) 
Definition equal_derivatives_at_different_points (f : R -> R) (xi xj : R) := xi <> xj /\ derivative f xi = derivative f xj.
                                              
                                              
(*exist G(X)=f′(x1)+f′(x2)+⋯+f′(xJ) and X=x1+x2+⋯+xJ *)
Require Import List.
Import ListNotations.
Fixpoint sum_list (l : list R) : R :=
  match l with
  | [] => 0
  | x :: xs => x + sum_list xs
  end.
Definition sum_derivatives (f' : R -> R) (l : list R) := sum_list (map f' l).
Definition exists_G (f' : R -> R) :=
  exists G : R -> R, forall l : list R, G (sum_list l) = sum_derivatives f' l.                                      


(*Lemma*)                                                         
Parameter my_f : R -> R.
Lemma my_function_is_0 : non_linear my_f.
Lemma my_function_is_1 : positive_for_all my_f.
Lemma my_function_is_2 : decreasing_at my_f.
Lemma my_function_is_3 : equal_derivatives_at_different_points my_f. 
                                                         
(*Hypothesis*)
Parameter a : R.
Parameter L : R -> R.
(*Hypothesis L_is_linear : exists m b : R, forall x : R, L x = m * x + b.*)
Lemma L_function_is_linear : linear L.
Definition ff (x : R) := a * x^2 + L x.

Hypothesis my_f_equals_f : forall x : R, my_f x = f x.
2

First remark. Looking at your code it is patent that it is your first proof and you don’t understand the meaning of commands yet. I suggest you start with a much easier proof.

Here are the points you need to understand first:

  • Lemma is to start a proof of a lemma. It makes coq switch to “proof interactive mode”. If you just want to state a hypothesis for a lemma that you want to prove then you should declare with Hypothesis inside a Section like this:
Section S.
  Parameter my_f : R -> R.
  Hypothesis my_function_is_0 : non_linear my_f.
  Hypothesis my_function_is_1 : positive_for_all my_f.
  Hypothesis my_function_is_2 : decreasing_at my_f.
  Hypothesis my_function_is_3 : equal_derivatives_at_different_points my_f. 

  Lemma exists m b : R, forall x : R, my_f x = m * x + b.
  Proof.
    (* interactive proofs mode: use tactic to prove your goal *)
  Qed. (* this will be accepted only iuf you manage to finish the proof. Otherwise change this to "Admitted".*)
End S.

It is also possible (simpler?) to state the lemma directly with its hypothesis inlined:

Lemma shape: forall myf: R -> R,
  non_linear my_f ->
  positive_for_all my_f ->
  ... ->
   exists m b, forall x, my_f x = ....
Proof.
 <start the proof here>

Note that your definition are not correct and do not compile. But this is the global structure you should use. Again: you should definitely start with much easier lemmas.