# Help to criate my first proof

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.
``````

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.