I have that for all j
in {1, 2, .. N}
such that j ≠ i
it holds that a_j ≤ b_j
. I want to prove in Coq that
How can I do that and what modules are the best for these kinds of manipulations?
I have that for all j
in {1, 2, .. N}
such that j ≠ i
it holds that a_j ≤ b_j
. I want to prove in Coq that
How can I do that and what modules are the best for these kinds of manipulations?
The mathematical components library has a theory of "big" operations with lots of lemmas. Here is how one might prove your result:
From mathcomp Require Import all_ssreflect.
Lemma test N (f g : nat -> nat) (i : 'I_N) :
(forall j, j != i -> f i <= g i) ->
\sum_(j < N | j != i) f i <= \sum_(j < N | j != i) g i.
Proof. move=> f_leq_g; exact: leq_sum. Qed.
Edit
If you want to reason about operations over the real numbers, you will also need to install the mathematical components analysis library. Here is how one might adapt this proof to work over the real numbers:
(* Bring real numbers into scope, as well as
the theory of algebraic and numeric structures *)
Require Import Coq.Reals.Reals.
From mathcomp Require Import all_ssreflect ssralg ssrnum Rstruct reals.
(* Change summation and other notations to work over rings
rather than the naturals *)
Local Open Scope ring_scope.
Lemma test N (f g : nat -> R) (i : 'I_N) :
(forall j, j != i -> f i <= g i) ->
\sum_(j < N | j != i) f i <= \sum_(j < N | j != i) g i.
Proof. move=> f_leq_g; exact: Num.Theory.ler_sum. Qed.
You can do this without the mathematical components library using lia
and induction.
Require Import Arith.
Require Import Lia.
Fixpoint sum (f: nat -> nat) (N: nat) :=
match N with
| 0 => 0
| S m => f 0 + sum (fun x => f (S x)) m
end.
Fixpoint sum_except (f: nat -> nat) (i : nat) (N: nat) {struct N} :=
match N with
| 0 => 0
| S m =>
match i with
| 0 => 0 + sum (fun x => f (S x)) m
| S j => f 0 + sum_except (fun x => f (S x)) j m
end
end.
Lemma SumLess : forall N a b,
(forall j, a j <= b j) ->
sum a N <= sum b N.
Proof.
induction N.
- simpl; lia.
- intros; simpl.
admit. (* I'll leave this as an exercise. Use lia. *)
Qed.
Lemma SumExceptLess :
forall N i a b,
(forall j, not (j = i) ->
a j <= b j) ->
sum_except a i N <= sum_except b i N.
Proof.
induction N.
- simpl. lia.
- destruct i.
simpl.
+ intros.
apply SumLess; auto.
+ intros; simpl.
admit. (* Again, I'll leave this for you to discover. Use lia. Follow the same pattern as you did in SumLess. *)
Qed.