From mathcomp Require Import all_ssreflect finmap.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

Set Implicit Arguments.
Unset Strict Implicit.

(******************************************************************************)
(*                                                                            *)
(*   Extra theorems and definitions                                           *)
(*                                                                            *)
(******************************************************************************)

(******************************************************************************)
(*                                                                            *)
(*   Extra theorems about lists                                               *)
(*                                                                            *)
(******************************************************************************)


Lemma rcons_injl (A : Type) (a: seq A) : injective (rcons a).
A:Type
a:seq A
injective (rcons a)
Proof.
2 by elim: a => /= [s1 s2 /= [] | b l IH s1 s2 [] /IH]. Qed.

Lemma rcons_injr (A : Type) (a: A) : injective (rcons ^~a).
5
a:A
injective (rcons^~ a)
Proof.
a
elim => [ [|b [|c]] //= | b s1 IH /= [/= [] -> |c s2 [] -> /IH-> //]].
5
a, b:A
s1:seq A
IH:forall x2 : seq A,
rcons s1 a = rcons x2 a -> s1 = x2
rcons s1 a = [::] -> a :: s1 = [::]
by case: (s1) => // [] [].
Qed.

Lemma cat_injl (A : Type) (a: seq A) : injective (cat a).
4
injective (cat a)
Proof.
19 by elim: a => // b l IH s1 s2 /= [] /IH. Qed.

Lemma cat_injr (A : Type) (a: seq A) : injective (cat ^~a).
4
injective (cat^~ a)
Proof.
1e
elim: a => [s1 s2 |b l IH s1 s2]; first by rewrite !cats0.
5
b:A
l:seq A
IH:injective (cat^~ l)
s1, s2:seq A
s1 ++ b :: l = s2 ++ b :: l -> s1 = s2
by rewrite -!cat_rcons => /IH; apply: rcons_injr.
Qed.

Lemma in_split (A : eqType) (a : A)  l :
  a \in l -> exists l1, exists l2, l = l1 ++ a :: l2.
A:eqType
d
l:seq_predType A
a \in l -> exists l1 l2 : seq A, l = l1 ++ a :: l2
Proof.
2c
elim: l => //= b l IH; rewrite inE => /orP[/eqP<-|aIl].
2f1427
IH:a \in l ->
exists l1 l2 : seq A, l = l1 ++ a :: l2
exists l1 l2 : seq A, a :: l = l1 ++ a :: l2
2f142737
aIl:a \in l
exists l1 l2 : seq A, b :: l = l1 ++ a :: l2
  by exists [::]; exists l.
3b
3d
case: (IH aIl) => l1 [l2 lE].
2f1427373c
l1, l2:seq A
lE:l = l1 ++ a :: l2
3d
by exists (b :: l1); exists l2; rewrite /= lE.
Qed.

Lemma split_first (A : eqType) (l : seq A) (P : pred A) :
  ~~ all [predC P] l -> {bl1l2 : (A * seq A * seq A) |
    [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1 &  
             l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}.
2f27
P:pred A
~~ all [predC P] l ->
{bl1l2 : A * seq A * seq A
| [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1
    & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
Proof.
48
elim: l => //= b l IH.
2f4b2627
IH:~~ all [predC P] l ->
{bl1l2 : A * seq A * seq A
| [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1
    & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
~~ ((b \notin P) && all [predC P] l) ->
{bl1l2 : A * seq A * seq A
| [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1
    & b :: l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
rewrite negb_and negbK; case: (boolP (b \in P)) =>
      [bIP _| bNIP /= /IH [[[c l1] l2] [H1 H2 ->]]].
2f4b262752
bIP:b \in P
{bl1l2 : A * seq A * seq A
| [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1
    & b :: l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
2f4b262752
bNIP:b \notin P
c:A
45
H1:all [predC P] (c, l1, l2).1.2
H2:P (c, l1, l2).1.1
{bl1l2 : A * seq A * seq A
| [/\ all [predC P] bl1l2.1.2, P bl1l2.1.1
    & b
      :: (c, l1, l2).1.2 ++
         (c, l1, l2).1.1 :: (c, l1, l2).2 =
      bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
  by exists (b, [::], l); split.
5c
61
by exists (c, b :: l1, l2); split; rewrite /= ?bNIP.
Qed.

Lemma split_last (A : eqType) (l : seq A) (P : pred A) :
  ~~ all [predC P] l  -> 
  {bl1l2 | [/\  P bl1l2.1.1, all [predC  P] bl1l2.2 &  
                l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}.
4a
~~ all [predC P] l ->
{bl1l2 : A * seq A * seq A
| [/\ P bl1l2.1.1, all [predC P] bl1l2.2
    & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
Proof.
66
move=> lA.
2f274b
lA:~~ all [predC P] l
{bl1l2 : A * seq A * seq A
| [/\ P bl1l2.1.1, all [predC P] bl1l2.2
    & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
case: (@split_first _ (rev l) P); first by rewrite all_rev.
6d
forall x : A * seq A * seq A,
[/\ all [predC P] x.1.2, P x.1.1
  & rev l = x.1.2 ++ x.1.1 :: x.2] ->
{bl1l2 : A * seq A * seq A
| [/\ P bl1l2.1.1, all [predC P] bl1l2.2
    & l = bl1l2.1.2 ++ bl1l2.1.1 :: bl1l2.2]}
move=> [[b l1] l2] [H1 H2 H3].
2f274b6e2645
H1:all [predC P] (b, l1, l2).1.2
H2:P (b, l1, l2).1.1
H3:rev l =
(b, l1, l2).1.2 ++
(b, l1, l2).1.1 :: (b, l1, l2).2
6f
exists (b, rev l2, rev l1); split => //; first by rewrite all_rev.
77
l =
(b, rev l2, rev l1).1.2 ++
(b, rev l2, rev l1).1.1 :: (b, rev l2, rev l1).2
by rewrite -{1}[l]revK H3 rev_cat /= rev_cons cat_rcons.
Qed.

Lemma split_head (A : eqType) (a b : A) l1 l2 l3 l4 :
  l1 ++ a :: l2 = l3 ++ b :: l4 ->
  [\/ [/\ l1 = l3, a = b & l2 = l4],
      exists l5, l3 = l1 ++ a :: l5 |
      exists l5, l1 = l3 ++ b :: l5].
2f14
l1, l2, l3, l4:seq A
l1 ++ a :: l2 = l3 ++ b :: l4 ->
[\/ [/\ l1 = l3, a = b & l2 = l4],
    exists l5 : seq A, l3 = l1 ++ a :: l5
  | exists l5 : seq A, l1 = l3 ++ b :: l5]
Proof.
80
elim: l1 l3 => /= [[[<- <-]|c l3 [<- ->]] /= | c l1 IH [[<- <-]|d l3 /= [<-]]].
2f14
l2, l4:seq A
[\/ [/\ [::] = [::], a = a & l2 = l2],
    exists l5 : seq A, [::] = a :: l5
  | exists l5 : seq A, [::] = a :: l5]
2f148a5e
l3:seq A
[\/ [/\ [::] = a :: l3, a = b & l3 ++ b :: l4 = l4],
    exists l5 : seq A, a :: l3 = a :: l5
  | exists l5 : seq A, [::] = a :: l3 ++ b :: l5]
2f148a5e
l1:seq A
IH:forall l3 : seq A,
l1 ++ a :: l2 = l3 ++ b :: l4 ->
[\/ [/\ l1 = l3, a = b & l2 = l4],
    exists l5 : seq A, l3 = l1 ++ a :: l5
  | exists l5 : seq A, l1 = l3 ++ b :: l5]
[\/ [/\ c :: l1 = [::], a = c & l2 = l1 ++ a :: l2],
    exists l5 : seq A, [::] = c :: l1 ++ a :: l5
  | exists l5 : seq A, c :: l1 = [::] ++ c :: l5]
2f148a5e9394
d:A
8f
l1 ++ a :: l2 = l3 ++ b :: l4 ->
[\/ [/\ c :: l1 = c :: l3, a = b & l2 = l4],
    exists l5 : seq A, c :: l3 = c :: l1 ++ a :: l5
  | exists l5 : seq A, c :: l1 = c :: l3 ++ b :: l5]
-
87 by apply: Or31.
8e
90
9196
-
9c by apply: Or32; exists l3.
92
95
96
-
a1 by apply: Or33; exists l1.
97
99
move=> /IH[[<- <- <-]|[l5 ->]|].
97
[\/ [/\ c :: l1 = c :: l1, a = a & l2 = l2],
    exists l5 : seq A, c :: l1 = c :: l1 ++ a :: l5
  | exists l5 : seq A, c :: l1 = c :: l1 ++ a :: l5]
2f148a5e939498
l3, l5:seq A
[\/ [/\ c :: l1 = c :: l1 ++ a :: l5, a = b & l2 = l4],
    exists l6 : seq A,
      c :: l1 ++ a :: l5 = c :: l1 ++ a :: l6
  | exists l6 : seq A,
      c :: l1 = c :: (l1 ++ a :: l5) ++ b :: l6]
97
(exists l5 : seq A, l1 = l3 ++ b :: l5) ->
[\/ [/\ c :: l1 = c :: l3, a = b & l2 = l4],
    exists l5 : seq A, c :: l3 = c :: l1 ++ a :: l5
  | exists l5 : seq A, c :: l1 = c :: l3 ++ b :: l5]
-
a9 by apply: Or31.
ae
b0
b1
-
b5 by apply: Or32; exists l5.
97
b2
by case=> l5 ->; apply: Or33; exists l5.
Qed.

Lemma split_tail (A : eqType) (a b : A) l1 l2 l3 l4 :
  l1 ++ a :: l2 = l3 ++ b :: l4 ->
  [\/ [/\ l1 = l3, a = b & l2 = l4],
      exists l5, l4 = l5 ++ a :: l2 |
      exists l5, l2 = l5 ++ b :: l4].
82
l1 ++ a :: l2 = l3 ++ b :: l4 ->
[\/ [/\ l1 = l3, a = b & l2 = l4],
    exists l5 : seq A, l4 = l5 ++ a :: l2
  | exists l5 : seq A, l2 = l5 ++ b :: l4]
Proof.
bd
elim/last_ind : l2 l4 => [l4|l2 c IH l4].
2f14
l1, l3, l4:seq A
l1 ++ [:: a] = l3 ++ b :: l4 ->
[\/ [/\ l1 = l3, a = b & [::] = l4],
    exists l5 : seq A, l4 = l5 ++ [:: a]
  | exists l5 : seq A, [::] = l5 ++ b :: l4]
2f14
l1, l3, l2:seq A
5e
IH:forall l4 : seq A,
l1 ++ a :: l2 = l3 ++ b :: l4 ->
[\/ [/\ l1 = l3, a = b & l2 = l4],
    exists l5 : seq A, l4 = l5 ++ a :: l2
  | exists l5 : seq A, l2 = l5 ++ b :: l4]
l4:seq A
l1 ++ a :: rcons l2 c = l3 ++ b :: l4 ->
[\/ [/\ l1 = l3, a = b & rcons l2 c = l4],
    exists l5 : seq A, l4 = l5 ++ a :: rcons l2 c
  | exists l5 : seq A, rcons l2 c = l5 ++ b :: l4]
  case: (lastP l4) => /= [|l5 c].
c4
l1 ++ [:: a] = l3 ++ [:: b] ->
[\/ [/\ l1 = l3, a = b & [::] = [::]],
    exists l5 : seq A, [::] = l5 ++ [:: a]
  | exists l5 : seq A, [::] = l5 ++ [:: b]]
2f14
l1, l3, l4, l5:seq A
5e
l1 ++ [:: a] = l3 ++ b :: rcons l5 c ->
[\/ [/\ l1 = l3, a = b & [::] = rcons l5 c],
    exists l6 : seq A, rcons l5 c = l6 ++ [:: a]
  | exists l6 : seq A, [::] = l6 ++ b :: rcons l5 c]
c8
    rewrite !cats1 => /rcons_inj[<- <-].
c4
[\/ [/\ l1 = l1, a = a & [::] = [::]],
    exists l5 : seq A, [::] = l5 ++ [:: a]
  | exists l5 : seq A, [::] = l5 ++ [:: a]]
d2
    by apply: Or31.
d4
d6
c7
  rewrite cats1 -rcons_cons -rcons_cat => /rcons_inj[-> <-].
d4
[\/ [/\ l3 ++ b :: l5 = l3, a = b & [::] = rcons l5 a],
    exists l6 : seq A, rcons l5 a = l6 ++ [:: a]
  | exists l6 : seq A, [::] = l6 ++ rcons (b :: l5) a]
c7
  by apply: Or32; exists l5; rewrite cats1.
c9
cd
case: (lastP l4) => /= [|l5 d].
c9
l1 ++ a :: rcons l2 c = l3 ++ [:: b] ->
[\/ [/\ l1 = l3, a = b & rcons l2 c = [::]],
    exists l5 : seq A, [::] = l5 ++ a :: rcons l2 c
  | exists l5 : seq A, rcons l2 c = l5 ++ [:: b]]
2f14ca5ecb
l4, l5:seq A
98
l1 ++ a :: rcons l2 c = l3 ++ b :: rcons l5 d ->
[\/ [/\ l1 = l3, a = b & rcons l2 c = rcons l5 d],
    exists l6 : seq A,
      rcons l5 d = l6 ++ a :: rcons l2 c
  | exists l6 : seq A,
      rcons l2 c = l6 ++ b :: rcons l5 d]
  rewrite cats1 -rcons_cons -rcons_cat => /rcons_inj[<- ->].
c9
[\/ [/\ l1 = l1 ++ a :: l2, a = b & rcons l2 b = [::]],
    exists l5 : seq A, [::] = l5 ++ rcons (a :: l2) b
  | exists l5 : seq A, rcons l2 b = l5 ++ [:: b]]
e9
  by apply: Or33; exists l2; rewrite cats1.
eb
ed
rewrite -!rcons_cons -!rcons_cat => 
   /rcons_inj[/IH [[<- <- <-]|[l6 ->]|[l6 ->]]] <-.
eb
[\/ [/\ l1 = l1, a = a & rcons l2 c = rcons l2 c],
    exists l5 : seq A,
      rcons l2 c = l5 ++ rcons (a :: l2) c
  | exists l5 : seq A,
      rcons l2 c = l5 ++ rcons (a :: l2) c]
2f14ca5ecbec98
l6:seq A
[\/ [/\ l1 = l3, a = b
      & rcons l2 c = rcons (l6 ++ a :: l2) c],
    exists l5 : seq A,
      rcons (l6 ++ a :: l2) c =
      l5 ++ rcons (a :: l2) c
  | exists l5 : seq A,
      rcons l2 c = l5 ++ rcons (b :: l6 ++ a :: l2) c]
fb
[\/ [/\ l1 = l3, a = b
      & rcons (l6 ++ b :: l5) c = rcons l5 c],
    exists l7 : seq A,
      rcons l5 c = l7 ++ rcons (a :: l6 ++ b :: l5) c
  | exists l7 : seq A,
      rcons (l6 ++ b :: l5) c =
      l7 ++ rcons (b :: l5) c]
-
f6 by apply: Or31.
fb
fd
fe
-
102 by apply: Or32; exists l6; rewrite -rcons_cat.
fb
ff
by apply: Or33; exists l6; rewrite -rcons_cat.
Qed.

(******************************************************************************)
(* We develop a twisted version of split that fills 'I_{m + n} with           *)
(* first the element of 'I_n (x -> x) then the element of m (x -> x + n)      *)
(* This is mostly motivated to naturally get an element of 'I_n from 'I_n.+1  *)
(* by removing max_ord                                                        *)
(******************************************************************************)

Lemma tlshift_subproof m n (i : 'I_m) : i + n < m + n.
m, n:nat
i:'I_m
i + n < m + n
Proof.
10a by rewrite ltn_add2r. Qed.
Lemma trshift_subproof m n (i : 'I_n) : i < m + n.
10d
i:'I_n
i < m + n
Proof.
112 by apply: leq_trans (valP i) _; apply: leq_addl. Qed.

Definition tlshift m n (i : 'I_m) := Ordinal (tlshift_subproof n i).
Definition trshift m n (i : 'I_n) := Ordinal (trshift_subproof m i).

Lemma tlshift_inj m n : injective (@tlshift m n).
10d
injective (tlshift n)
Proof.
119 by move=> ? ? /(f_equal val) /addIn /val_inj. Qed.

Lemma trshift_inj m n : injective (@trshift m n).
11b
injective (trshift m (n:=n))
Proof.
11f by move=> ? ? /(f_equal val) /= /val_inj. Qed.

Lemma trshift_lift n (i : 'I_ n) : trshift 1 i = lift ord_max i.
n:nat
115
trshift 1 i = lift ord_max i
Proof.
124 by apply/val_eqP; rewrite /= /bump leqNgt ltn_ord. Qed.

Lemma tsplit_subproof m n (i : 'I_(m + n)) : i >= n -> i - n < m.
10d
i:'I_(m + n)
n <= i -> i - n < m
Proof.
12b by move/subSn <-; rewrite leq_subLR [n + m]addnC. Qed.

Definition tsplit {m n} (i : 'I_(m + n)) : 'I_m + 'I_n :=
  match ltnP (i) n with
  | LtnNotGeq lt_i_n =>  inr _ (Ordinal lt_i_n)
  | GeqNotLtn ge_i_n =>  inl _ (Ordinal (tsplit_subproof ge_i_n))
  end.

Variant tsplit_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
  | TSplitLo (j : 'I_n) of i = j :> nat : tsplit_spec i (inr _ j) true
  | TSplitHi (k : 'I_m) of i = k + n :> nat : tsplit_spec i (inl _ k) false.

Lemma tsplitP m n (i : 'I_(m + n)) : tsplit_spec i (tsplit i) (i < n).
12d
tsplit_spec i (tsplit i) (i < n)
Proof.
132
set lt_i_n := i < n; rewrite /tsplit.
10d12e
lt_i_n:=i < n:bool
tsplit_spec i
  match ltnP i n with
  | LtnNotGeq lt_i_n =>
      inr (Ordinal (n:=n) (m:=i) lt_i_n)
  | GeqNotLtn ge_i_n =>
      inl
        (Ordinal (n:=m) (m:=i - n)
           (tsplit_subproof (m:=m) (n:=n) (i:=i)
              ge_i_n))
  end lt_i_n
by case: {-}_ lt_i_n / ltnP; [left |right; rewrite subnK].
Qed.

Definition tunsplit {m n} (jk : 'I_m + 'I_n) :=
  match jk with inl j => tlshift n j | inr k => trshift m k end.


Lemma ltn_tunsplit m n (jk : 'I_m + 'I_n) : (n <= tunsplit jk) = jk.
10d
jk:('I_m + 'I_n)%type
(n <= tunsplit jk) = jk
Proof.
13d
by case: jk => [j|k]; rewrite /= ?ltn_ord ?leq_addl // leqNgt ltn_ord.
Qed.

Lemma tsplitK {m n} : cancel (@tsplit m n) tunsplit.
11b
cancel tsplit tunsplit
Proof.
144 by move=> i; apply: val_inj; case: tsplitP. Qed.

Lemma tunsplitK {m n} : cancel (@tunsplit m n) tsplit.
11b
cancel tunsplit tsplit
Proof.
149
move=> jk; have:= ltn_tunsplit jk; rewrite leqNgt.
13f
~~ (tunsplit jk < n) = jk -> tsplit (tunsplit jk) = jk
by do [case: tsplitP; case: jk => //= i j] => [|/addIn] => /ord_inj->.
Qed.

(******************************************************************************)
(*                                                                            *)
(*   Extra theorems about fset                                                *)
(*                                                                            *)
(******************************************************************************)

Open Scope fset_scope.

Definition sint a b : {fset nat} :=
   [fset @nat_of_ord _ i | i in 'I_b & a <= i].

Lemma mem_sint a b i : i \in sint a b = (a <= i < b).
a, b:nat
i:nat_choiceType
(i \in sint a b) = (a <= i < b)
Proof.
152
apply/imfsetP/idP => [[j /= aLj ->]|/andP[aLi iLb]].
155156
j:ordinal_choiceType b
aLj:j \in [pred x | a <= x]
a <= j < b
155156
aLi:a <= i
iLb:i < b
exists2 x : ordinal_choiceType b,
  in_mem x
    (mem_fin
       (subfinset_finpred (T:=ordinal_choiceType b)
          (mem_fin
             (fin_finpred
                (pT:=pred_finpredType
                       (ordinal_finType b)) 'I_b))
          (fun i : 'I_b => a <= i))) & i = x
  by rewrite ltn_ord andbT.
162
165
by exists (Ordinal iLb).
Qed.

Lemma sint_sub a b c : a <= c ->
   [fset i in  (sint a b) | c <= i] = sint c b.
a, b, c:nat
a <= c -> [fset i in sint a b | c <= i] = sint c b
Proof.
16a
move=> aLc.
16d
aLc:a <= c
[fset i in sint a b | c <= i] = sint c b
apply/fsetP => i.
16d174156
(i \in [fset i | i in sint a b & c <= i]) =
(i \in sint c b)
rewrite mem_sint.
179
(i \in [fset i | i in sint a b & c <= i]) =
(c <= i < b)
apply/imfsetP/idP => [[j /=]|/andP[cLi iLb]].
16d174
i, j:nat_choiceType
j
  \in [pred x in [eta mem_seq (T:=nat_choiceType)
                        (sint a b)] |
        c <= x] -> i = j -> c <= i < b
16d174156
cLi:c <= i
164
exists2 x : nat_choiceType,
  in_mem x
    (mem_fin
       (subfinset_finpred (T:=nat_choiceType)
          (mem_fin (fset_finpred (sint a b))) (leq c))) &
  i = x
  rewrite inE mem_sint => /andP[/andP[aLj jLb] cLj] ->.
16d174183
aLj:a <= j
jLb:j < b
cLj:c <= j
c <= j < b
185
  by rewrite cLj.
187
189
by exists i; rewrite //= inE mem_sint cLi iLb (leq_trans aLc).
Qed.

Lemma sintSl a b : sint a.+1 b = sint a b `\ a.
155
sint a.+1 b = sint a b `\ a
Proof.
196
apply/fsetP => /= i; rewrite !inE !mem_sint.
a, b, i:nat
(a < i < b) = [&& i != a, a <= i & i < b]
by do 2 case: ltngtP.
Qed.

Lemma sintSr a b : sint a b.+1 `\ b = sint a b.
198
sint a b.+1 `\ b = sint a b
Proof.
1a2
apply/fsetP => /= i; rewrite !inE !mem_sint ltnS.
19e
[&& i != b, a <= i & i <= b] = (a <= i < b)
by do 2 case: ltngtP.
Qed.

Lemma sint_split a b : sint a b = sint 0 b `\` sint 0 a.
198
sint a b = sint 0 b `\` sint 0 a
Proof.
1ab
by apply/fsetP => /= i; rewrite !inE !mem_sint /= -leqNgt.
Qed.

Lemma card_sint a b : #|`sint a b| = (b - a).
198
#|` sint a b| = b - a
Proof.
1b0
elim: b => [|b IH].
a:nat
#|` sint a 0| = 0 - a
155
IH:#|` sint a b| = b - a
#|` sint a b.+1| = b.+1 - a
  apply/eqP; rewrite cardfs_eq0; apply/eqP/fsetP=> i.
1b8156
(i \in sint a 0) = (i \in fset0)
1ba
  by rewrite mem_sint andbF inE.
1bc
1be
have [aLb|bLa] := leqP a b; last first.
1551bd
bLa:b < a
1be
1551bd
aLb:a <= b
1be
  rewrite (_ : _ - _ =  0); last first.
1ca
b.+1 - a = 0
1ca
#|` sint a b.+1| = 0
1cd
    by apply/eqP; rewrite subn_eq0.
1ca
1d6
1cc
  apply/eqP; rewrite cardfs_eq0; apply/eqP/fsetP=> i; rewrite mem_sint inE ltnS.
1551bd1cb156
(a <= i <= b) = false
1cc
  by apply/idP => /andP[H1 /(leq_trans H1)]; rewrite leqNgt bLa.
1ce
1be
rewrite (cardfsD1 b) (_ : _ \in _); last by rewrite mem_sint aLb /=.
1ce
(true + #|` sint a b.+1 `\ b|)%N = b.+1 - a
by rewrite sintSr IH subSn.
Qed.

Notation "`[ n ]" := (sint 0 n) (format "`[ n ]").

Lemma sint0_set0 : `[0] = fset0.
`[0] = fset0
Proof.
1e7  by apply/fsetP=> i; rewrite mem_sint inE; case: ltngtP. Qed.

Definition s2f n (s : {set 'I_n}) := [fset nat_of_ord i | i in s]. 

Lemma mem_s2f n (s : {set 'I_n}) (i : 'I_n) : (i : nat) \in s2f s = (i \in s).
127
s:{set 'I_n}
115
((i : nat) \in s2f (n:=n) s) = (i \in s)
Proof.
1ec
apply/imfsetP/idP => /= [[j jIs iEj]|iIs]; last by exists i.
1271ef
i, j:'I_n
jIs:j \in s
iEj:i = j
i \in s
by rewrite (_ : i = j) //; apply: val_inj.
Qed.

Lemma s2f_set0 n : s2f (set0 : {set 'I_n}) = fset0.
127
s2f (n:=n) (set0 : {set 'I_n}) = fset0
Proof.
1fb
apply/fsetP => i; rewrite inE.
127156
(i \in s2f (n:=n) set0) = false
by apply/idP => /imfsetP[j /=]; rewrite inE.
Qed.

Lemma s2f_setT n : s2f (setT : {set 'I_n}) = sint 0 n.
1fd
s2f (n:=n) ([set: ordinal_finType n] : {set 'I_n}) =
`[n]
Proof.
206
apply/fsetP => i; rewrite mem_sint /=.
203
(i \in s2f (n:=n) [set: 'I_n]) = (i < n)
apply/imfsetP/idP => /= [[j _ -> //]| iLn].
127156
iLn:i < n
exists2 x : 'I_n, x \in [set: 'I_n] & i = x
by exists (Ordinal iLn).
Qed.


Lemma s2fD n (s1 s2 : {set 'I_n}) : s2f (s1 :\: s2)  = s2f s1 `\` s2f s2.
127
s1, s2:{set 'I_n}
s2f (n:=n) (s1 :\: s2) =
s2f (n:=n) s1 `\` s2f (n:=n) s2
Proof.
215
apply/fsetP => j; rewrite !inE.
127218
j:nat_choiceType
(j \in s2f (n:=n) (s1 :\: s2)) =
(j \notin s2f (n:=n) s2) && (j \in s2f (n:=n) s1)
apply/imfsetP/andP => /= [[k]|[jDi /imfsetP[/= k kIs jEk]]].
12721821f
k:'I_n
k \in s1 :\: s2 ->
j = k -> j \notin s2f (n:=n) s2 /\ j \in s2f (n:=n) s1
12721821f
jDi:j \notin s2f (n:=n) s2
225
kIs:k \in s1
jEk:j = k
exists2 x : 'I_n, x \in s1 :\: s2 & j = x
  by rewrite !inE -!mem_s2f => /andP[kDi kIs] ->.
229
22d
by exists k => //; rewrite !inE kIs -mem_s2f -jEk jDi.
Qed.

Lemma s2fU n (s1 s2 : {set 'I_n}) : s2f (s1 :|: s2)  = s2f s1 `|` s2f s2.
217
s2f (n:=n) (s1 :|: s2) =
s2f (n:=n) s1 `|` s2f (n:=n) s2
Proof.
232
apply/fsetP => j; rewrite !inE.
21e
(j \in s2f (n:=n) (s1 :|: s2)) =
(j \in s2f (n:=n) s1) || (j \in s2f (n:=n) s2)
apply/imfsetP/orP => /= [[k]|[] /imfsetP[/= k]].
224
k \in s1 :|: s2 ->
j = k -> j \in s2f (n:=n) s1 \/ j \in s2f (n:=n) s2
224
k \in s1 ->
j = k -> exists2 x : 'I_n, x \in s1 :|: s2 & j = x
224
k \in s2 ->
j = k -> exists2 x : 'I_n, x \in s1 :|: s2 & j = x
-
23b by rewrite !inE -!mem_s2f => /orP[] kIs ->; [left|right].
224
240
241
-
245 by move => kIs1 ->; exists k; rewrite // inE kIs1.
224
242
by move => kIs2 ->; exists k; rewrite // inE kIs2 orbT.
Qed.

Lemma s2fI n (s1 s2 : {set 'I_n}) : s2f (s1 :&: s2)  = s2f s1 `&` s2f s2.
217
s2f (n:=n) (s1 :&: s2) =
s2f (n:=n) s1 `&` s2f (n:=n) s2
Proof.
24d
apply/fsetP => j; rewrite !inE.
21e
(j \in s2f (n:=n) (s1 :&: s2)) =
(j \in s2f (n:=n) s1) && (j \in s2f (n:=n) s2)
apply/imfsetP/andP => /= [[k]|[jDi /imfsetP[/= k kIs jEk]]].
224
k \in s1 :&: s2 ->
j = k -> j \in s2f (n:=n) s1 /\ j \in s2f (n:=n) s2
12721821f
jDi:j \in s2f (n:=n) s1
225
kIs:k \in s2
22c
exists2 x : 'I_n, x \in s1 :&: s2 & j = x
  by rewrite !inE -!mem_s2f => /andP[kDi kIs] ->.
25b
25e
by exists k => //; rewrite !inE kIs -mem_s2f -jEk jDi.
Qed.

Lemma s2f1 n (i : 'I_n) : s2f [set i] = [fset (nat_of_ord i)].
126
s2f (n:=n) [set i] = [fset i]
Proof.
263
apply/fsetP => j; rewrite !inE.
12711521f
(j \in s2f (n:=n) [set i]) = (j == i)
apply/imfsetP/eqP => /= [[k]|->]; first by rewrite inE => /eqP ->.
26a
exists2 x : 'I_n, x \in [set i] & i = x
by exists i; rewrite ?inE.
Qed.

Lemma s2f_pred n (s : {set 'I_n}) (P : pred nat) : 
   s2f [set i in s | P i] = [fset i in (s2f s) | P i].
1271ef
P:pred nat
s2f (n:=n) [set i in s | P i] =
[fset i in s2f (n:=n) s | P i]
Proof.
271
apply/fsetP=> i; rewrite !inE /=.
1271ef274156
(i \in s2f (n:=n) [set i in s | P i]) =
(i
   \in [eta mem_seq (T:=nat_choiceType) (s2f (n:=n) s)]) &&
P i
apply/imfsetP/andP => /= [[j]|].
1271ef274156
j:'I_n
j \in [set i in s | P i] ->
i = j ->
i \in [eta mem_seq (T:=nat_choiceType) (s2f (n:=n) s)] /\
P i
27a
i \in [eta mem_seq (T:=nat_choiceType) (s2f (n:=n) s)] /\
P i ->
exists2 x : 'I_n, x \in [set i in s | P i] & i = x
  rewrite !inE => /andP[jIs jP] ->; split => //.
1271ef2741562801f7
jP:P j
j \in [eta mem_seq (T:=nat_choiceType) (s2f (n:=n) s)]
282
  by apply/imfsetP; exists j.
27a
284
move=> [/imfsetP[/= j jIs ->] jP]; exists j => //.
288
j \in [set i in s | P i]
by rewrite inE jIs.
Qed.

Lemma s2fD1 n (s : {set 'I_n}) i : s2f (s :\ i) = s2f s `\ (nat_of_ord i).
1271ef
i:ordinal_finType n
s2f (n:=n) (s :\ i) = s2f (n:=n) s `\ i
Proof.
293 by rewrite s2fD s2f1. Qed.

Lemma card_s2f n (s : {set 'I_n}) : #|` s2f s| = #|s|.
1271ef
#|` s2f (n:=n) s| = #|s|
Proof.
29a
have [m sLm] := ubnP #|s|; elim: m => // m IH s sLm in s sLm *.
n, m:nat
IH:forall s : {set 'I_n},
#|s| < m -> #|` s2f (n:=n) s| = #|s|
1ef
sLm:#|s| < m.+1
29d
 case: (set_0Vmem s) => [->|[i iIs]]; first by rewrite s2f_set0 cards0.
2a32a41ef2a5296
iIs:i \in s
29d
rewrite (cardsD1 i) iIs /= -IH //; last first.
2a9
#|s :\ i| < m
2a9
#|` s2f (n:=n) s| = (1 + #|` s2f (n:=n) (s :\ i)|)%N
  by move: sLm; rewrite (cardsD1 i) iIs.
2a9
2b1
rewrite [LHS](cardfsD1 (nat_of_ord i)) (_ : _ \in _); last first.
2a9
i \in s2f (n:=n) s
2a9
(true + #|` s2f (n:=n) s `\ i|)%N =
(1 + #|` s2f (n:=n) (s :\ i)|)%N
  by rewrite mem_s2f.
2a9
2bb
by rewrite s2fD1.
Qed.

(* initial section of an ordinal *)
Definition isO n t := [set i | (i : 'I_n) < t].

Lemma isOE n t : t <= n -> s2f (isO n t) = sint 0 t.
n, t:nat
t <= n -> s2f (n:=n) (isO n t) = `[t]
Proof.
2c0
move=> tLn.
2c3
tLn:t <= n
s2f (n:=n) (isO n t) = `[t]
apply/fsetP => i; rewrite mem_sint.
2c32ca156
(i \in s2f (n:=n) (isO n t)) = (0 <= i < t)
apply/imfsetP/idP => /= [[j]|iLt]; first by rewrite inE => jLt ->.
2c32ca156
iLt:i < t
exists2 x : 'I_n, x \in isO n t & i = x
have iLn : i < n by apply: leq_trans tLn.
2c32ca1562d5212
2d6
by exists (Ordinal iLn); rewrite // inE.
Qed.

Lemma mem_isO n t i : (i \in isO n t) = (i < t).
2c3296
(i \in isO n t) = (i < t)
Proof.
2dc by rewrite inE. Qed.

Lemma isOE_ge n t : n <= t -> isO n t = setT.
2c2
n <= t -> isO n t = [set: ordinal_finType n]
Proof.
2e2
by move=> nLt; apply/setP => í; rewrite !inE (leq_trans _ nLt).
Qed.

Lemma isOE_le n t : t < n.+1 -> isO n.+1 t = [set inord i | i : 'I_t].
2c2
t < n.+1 -> isO n.+1 t = [set inord i | i : 'I_t]
Proof.
2e7
move=> tLn; apply/setP=> i; rewrite !inE.
2c3
tLn:t < n.+1
i:ordinal_finType n.+1
(i < t) = (i \in [set inord i | i : 'I_t])
apply/idP/imsetP => [iLt| [j _ ->]].
2c32ef2f02d5
exists2 x : ordinal_finType t,
  x \in 'I_t & i = inord x
2c32ef2f0
j:ordinal_finType t
inord j < t
  by exists (Ordinal iLt); rewrite //=; apply/val_eqP; rewrite /= inordK.
2f9
2fb
by rewrite inordK // (leq_trans _ tLn) // ltnS // ltnW.
Qed.

Lemma card_isO n t : #|isO n t| = minn n t.
2c2
#|isO n t| = minn n t
Proof.
300
apply/sym_equal.
2c2
minn n t = #|isO n t|
case: (leqP n t) => [nLt|tLn].
2c3
nLt:n <= t
n = #|isO n t|
2c3
tLn:t < n
t = #|isO n t|
  by rewrite isOE_ge //= cardsT card_ord.
310
312
case: n tLn => // n tLn.
t, n:nat
2ef
t = #|isO n.+1 t|
rewrite isOE_le // card_imset // => [|i j /val_eqP/eqP /=].
319
t = #|'I_t|
31a2ef
i, j:ordinal_finType t
inord i = inord j -> i = j
  by rewrite card_ord.
322
324
by rewrite !inordK ?(leq_trans _ tLn) ?ltnS 1?ltnW // => /eqP/val_eqP.
Qed.

Lemma s2fD_isO n (s : {set 'I_n}) t : s2f (s :\: isO n t)  = s2f s `\` sint 0 t.
1271ef
t:nat
s2f (n:=n) (s :\: isO n t) = s2f (n:=n) s `\` `[t]
Proof.
329
apply/fsetP => j; rewrite !inE.
1271ef32c21f
(j \in s2f (n:=n) (s :\: isO n t)) =
(j \notin `[t]) && (j \in s2f (n:=n) s)
apply/imfsetP/andP => /= [[k]|[jDi /imfsetP[/= k kIs jEk]]].
1271ef32c21f225
k \in s :\: isO n t ->
j = k -> j \notin `[t] /\ j \in s2f (n:=n) s
1271ef32c21f
jDi:j \notin `[t]
225
kIs:k \in s
22c
exists2 x : 'I_n, x \in s :\: isO n t & j = x
  by rewrite !inE -!mem_s2f mem_sint /= => /andP[kDi kIs] ->.
33b
33e
move: jDi; rewrite mem_sint /= -leqNgt => jDi.
1271ef32c21f22533d22c
jDi:t <= j
33e
by exists k; rewrite // !inE -leqNgt kIs -jEk jDi.
Qed.

(******************************************************************************)
(*                                                                            *)
(*              Specific theorems for shanoi                                  *)
(*                                                                            *)
(******************************************************************************)

Open Scope nat_scope.

Lemma codom_subC (A : finType) (B : finType) (f : {ffun A -> B}) 
          (p1 p2 : B) : 
  (codom f \subset [:: p1; p2]) = (codom f \subset [:: p2; p1]).
A, B:finType
f:{ffun A -> B}
p1, p2:B
(codom f \subset [:: p1; p2]) =
(codom f \subset [:: p2; p1])
Proof.
348
by apply/subsetP/subsetP; move => sB i /sB; rewrite !inE orbC.
Qed.

Lemma inord_eq0 n k : k = 0 -> inord k = ord0 :> 'I_n.+1.
n, k:nat
k = 0 -> inord k = ord0
Proof.
351 by move=> -> /=; apply/val_eqP; rewrite /= inordK. Qed.

Lemma mod3_0 a : (3 * a) %% 3 = 0.
1b7
(3 * a) %% 3 = 0
Proof.
358 by rewrite modnMr. Qed.

Lemma mod3_1 a : (3 * a).+1 %% 3 = 1.
1b7
(3 * a).+1 %% 3 = 1
Proof.
35d by rewrite mulnC -addn1 modnMDl. Qed.

Lemma mod3_2 a : (3 * a).+2 %% 3 = 2.
1b7
(3 * a).+2 %% 3 = 2
Proof.
362 by rewrite mulnC -addn2 modnMDl. Qed.

Definition mod3E := (mod3_0, mod3_1, mod3_2).

Lemma div3_0 a : (3 * a) %/ 3 = a.
1b7
(3 * a) %/ 3 = a
Proof.
367 by rewrite mulKn. Qed.

Lemma div3_1 a : (3 * a).+1 %/ 3 = a.
1b7
(3 * a).+1 %/ 3 = a
Proof.
36c by rewrite mulnC -addn1 divnMDl // divn_small // addn0. Qed.

Lemma div3_2 a : (3 * a).+2 %/ 3 = a.
1b7
(3 * a).+2 %/ 3 = a
Proof.
371 by rewrite mulnC -addn2 divnMDl // divn_small // addn0. Qed.

Definition div3E := (div3_0, div3_1, div3_2).

Lemma sum3E n (f : nat -> nat) : 
  \sum_(i < 3 * n) f i =
  \sum_(i < n) (f (3 * i) + f (3 * i).+1 + f (3 * i).+2).
127
f:nat -> nat
\sum_(i < 3 * n) f i =
\sum_(i < n) (f (3 * i) + f (3 * i).+1 + f (3 * i).+2)
Proof.
376
elim: n => [|n IH]; first by rewrite !big_ord0.
379127
IH:\sum_(i < 3 * n) f i =
\sum_(i < n)
   (f (3 * i) + f (3 * i).+1 + f (3 * i).+2)
\sum_(i < 3 * n.+1) f i =
\sum_(i < n.+1)
   (f (3 * i) + f (3 * i).+1 + f (3 * i).+2)
by rewrite mulnS !big_ord_recr /= IH !addnA.
Qed.

Lemma Ival_eq n (x y : 'I_n) : (x == y) = (val x == val y).
127
x, y:'I_n
(x == y) = (val x == val y)
Proof.
383 by apply/eqP/val_eqP. Qed.

Lemma oddS n : odd n.+1 = ~~ odd n.
1fd
odd n.+1 = ~~ odd n
Proof.
38a by []. Qed.

Lemma even_halfMl k m : 
  ~~ odd m -> (k * m)./2 = k * m./2.
k, m:nat
~~ odd m -> (k * m)./2 = k * m./2
Proof.
38f
move=> mE.
392
mE:~~ odd m
(k * m)./2 = k * m./2
have := odd_double_half m; rewrite (negPf mE) add0n => {1}<-.
398
(k * (m./2).*2)./2 = k * m./2
by rewrite -doubleMr doubleK.
Qed.

Lemma even_halfMr k m : 
  ~~ odd m -> (m * k)./2 = m./2 * k.
391
~~ odd m -> (m * k)./2 = m./2 * k
Proof.
3a0
move=> mE.
398
(m * k)./2 = m./2 * k
have := odd_double_half m; rewrite (negPf mE) add0n => {1}<-.
398
((m./2).*2 * k)./2 = m./2 * k
by rewrite -doubleMl doubleK.
Qed.

Lemma even_halfD m n : 
  ~~ odd m -> ~~ odd n -> (m + n)./2 = (m./2 + n./2).
11b
~~ odd m -> ~~ odd n -> (m + n)./2 = m./2 + n./2
Proof.
3ad
move=> mE nE.
10d399
nE:~~ odd n
(m + n)./2 = m./2 + n./2
have := odd_double_half m; rewrite (negPf mE) add0n => {1}<-.
3b4
((m./2).*2 + n)./2 = m./2 + n./2
have := odd_double_half n; rewrite (negPf nE) add0n => {1}<-.
3b4
((m./2).*2 + (n./2).*2)./2 = m./2 + n./2
by rewrite -doubleD doubleK.
Qed.

Lemma even_halfB m n : 
  ~~ odd m -> ~~ odd n -> (m - n)./2 = m./2 - n./2.
11b
~~ odd m -> ~~ odd n -> (m - n)./2 = m./2 - n./2
Proof.
3c0
move=> mE nE.
3b4
(m - n)./2 = m./2 - n./2
have := odd_double_half m; rewrite (negPf mE) add0n => {1}<-.
3b4
((m./2).*2 - n)./2 = m./2 - n./2
have := odd_double_half n; rewrite (negPf nE) add0n => {1}<-.
3b4
((m./2).*2 - (n./2).*2)./2 = m./2 - n./2
by rewrite -doubleB doubleK.
Qed.

Lemma leq_pred2 m n : m <= n -> m.-1 <= n.-1.
11b
m <= n -> m.-1 <= n.-1
Proof.
3d1 by case: m; case: n => //=. Qed.

Lemma subn_minr : left_distributive subn minn.
left_distributive subn minn
Proof.
3d6
move=> m n p; rewrite /minn; case: leqP => [nLm|mLn].
m, n, p:nat
nLm:n <= m
n - p = (if m - p < n - p then m - p else n - p)
3de
mLn:m < n
m - p = (if m - p < n - p then m - p else n - p)
  by rewrite ltnNge leq_sub2r.
3e3
3e5
have [nLp|pLn] := leqP n p; last by rewrite ltn_sub2r.
3de3e4
nLp:n <= p
3e5
apply/eqP; move: (nLp); rewrite -subn_eq0 => /eqP->.
3ec
m - p == (if m - p < 0 then m - p else 0)
by rewrite ltnNge //= subn_eq0 (leq_trans (ltnW mLn)).
Qed.

Lemma subn_maxr : left_distributive subn maxn.
left_distributive subn maxn
Proof.
3f3
move=> m n p; rewrite /maxn; case: leqP => [nLm|mLn].
3dd
m - p = (if m - p < n - p then n - p else m - p)
3e3
n - p = (if m - p < n - p then n - p else m - p)
  by rewrite ltnNge leq_sub2r.
3e3
3fd
have [nLp|pLn] := leqP n p; last by rewrite ltn_sub2r.
3ec
3fd
apply/eqP; move: (nLp); rewrite -subn_eq0 => /eqP->.
3ec
0 == (if m - p < 0 then 0 else m - p)
by rewrite ltnNge //= eq_sym subn_eq0 (leq_trans (ltnW mLn)).
Qed.

Lemma leq_minn2r m n p : m <= n -> minn m p <= minn n p.
3de
m <= n -> minn m p <= minn n p
Proof.
409
move=> mLn; rewrite /minn.
3de
mLn:m <= n
(if m < p then m else p) <= (if n < p then n else p)
case: leqP => pLm; case: leqP => //.
3de412
pLm:p <= m
n < p -> p <= n
3de412
pLm:m < p
p <= n -> m <= p
  by rewrite ltnNge (leq_trans pLm).
41c
41e
by move=> _; rewrite ltnW.
Qed.

Lemma leq_minn2l m n p : m <= n -> minn p m <= minn p n.
40b
m <= n -> minn p m <= minn p n
Proof.
423
move=> mLn; rewrite /minn.
411
(if p < m then p else m) <= (if p < n then p else n)
case: leqP => pLm; case: leqP => //.
3de412
pLm:p < m
n <= p -> p <= n
by move=> _; rewrite (leq_trans (ltnW pLm)).
Qed.

(******************************************************************************)
(* Definiion of discrete convex and concave version                           *)
(*  it contains just what is needed for shanoi4                               *)
(******************************************************************************)

Section Convex.

Definition increasing (f : nat -> nat) := forall n, f n <= f n.+1.

Definition decreasing (f : nat -> nat) := forall n, f n.+1 <= f n.

Lemma increasing_ext f1 f2 : f1 =1 f2 -> increasing f1 -> increasing f2.
f1, f2:nat -> nat
f1 =1 f2 -> increasing f1 -> increasing f2
Proof.
432 by move=> fE fI i; rewrite -!fE. Qed.

Lemma increasingE f m n : increasing f -> m <= n -> f m <= f n.
37910d
increasing f -> m <= n -> f m <= f n
Proof.
439
move=> fI mLn; rewrite -(subnK mLn).
37910d
fI:increasing f
412
f m <= f (n - m + m)
elim: (_ - _) => //= d fL.
37910d442412
d:nat
fL:f m <= f (d + m)
f m <= f (d.+1 + m)
by apply: leq_trans (fI (d + m)).
Qed.

Lemma decreasingE f m n : decreasing f -> m <= n -> f n <= f m.
43b
decreasing f -> m <= n -> f n <= f m
Proof.
44c
move=> fI mLn; rewrite -(subnK mLn).
37910d
fI:decreasing f
412
f (n - m + m) <= f m
elim: (_ - _) => //= d fL.
37910d454412448
fL:f (d + m) <= f m
f (d.+1 + m) <= f m
by apply: leq_trans (fI _) fL.
Qed.

Definition delta (f : nat -> nat) n := f n.+1 - f n.

Lemma delta_ext f1 f2 : f1 =1 f2 -> delta f1 =1 delta f2.
434
f1 =1 f2 -> delta f1 =1 delta f2
Proof.
45d by move=> fE i; rewrite /delta !fE. Qed.

Definition fnorm (f : nat -> nat) n := f n - f 0.

Lemma increasing_fnorm f : increasing f -> increasing (fnorm f).
379
increasing f -> increasing (fnorm f)
Proof.
462 by move=> fI n; rewrite leq_sub2r. Qed.

Lemma delta_fnorm f n : increasing f -> delta (fnorm f) n = delta f n.
379127
increasing f -> delta (fnorm f) n = delta f n
Proof.
468
by move=> fI; rewrite /delta /fnorm -subnDA addnC subnK // increasingE.
Qed.

Lemma sum_delta f n : 
increasing f -> fnorm f n = \sum_(i < n) delta (fnorm f) i.
46a
increasing f ->
fnorm f n = \sum_(i < n) delta (fnorm f) i
Proof.
46e
move=> iF.
379127
iF:increasing f
fnorm f n = \sum_(i < n) delta (fnorm f) i
elim: n => [|n IH]; first by rewrite [LHS]subnn big_ord0.
379476127
IH:fnorm f n = \sum_(i < n) delta (fnorm f) i
fnorm f n.+1 = \sum_(i < n.+1) delta (fnorm f) i
by rewrite big_ord_recr /= -IH addnC subnK // increasing_fnorm.
Qed.

(* we restrict this to increasing function because of the behavior -*)
Definition convex f :=
  increasing f /\ increasing (delta f).

(* we restrict this to increasing function because of the behavior -*)
Definition concave f :=
  increasing f /\ decreasing (delta f).

Lemma concaveE f : 
  increasing f -> (forall i, f i + f i.+2 <= (f i.+1).*2) -> concave f.
464
increasing f ->
(forall i : nat, f i + f i.+2 <= (f i.+1).*2) ->
concave f
Proof.
47f
move=> fI fH; split => // i.
379442
fH:forall i : nat, f i + f i.+2 <= (f i.+1).*2
i:nat
delta f i.+1 <= delta f i
rewrite /delta.
486
f i.+2 - f i.+1 <= f i.+1 - f i
rewrite -(leq_add2r (f i.+1 + f i)) addnA subnK // addnCA subnK //.
486
f i.+2 + f i <= f i.+1 + f i.+1
by rewrite addnn addnC.
Qed.

Lemma concaveEk f i k : 
  concave f -> k <= i -> f (i - k) + f (i + k) <= (f i).*2.
379
i, k:nat
concave f ->
k <= i -> f (i - k) + f (i + k) <= (f i).*2
Proof.
493
move=> [fI dfD].
379496442
dfD:decreasing (delta f)
k <= i -> f (i - k) + f (i + k) <= (f i).*2
elim: k => /= [kLi|k IH kLi]; first by rewrite subn0 addn0 addnn.
37948844249d
k:nat
IH:k <= i -> f (i - k) + f (i + k) <= (f i).*2
kLi:k < i
f (i - k.+1) + f (i + k.+1) <= (f i).*2
have H : i - k.+1 <= i + k.
4a2
i - k.+1 <= i + k
37948844249d4a34a44a5
H:i - k.+1 <= i + k
4a6
  by apply: leq_trans (leq_subr _ _) (leq_addr _ _).
4ad
4a6
have fk1Lfk : f (i - k.+1) <= f (i - k).
4ad
f (i - k.+1) <= f (i - k)
37948844249d4a34a44a54ae
fk1Lfk:f (i - k.+1) <= f (i - k)
4a6
  by apply/(increasingE fI)/leq_sub2l.
4b8
4a6
have := leq_add (decreasingE dfD H) (IH (ltnW kLi)).
4b8
delta f (i + k) + (f (i - k) + f (i + k)) <=
delta f (i - k.+1) + (f i).*2 ->
f (i - k.+1) + f (i + k.+1) <= (f i).*2
rewrite /delta [f (i - k) + _]addnC addnA subnK ?fU // addnC.
4b8
f (i - k) + f (i + k).+1 <=
f (i - k.+1).+1 - f (i - k.+1) + (f i).*2 ->
f (i - k.+1) + f (i + k.+1) <= (f i).*2
rewrite -subSn // subSS addnBAC // leq_subRL.
4b8
f (i - k.+1) + (f (i - k) + f (i + k).+1) <=
f (i - k) + (f i).*2 ->
f (i - k.+1) + f (i + k.+1) <= (f i).*2
4b8
f (i - k.+1) <= f (i - k) + (f i).*2
  by rewrite addnCA leq_add2l addnS.
4b8
4cb
by apply: leq_trans fk1Lfk (leq_addr _ _).
Qed.

Lemma concaveEk1 (f : nat -> nat) (i k1 k2 : nat) :
  concave f -> f (i + k1 + k2) + f i <= f (i + k2) + f (i + k1).
379
i, k1, k2:nat
concave f ->
f (i + k1 + k2) + f i <= f (i + k2) + f (i + k1)
Proof.
4d0
move=> fC; have [fI dfD] := fC.
3794d3
fC:concave f
44249d
f (i + k1 + k2) + f i <= f (i + k2) + f (i + k1)
elim: k2 k1 i => [k1 i|k2 IHH k1 i]; first by rewrite !addn0 addnC.
3794da44249d
k2:nat
IHH:forall k1 i : nat, f (i + k1 + k2) + f i <= f (i + k2) + f (i + k1)
k1, i:nat
f (i + k1 + k2.+1) + f i <= f (i + k2.+1) + f (i + k1)
rewrite !addnS -(subnK (fI _)) -[X in _ <= X + _](subnK (fI _)).
4df
f (i + k1 + k2).+1 - f (i + k1 + k2) + f (i + k1 + k2) +
f i <=
f (i + k2).+1 - f (i + k2) + f (i + k2) + f (i + k1)
rewrite -addnA -[X in _ <= X]addnA leq_add //.
4df
f (i + k1 + k2).+1 - f (i + k1 + k2) <=
f (i + k2).+1 - f (i + k2)
by apply: (decreasingE dfD); rewrite addnAC leq_addr.
Qed.

Lemma convexE f : 
  increasing f -> (forall i, (f i.+1).*2 <= f i + f i.+2) -> convex f.
464
increasing f ->
(forall i : nat, (f i.+1).*2 <= f i + f i.+2) ->
convex f
Proof.
4ed
move=> fI fH; split => // i.
379442
fH:forall i : nat, (f i.+1).*2 <= f i + f i.+2
488
delta f i <= delta f i.+1
rewrite /delta.
4f4
f i.+1 - f i <= f i.+2 - f i.+1
rewrite -(leq_add2r (f i.+1 + f i)) [_ + f i]addnC addnA subnK //.
4f4
f i.+1 + f i.+1 <= f i.+2 - f i.+1 + (f i + f i.+1)
by rewrite addnn [f i + _]addnC addnA subnK // addnC.
Qed.

Lemma convexEk f i k : 
  convex f -> k <= i -> (f i).*2 <= f (i - k) + f (i + k).
495
convex f ->
k <= i -> (f i).*2 <= f (i - k) + f (i + k)
Proof.
500
move=> [fI dfI].
379496442
dfI:increasing (delta f)
k <= i -> (f i).*2 <= f (i - k) + f (i + k)
elim: k => /= [kLi|k IH kLi]; first by rewrite subn0 addn0 addnn.
3794884425084a3
IH:k <= i -> (f i).*2 <= f (i - k) + f (i + k)
4a5
(f i).*2 <= f (i - k.+1) + f (i + k.+1)
have H : i - k.+1 <= i + k.
50d
4aa
3794884425084a350e4a54ae
50f
  by apply: leq_trans (leq_subr _ _) (leq_addr _ _).
515
50f
have fk1Lfk : f (i - k.+1) <= f (i - k).
515
4b5
3794884425084a350e4a54ae4b9
50f
  by apply/(increasingE fI)/leq_sub2l.
51e
50f
have := leq_add (increasingE dfI H) (IH (ltnW kLi)).
51e
delta f (i - k.+1) + (f i).*2 <=
delta f (i + k) + (f (i - k) + f (i + k)) ->
(f i).*2 <= f (i - k.+1) + f (i + k.+1)
rewrite /delta [f (i - k) + _]addnC addnA subnK ?fU // addnC.
51e
(f i).*2 + (f (i - k.+1).+1 - f (i - k.+1)) <=
f (i + k).+1 + f (i - k) ->
(f i).*2 <= f (i - k.+1) + f (i + k.+1)
by rewrite -subSn // subSS addnS addnBA // leq_subLR addnA leq_add2r.
Qed.

(* Ad-hoc bigmin operator *)

Fixpoint bigmin f n := 
 if n is n1.+1 then minn (f n) (bigmin f n1)
 else f 0.

Notation "\min_ ( i <= n ) F" := (bigmin (fun i => F) n)
 (at level 41, F at level 41, i, n at level 50,
  format "\min_ ( i  <=  n )  F").

Lemma bigmin_constD  f n k :
 \min_(i <= n) (f i + k) =  (\min_(i <= n) f i) + k.
379354
\min_(i <= n) (f i + k) = \min_(i <= n) f i + k
Proof.
52b by elim: n => //=  n ->; rewrite addn_minl. Qed.

Lemma bigmin_constB  f n k :
 \min_(i <= n) (f i - k) =  (\min_(i <= n) f i) - k.
52d
\min_(i <= n) (f i - k) = \min_(i <= n) f i - k
Proof.
531 by elim: n => //=  n ->; rewrite subn_minr. Qed.

Lemma eq_bigmin f n : {i0 : 'I_n.+1 | \min_(i <= n) f i = f i0}.
46a
{i0 : 'I_n.+1 | \min_(i <= n) f i = f i0}
Proof.
536
elim: n => /= [|n [i ->]]; first by exists ord0.
379127
i:'I_n.+1
{i0 : 'I_n.+2 | minn (f n.+1) (f i) = f i0}
rewrite /minn; case: leqP => H.
37912753e
H:f i <= f n.+1
{i0 : 'I_n.+2 | f i = f i0}
37912753e
H:f n.+1 < f i
{i0 : 'I_n.+2 | f n.+1 = f i0}
  by exists (inord i); rewrite inordK // (leq_trans (ltn_ord i)).
548
54a
by exists ord_max.
Qed.

Lemma bigmin_leqP f n m :
  reflect (forall i, i <= n -> m <= f i) 
          (m <= \min_(i <= n) f i).
3792a3
reflect (forall i : nat, i <= n -> m <= f i)
  (m <= \min_(i <= n) f i)
Proof.
54f
elim: n => /= [|n IH].
379
m:nat
reflect (forall i : nat, i <= 0 -> m <= f i)
  (m <= f 0)
37910d
IH:reflect (forall i : nat, i <= n -> m <= f i)
  (m <= \min_(i <= n) f i)
reflect (forall i : nat, i <= n.+1 -> m <= f i)
  (m <= minn (f n.+1) (\min_(i <= n) f i))
  by apply: (iffP idP) => [mLf0 [|i] //|->].
55c
55e
apply: (iffP idP) => [|H].
55c
m <= minn (f n.+1) (\min_(i <= n) f i) ->
forall i : nat, i <= n.+1 -> m <= f i
37910d55d
H:forall i : nat, i <= n.+1 -> m <= f i
m <= minn (f n.+1) (\min_(i <= n) f i)
  rewrite leq_min => /andP[mLf mLmin] i.
37910d55d
mLf:m <= f n.+1
mLmin:m <= \min_(i <= n) f i
488
i <= n.+1 -> m <= f i
566
  case: ltngtP => // [iLn _|-> _ //].
37910d55d56f570488
iLn:i < n.+1
m <= f i
566
  by rewrite ltnS in iLn; move: i iLn; apply/IH.
568
56a
rewrite leq_min H //=.
568
m <= \min_(i <= n) f i
by apply/IH => i iLn; rewrite H // (leq_trans iLn).
Qed.

Lemma bigmin_inf f n i0 m :
  i0 <= n -> f i0 <= m -> \min_(i <= n) f i <= m.
379
n, i0, m:nat
i0 <= n -> f i0 <= m -> \min_(i <= n) f i <= m
Proof.
580
move=> i0Ln fi0Lm; apply: leq_trans fi0Lm.
379583
i0Ln:i0 <= n
\min_(i <= n) f i <= f i0
elim: n i0Ln => /= [|n IH]; first by case: i0.
379
i0, m, n:nat
IH:i0 <= n -> \min_(i <= n) f i <= f i0
i0 <= n.+1 ->
minn (f n.+1) (\min_(i <= n) f i) <= f i0
by case: ltngtP => // [i0Ln _| -> _]; rewrite geq_min ?leqnn ?IH ?orbT.
Qed.

Lemma bigmin_fnorm f n : \min_(i <= n) fnorm f i = fnorm (bigmin f) n.
46a
\min_(i <= n) fnorm f i = fnorm (bigmin f) n 
Proof.
594 by elim: n => //= n ->; rewrite -subn_minr. Qed.

Lemma bigmin_ext f1 f2 n : 
  (forall i, i <= n -> f1 i = f2 i) -> \min_(i <= n) f1 i = \min_(i <= n) f2 i.
435127
(forall i : nat, i <= n -> f1 i = f2 i) ->
\min_(i <= n) f1 i = \min_(i <= n) f2 i
Proof.
599
elim: n => /= [->//|n IH H].
435127
IH:(forall i : nat, i <= n -> f1 i = f2 i) ->
\min_(i <= n) f1 i = \min_(i <= n) f2 i
H:forall i : nat, i <= n.+1 -> f1 i = f2 i
minn (f1 n.+1) (\min_(i <= n) f1 i) =
minn (f2 n.+1) (\min_(i <= n) f2 i)
by rewrite H // IH // => i iH; rewrite H // (leq_trans iH).
Qed.

Lemma bigminMr  f n k :
 \min_(i <= n) (f i * k) =  (\min_(i <= n) f i) * k.
52d
\min_(i <= n) f i * k = (\min_(i <= n) f i) * k
Proof.
5a6 by elim: n => //= n ->; rewrite  minnMl. Qed.

(* Convolution *)

Definition conv (f g : nat -> nat) n :=
  \min_(i <= n) (f i + g (n - i)).

Lemma conv0 f g : conv f g 0 = f 0 + g 0.
f, g:nat -> nat
conv f g 0 = f 0 + g 0
Proof.
5ab by []. Qed.

Lemma conv1 f g : 
  conv f g 1 = minn (f 1 + g 0) (f 0 + g 1).
5ad
conv f g 1 = minn (f 1 + g 0) (f 0 + g 1)
Proof.
5b2 by []. Qed.

Lemma conv_fnorm f g : 
  increasing f -> increasing g -> 
  conv (fnorm f) (fnorm g) =1 fnorm (conv f g).
5ad
increasing f ->
increasing g ->
conv (fnorm f) (fnorm g) =1 fnorm (conv f g)
Proof.
5b7
move=> fI gI i.
5ae442
gI:increasing g
488
conv (fnorm f) (fnorm g) i = fnorm (conv f g) i
rewrite /fnorm /conv /= -bigmin_constB subnn.
5be
\min_(i0 <= i) (f i0 - f 0 + (g (i - i0) - g 0)) =
\min_(i0 <= i) (f i0 + g (i - i0) - (f 0 + g 0))
apply: bigmin_ext => j.
5ae4425bf
i, j:nat
j <= i ->
f j - f 0 + (g (i - j) - g 0) =
f j + g (i - j) - (f 0 + g 0)
by rewrite addnBA ?increasingE // addnBAC ?increasingE // subnDA.
Qed.

Lemma conv_ext f1 g1 f2 g2 : f1 =1 f2 -> g1 =1 g2 -> conv f1 g1 =1 conv f2 g2.
f1, g1, f2, g2:nat -> nat
f1 =1 f2 -> g1 =1 g2 -> conv f1 g1 =1 conv f2 g2
Proof.
5cc by move=> fE gE i; apply: bigmin_ext => j; rewrite fE gE. Qed.

Lemma convC f g : conv f g =1 conv g f.
5ad
conv f g =1 conv g f
Proof.
5d3
move=> n; apply/eqP; rewrite /conv eqn_leq; apply/andP; split.
5ae127
\min_(i <= n) (f i + g (n - i)) <=
\min_(i <= n) (g i + f (n - i))
5da
\min_(i <= n) (g i + f (n - i)) <=
\min_(i <= n) (f i + g (n - i))
  apply/bigmin_leqP => i iLn.
5ae
n, i:nat
iLn:i <= n
\min_(i <= n) (f i + g (n - i)) <= g i + f (n - i)
5dc
  rewrite -{1}(subKn iLn) addnC.
5e2
\min_(i <= n) (f i + g (n - i)) <=
f (n - i) + g (n - (n - i))
5dc
  by apply: bigmin_inf (leq_subr _ _) (leqnn _).
5da
5de
apply/bigmin_leqP => i iLn.
5e2
\min_(i <= n) (g i + f (n - i)) <= f i + g (n - i)
rewrite -{1}(subKn iLn) addnC.
5e2
\min_(i <= n) (g i + f (n - i)) <=
g (n - i) + f (n - (n - i))
by apply: bigmin_inf (leq_subr _ _) (leqnn _).
Qed.

Lemma increasing_conv f g : 
  increasing f -> increasing g -> increasing (conv f g).
5ad
increasing f -> increasing g -> increasing (conv f g)
Proof.
5f6
move=> fI gI i.
5be
conv f g i <= conv f g i.+1
apply/bigmin_leqP => j.
5c8
j <= i.+1 -> conv f g i <= f j + g (i.+1 - j)
case: ltngtP => // [jLi | ->] _.
5ae4425bf5c9
jLi:j < i.+1
conv f g i <= f j + g (i.+1 - j)
5c8
conv f g i <= f i.+1 + g (i.+1 - i.+1)
  by apply: bigmin_inf (_ : j <= i) _; rewrite // leq_add2l subSn.
5c8
60a
rewrite subnn.
5c8
conv f g i <= f i.+1 + g 0
by apply: bigmin_inf (leqnn i) _; rewrite subnn leq_add2r.
Qed.

(* merging increasing functions *)

Fixpoint fmerge_aux (f g : nat -> nat) i j n := 
 if n is n1.+1 then
   if f i < g j then fmerge_aux f g i.+1 j n1 
   else fmerge_aux f g i j.+1 n1
 else minn (f i) (g j).

Definition fmerge f g n := fmerge_aux f g 0 0 n.

Lemma fmerge_aux_ext f1 f2 g1 g2 i j : f1 =1 f2 -> g1 =1 g2 -> 
  fmerge_aux f1 g1 i j =1 fmerge_aux f2 g2 i j.
f1, f2, g1, g2:nat -> nat
5c9
f1 =1 f2 ->
g1 =1 g2 ->
fmerge_aux f1 g1 i j =1 fmerge_aux f2 g2 i j
Proof.
613
move=> fE gE n; elim: n i j => /= [i1 j1|n IH i j]; first by rewrite fE gE.
616
fE:f1 =1 f2
gE:g1 =1 g2
127
IH:forall i j : nat,
fmerge_aux f1 g1 i j n = fmerge_aux f2 g2 i j n
5c9
(if f1 i < g1 j
 then fmerge_aux f1 g1 i.+1 j n
 else fmerge_aux f1 g1 i j.+1 n) =
(if f2 i < g2 j
 then fmerge_aux f2 g2 i.+1 j n
 else fmerge_aux f2 g2 i j.+1 n)
by rewrite !(fE, gE, IH).
Qed.

Lemma fmerge_ext f1 f2 g1 g2 : f1 =1 f2 -> g1 =1 g2 -> 
  fmerge f1 g1 =1 fmerge f2 g2.
616
f1 =1 f2 -> g1 =1 g2 -> fmerge f1 g1 =1 fmerge f2 g2
Proof.
622 by move=> fE gE n; apply: fmerge_aux_ext. Qed.

Lemma fmerge_aux_correct f g i j n :
  increasing f -> increasing g -> 
  (forall k, k <= n ->  
     minn (f (i + k)) (g (j + (n - k))) <=  
     fmerge_aux f g i j n).
5ae
i, j, n:nat
increasing f ->
increasing g ->
forall k : nat,
k <= n ->
minn (f (i + k)) (g (j + (n - k))) <=
fmerge_aux f g i j n
Proof.
628
move=> fI gI.
5ae62b4425bf
forall k : nat,
k <= n ->
minn (f (i + k)) (g (j + (n - k))) <=
fmerge_aux f g i j n
elim: n i j => /= [i j [|] // _|n IH i j k kLn].
5c8
minn (f (i + 0)) (g (j + (0 - 0))) <= minn (f i) (g j)
5ae4425bf127
IH:forall i j k : nat,
k <= n ->
minn (f (i + k)) (g (j + (n - k))) <=
fmerge_aux f g i j n
i, j, k:nat
kLn:k <= n.+1
minn (f (i + k)) (g (j + (n.+1 - k))) <=
(if f i < g j
 then fmerge_aux f g i.+1 j n
 else fmerge_aux f g i j.+1 n)
  by rewrite !addn0.
639
63d
case: leqP => [gLf|fLg].
5ae4425bf12763a63b63c
gLf:g j <= f i
minn (f (i + k)) (g (j + (n.+1 - k))) <=
fmerge_aux f g i j.+1 n
5ae4425bf12763a63b63c
fLg:f i < g j
minn (f (i + k)) (g (j + (n.+1 - k))) <=
fmerge_aux f g i.+1 j n
  move: kLn; rewrite leq_eqVlt => /orP[/eqP->|kLn].
5ae4425bf12763a63b645
minn (f (i + n.+1)) (g (j + (n.+1 - n.+1))) <=
fmerge_aux f g i j.+1 n
5ae4425bf12763a63b645
kLn:k < n.+1
646
648
    rewrite subnn addn0 (minn_idPr _); last first.
64f
g j <= f (i + n.+1)
64f
g j <= fmerge_aux f g i j.+1 n
652648
      by rewrite (leq_trans gLf) // increasingE // leq_addr.
64f
65b
651
    apply: leq_trans (IH _ _ _ (leqnn _)).
64f
g j <= minn (f (i + n)) (g (j.+1 + (n - n)))
651
    rewrite subnn addn0 leq_min increasingE // andbT (leq_trans gLf) //.
64f
f i <= f (i + n)
651
    by rewrite increasingE // leq_addr.
653
646
647
  by rewrite subSn // -addSnnS IH.
649
64b
case: k kLn => [_ | k kLn].
5ae4425bf12763a5c964a
minn (f (i + 0)) (g (j + (n.+1 - 0))) <=
fmerge_aux f g i.+1 j n
5ae4425bf12763a5c964a4a3654
minn (f (i + k.+1)) (g (j + (n.+1 - k.+1))) <=
fmerge_aux f g i.+1 j n
  rewrite addn0 subn0 (minn_idPl _); last first.
670
f i <= g (j + n.+1)
670
f i <= fmerge_aux f g i.+1 j n
673
    by rewrite (leq_trans (ltnW fLg)) // increasingE // leq_addr.
670
67c
672
  apply: leq_trans (IH i.+1 j 0 isT).
670
f i <= minn (f (i.+1 + 0)) (g (j + (n - 0)))
672
  rewrite addn0 leq_min increasingE //= (leq_trans (ltnW fLg)) //.
670
g j <= g (j + (n - 0))
672
  by rewrite increasingE // leq_addr.
674
675
by rewrite subSS -addSnnS IH.
Qed.

Lemma fmerge_aux_exist f g i j n :
  exists2 k, k <= n & fmerge_aux f g i j n = minn (f (i + k)) (g (j + (n - k))).
62a
exists2 k : nat,
  k <= n &
  fmerge_aux f g i j n =
  minn (f (i + k)) (g (j + (n - k)))
Proof.
68c
elim: n i j => /= [i j | n IH i j]; first by exists 0; rewrite //= !addn0.
5ae127
IH:forall i j : nat,
exists2 k : nat,
  k <= n &
  fmerge_aux f g i j n =
  minn (f (i + k)) (g (j + (n - k)))
5c9
exists2 k : nat,
  k <= n.+1 &
  (if f i < g j
   then fmerge_aux f g i.+1 j n
   else fmerge_aux f g i j.+1 n) =
  minn (f (i + k)) (g (j + (n.+1 - k)))
case: (leqP (g j) (f i)) => [gLf|fLg]; last first.
5ae1276945c964a
exists2 k : nat,
  k <= n.+1 &
  fmerge_aux f g i.+1 j n =
  minn (f (i + k)) (g (j + (n.+1 - k)))
5ae1276945c9645
exists2 k : nat,
  k <= n.+1 &
  fmerge_aux f g i j.+1 n =
  minn (f (i + k)) (g (j + (n.+1 - k)))
  by case: (IH i.+1 j) => k kLn ->; exists k.+1; rewrite // addnS subSS.
69d
69e
case: (IH i j.+1) => [] [|k] kLn ->.
5ae1276945c9645
kLn:0 <= n
exists2 k : nat,
  k <= n.+1 &
  minn (f (i + 0)) (g (j.+1 + (n - 0))) =
  minn (f (i + k)) (g (j + (n.+1 - k)))
5ae1276945c96454a3
kLn:k < n
ex2 (fun k : nat => k <= n.+1)
  (fun k0 : nat =>
   minn (f (i + k.+1)) (g (j.+1 + (n - k.+1))) =
   minn (f (i + k0)) (g (j + (n.+1 - k0))))
  by exists 0; rewrite // addn0 !subn0 addnS.
6aa
6ac
by exists k.+1; rewrite ?(leq_trans kLn) // addSnnS -subSn.
Qed.

Lemma fmergeE (f g : nat -> nat) n : 
 increasing f -> increasing g ->
 fmerge f g n = \max_(i < n.+1) minn (f i) (g (n - i)).
5da
increasing f ->
increasing g ->
fmerge f g n = \max_(i < n.+1) minn (f i) (g (n - i))
Proof.
6b1
move=> fI gI.
5ae1274425bf
fmerge f g n = \max_(i < n.+1) minn (f i) (g (n - i))
apply/eqP; rewrite /fmerge eqn_leq; apply/andP; split.
6b8
fmerge_aux f g 0 0 n <=
\max_(i < n.+1) minn (f i) (g (n - i))
6b8
\max_(i < n.+1) minn (f i) (g (n - i)) <=
fmerge_aux f g 0 0 n
  case: (@fmerge_aux_exist f g 0 0 n) => // i1 i1Ln ->.
5ae1274425bf
i1:nat
i1Ln:i1 <= n
minn (f (0 + i1)) (g (0 + (n - i1))) <=
\max_(i < n.+1) minn (f i) (g (n - i))
6be
  by apply: (@leq_bigmax_cond _ _ _ (Ordinal (i1Ln : i1 < n.+1))).
6b8
6c0
apply/bigmax_leqP => /= i _.
5ae1274425bf53e
minn (f i) (g (n - i)) <= fmerge_aux f g 0 0 n
by apply: fmerge_aux_correct; rewrite -1?ltnS.
Qed.

Lemma increasing_fmerge f g : 
  increasing f -> increasing g -> increasing (fmerge f g).
5ad
increasing f ->
increasing g -> increasing (fmerge f g)
Proof.
6d1
move=> fI gI n; rewrite !fmergeE //.
5ae4425bf127
\max_(i < n.+1) minn (f i) (g (n - i)) <=
\max_(i < n.+2) minn (f i) (g (n.+1 - i))
apply/bigmax_leqP => /= i _.
5ae4425bf12753e
minn (f i) (g (n - i)) <=
\max_(i < n.+2) minn (f i) (g (n.+1 - i))
apply: leq_trans (leq_bigmax_cond _ (isT : xpredT (inord i : 'I_n.+2))).
6dd
minn (f i) (g (n - i)) <=
minn (f (inord i)) (g (n.+1 - inord i))
rewrite inordK ?(leq_trans (ltn_ord _)) //.
6dd
minn (f i) (g (n - i)) <= minn (f i) (g (n.+1 - i))
rewrite leq_min geq_minl /= (leq_trans (geq_minr _ _)) //.
6dd
g (n - i) <= g (n.+1 - i)
apply: increasingE gI _.
5ae44212753e
n - i <= n.+1 - i
by rewrite leq_sub2r.
Qed.

Lemma fmerge0 f g : fmerge f g 0 = minn (f 0) (g 0).
5ad
fmerge f g 0 = minn (f 0) (g 0)
Proof.
6f1 by []. Qed.

Fixpoint sum_fmerge_aux (f g : nat -> nat) i j n := 
 if n is n1.+1 then
   if f i < g j then f i + sum_fmerge_aux f g i.+1 j n1 
   else g j + sum_fmerge_aux f g i j.+1 n1
 else minn (f i) (g j).

Definition sum_fmerge f g n := sum_fmerge_aux f g 0 0 n.

Lemma sum_fmerge_aux_correct f g n i j : 
  sum_fmerge_aux f g i j n = \sum_(k < n.+1) fmerge_aux f g i j k.
5ae
n, i, j:nat
sum_fmerge_aux f g i j n =
\sum_(k < n.+1) fmerge_aux f g i j k
Proof.
6f6
elim: n i j => //= [i j|n IH i j]; first by rewrite big_ord_recr big_ord0.
5ae127
IH:forall i j : nat,
sum_fmerge_aux f g i j n =
\sum_(k < n.+1) fmerge_aux f g i j k
5c9
(if f i < g j
 then f i + sum_fmerge_aux f g i.+1 j n
 else g j + sum_fmerge_aux f g i j.+1 n) =
\sum_(k < n.+2) fmerge_aux f g i j k
by rewrite big_ord_recl /= /minn; case: leqP; rewrite IH.
Qed.

Lemma sum_fmerge_correct f g n : 
  sum_fmerge f g n = \sum_(k < n.+1) fmerge f g k.
5da
sum_fmerge f g n = \sum_(k < n.+1) fmerge f g k
Proof.
703 by apply: sum_fmerge_aux_correct. Qed.

Lemma sum_fmerge_aux_conv_correct f g i j n :
  increasing f -> increasing g -> 
  (forall k, k <= n.+1 -> 
    sum_fmerge_aux f g i j n <= 
    \sum_(l < k) f (i + l) + \sum_(l < n.+1 - k) g (j + l)).
62a
increasing f ->
increasing g ->
forall k : nat,
k <= n.+1 ->
sum_fmerge_aux f g i j n <=
\sum_(l < k) f (i + l) + \sum_(l < n.+1 - k) g (j + l)
Proof.
708
move=> fI gI.
631
forall k : nat,
k <= n.+1 ->
sum_fmerge_aux f g i j n <=
\sum_(l < k) f (i + l) + \sum_(l < n.+1 - k) g (j + l)
elim: n i j => /= [i j [_|[_|]]//|n IH i j k kLn].
5c8
minn (f i) (g j) <=
\sum_(l < 0) f (i + l) + \sum_(l < 1 - 0) g (j + l)
5c8
minn (f i) (g j) <=
\sum_(l < 1) f (i + l) + \sum_(l < 1 - 1) g (j + l)
5ae4425bf127
IH:forall i j k : nat,
k <= n.+1 ->
sum_fmerge_aux f g i j n <=
\sum_(l < k) f (i + l) +
\sum_(l < n.+1 - k) g (j + l)
63b
kLn:k <= n.+2
(if f i < g j
 then f i + sum_fmerge_aux f g i.+1 j n
 else g j + sum_fmerge_aux f g i j.+1 n) <=
\sum_(l < k) f (i + l) + \sum_(l < n.+2 - k) g (j + l)
-
711 by rewrite big_ord_recr !big_ord0 /= !addn0 !add0n geq_minr.
5c8
716
717
-
71e by rewrite big_ord_recr !big_ord0 /= !addn0 !add0n geq_minl.
718
71b
case: leqP => [gLf|fLg].
5ae4425bf12771963b71a645
g j + sum_fmerge_aux f g i j.+1 n <=
\sum_(l < k) f (i + l) + \sum_(l < n.+2 - k) g (j + l)
5ae4425bf12771963b71a64a
f i + sum_fmerge_aux f g i.+1 j n <=
\sum_(l < k) f (i + l) + \sum_(l < n.+2 - k) g (j + l)
  move: kLn; case: ltngtP => // [kLn _ |-> _]; last first.
5ae4425bf12771963b645
g j + sum_fmerge_aux f g i j.+1 n <=
\sum_(l < n.+2) f (i + l) +
\sum_(l < n.+2 - n.+2) g (j + l)
5ae4425bf12771963b645
kLn:k < n.+2
729
72b
    rewrite subnn big_ord0 addn0 big_ord_recl addn0 /=.
731
g j + sum_fmerge_aux f g i j.+1 n <=
f i + \sum_(i0 < n.+1) f (i + bump 0 i0)
733
    apply: leq_add => //.
731
sum_fmerge_aux f g i j.+1 n <=
\sum_(i0 < n.+1) f (i + bump 0 i0)
733
    rewrite /bump /=.
731
sum_fmerge_aux f g i j.+1 n <=
\sum_(i0 < n.+1) f (i + (1 + i0))
733
    apply: leq_trans (IH _ _ _ (leqnn _)) _.
731
\sum_(l < n.+1) f (i + l) +
\sum_(l < n.+1 - n.+1) g (j.+1 + l) <=
\sum_(i0 < n.+1) f (i + (1 + i0))
733
    rewrite subnn big_ord0 addn0 leq_sum // => l _.
5ae4425bf12771963b645
l:'I_n.+1
f (i + l) <= f (i + (1 + l))
733
    by apply: increasingE; rewrite // addnCA leq_addl.
735
729
72a
  rewrite subSn // big_ord_recl addn0 addnCA leq_add2l.
735
sum_fmerge_aux f g i j.+1 n <=
\sum_(l < k) f (i + l) +
\sum_(i < n.+1 - k) g (j + lift ord0 i)
72a
  apply: leq_trans (IH _ _ _ (kLn : k <= n.+1)) _.
735
\sum_(l < k) f (i + l) +
\sum_(l < n.+1 - k) g (j.+1 + l) <=
\sum_(l < k) f (i + l) +
\sum_(i < n.+1 - k) g (j + lift ord0 i)
72a
  rewrite leq_add2l leq_sum // => l _.
5ae4425bf12771963b645736
l:'I_(n.+1 - k)
g (j.+1 + l) <= g (j + lift ord0 l)
72a
  by rewrite increasingE //= /bump addnCA add1n.
72c
72d
move: kLn; case: ltngtP => // [kLn _ |-> _]; last first.
5ae4425bf12771963b64a
f i + sum_fmerge_aux f g i.+1 j n <=
\sum_(l < n.+2) f (i + l) +
\sum_(l < n.+2 - n.+2) g (j + l)
5ae4425bf12771963b64a736
72d
  rewrite subnn big_ord0 addn0 big_ord_recl addn0 /= leq_add2l /bump /=.
764
sum_fmerge_aux f g i.+1 j n <=
\sum_(i0 < n.+1) f (i + (1 + i0))
766
  apply: leq_trans (IH _ _ _ (leqnn _)) _.
764
\sum_(l < n.+1) f (i.+1 + l) +
\sum_(l < n.+1 - n.+1) g (j + l) <=
\sum_(i0 < n.+1) f (i + (1 + i0))
766
  rewrite subnn big_ord0 addn0 leq_sum // => l _.
5ae4425bf12771963b64a74b
f (i.+1 + l) <= f (i + (1 + l))
766
  by rewrite increasingE // addnCA add1n.
768
72d
case: k kLn => [_|k kLn]; last first.
5ae4425bf1277195c964a4a3
kLn:k.+1 < n.+2
f i + sum_fmerge_aux f g i.+1 j n <=
\sum_(l < k.+1) f (i + l) +
\sum_(l < n.+2 - k.+1) g (j + l)
5ae4425bf1277195c964a
f i + sum_fmerge_aux f g i.+1 j n <=
\sum_(l < 0) f (i + l) + \sum_(l < n.+2 - 0) g (j + l)
  rewrite subSS.
77c
f i + sum_fmerge_aux f g i.+1 j n <=
\sum_(l < k.+1) f (i + l) +
\sum_(l < n.+1 - k) g (j + l)
77f
  apply: leq_trans (leq_add  (leqnn _) (IH i.+1 j k _)) _ .
77c
k <= n.+1
77c
f i +
(\sum_(l < k) f (i.+1 + l) +
 \sum_(l < n.+1 - k) g (j + l)) <=
\sum_(l < k.+1) f (i + l) +
\sum_(l < n.+1 - k) g (j + l)
780
    by rewrite -ltnS ltnW.
77c
78d
77f
  rewrite addnA leq_add2r big_ord_recl addn0 leq_add2l leq_sum // => l _.
5ae4425bf1277195c964a4a377d
l:'I_k
f (i.+1 + l) <= f (i + lift ord0 l)
77f
  by rewrite addnCA.
781
782
rewrite big_ord0 add0n subn0.
781
f i + sum_fmerge_aux f g i.+1 j n <=
\sum_(l < n.+2) g (j + l)
apply: leq_trans (leq_add  (leqnn _) (IH i.+1 j 0 isT)) _ .
781
f i +
(\sum_(l < 0) f (i.+1 + l) +
 \sum_(l < n.+1 - 0) g (j + l)) <=
\sum_(l < n.+2) g (j + l)
rewrite big_ord0 add0n subn0 [X in _ <= X]big_ord_recr addnC leq_add //.
781
f i <= g (j + ord_max)
apply: leq_trans (ltnW fLg) _.
781
g j <= g (j + ord_max)
by rewrite increasingE // leq_addr.
Qed.

Lemma leq_sum_fmerge_conv f g k n :
  increasing f -> increasing g -> k <= n -> 
  \sum_(i < n) fmerge f g i <= \sum_(i < k) f i + \sum_(i < n - k) g i.
5ae
k, n:nat
increasing f ->
increasing g ->
k <= n ->
\sum_(i < n) fmerge f g i <=
\sum_(i < k) f i + \sum_(i < n - k) g i
Proof.
7ab
move=> fI gI; case: n => [|n kLn].
5ae4a34425bf
k <= 0 ->
\sum_(i < 0) fmerge f g i <=
\sum_(i < k) f i + \sum_(i < 0 - k) g i
5ae4a34425bf12763c
\sum_(i < n.+1) fmerge f g i <=
\sum_(i < k) f i + \sum_(i < n.+1 - k) g i
  by case: k; rewrite // !big_ord0.
7b8
7b9
rewrite -sum_fmerge_correct.
7b8
sum_fmerge f g n <=
\sum_(i < k) f i + \sum_(i < n.+1 - k) g i
exact: (sum_fmerge_aux_conv_correct 0 0 fI gI kLn).
Qed.

Lemma sum_fmerge_aux_exist f g i j n :
  exists2 k, k <= n.+1 & 
  sum_fmerge_aux f g i j n =     
  \sum_(l < k) f (i + l) + \sum_(l < n.+1 - k) g (j + l).
62a
exists2 k : nat,
  k <= n.+1 &
  sum_fmerge_aux f g i j n =
  \sum_(l < k) f (i + l) +
  \sum_(l < n.+1 - k) g (j + l)
Proof.
7c2
elim: n i j => /= [i j | n IH i j].
5ae5c9
exists2 k : nat,
  k <= 1 &
  minn (f i) (g j) =
  \sum_(l < k) f (i + l) + \sum_(l < 1 - k) g (j + l)
5ae127
IH:forall i j : nat,
exists2 k : nat,
  k <= n.+1 &
  sum_fmerge_aux f g i j n =
  \sum_(l < k) f (i + l) +
  \sum_(l < n.+1 - k) g (j + l)
5c9
exists2 k : nat,
  k <= n.+2 &
  (if f i < g j
   then f i + sum_fmerge_aux f g i.+1 j n
   else g j + sum_fmerge_aux f g i j.+1 n) =
  \sum_(l < k) f (i + l) +
  \sum_(l < n.+2 - k) g (j + l)
  rewrite /minn; case: leqP => [gLf|fLg].
5ae5c9645
exists2 k : nat,
  k <= 1 &
  g j =
  \sum_(l < k) f (i + l) + \sum_(l < 1 - k) g (j + l)
5ae5c964a
exists2 k : nat,
  k <= 1 &
  f i =
  \sum_(l < k) f (i + l) + \sum_(l < 1 - k) g (j + l)
7cc
    by exists 0; rewrite // big_ord_recl !big_ord0 !(add0n, addn0).
7d7
7d8
7cb
  by exists 1; rewrite // subnn big_ord_recl !big_ord0 !(add0n, addn0).
7cd
7cf
case: (leqP (g j) (f i)) => [gLf|fLg].
5ae1277ce5c9645
exists2 k : nat,
  k <= n.+2 &
  g j + sum_fmerge_aux f g i j.+1 n =
  \sum_(l < k) f (i + l) +
  \sum_(l < n.+2 - k) g (j + l)
5ae1277ce5c964a
exists2 k : nat,
  k <= n.+2 &
  f i + sum_fmerge_aux f g i.+1 j n =
  \sum_(l < k) f (i + l) +
  \sum_(l < n.+2 - k) g (j + l)
  case: (IH i j.+1) => k kLn ->.
5ae1277ce5c96454a363c
ex2 (fun k : nat => k <= n.+2)
  (fun k0 : nat =>
   g j +
   (\sum_(l < k) f (i + l) +
    \sum_(l < n.+1 - k) g (j.+1 + l)) =
   \sum_(l < k0) f (i + l) +
   \sum_(l < n.+2 - k0) g (j + l))
7e4
  exists k; first by apply: leq_trans kLn _.
7eb
g j +
(\sum_(l < k) f (i + l) +
 \sum_(l < n.+1 - k) g (j.+1 + l)) =
\sum_(l < k) f (i + l) + \sum_(l < n.+2 - k) g (j + l)
7e4
  rewrite (subSn kLn) big_ord_recl addn0 addnCA.
7eb
\sum_(l < k) f (i + l) +
(g j + \sum_(l < n.+1 - k) g (j.+1 + l)) =
\sum_(l < k) f (i + l) +
(g j + \sum_(i < n.+1 - k) g (j + lift ord0 i))
7e4
  by congr (_ + (_ + _)); apply: eq_bigr => l _; rewrite addnCA.
7e6
7e7
case: (IH i.+1 j) => k kLn ->; exists k.+1; first by apply: leq_trans kLn _.
5ae1277ce5c964a4a363c
f i +
(\sum_(l < k) f (i.+1 + l) +
 \sum_(l < n.+1 - k) g (j + l)) =
\sum_(l < k.+1) f (i + l) +
\sum_(l < n.+2 - k.+1) g (j + l)
rewrite big_ord_recl addn0 subSS -addnA.
7fb
f i +
(\sum_(l < k) f (i.+1 + l) +
 \sum_(l < n.+1 - k) g (j + l)) =
f i +
(\sum_(i0 < k) f (i + lift ord0 i0) +
 \sum_(l < n.+1 - k) g (j + l))
by congr (_ + (_ + _)); apply: eq_bigr => l _; rewrite addnCA.
Qed.

Lemma sum_fmerge_exist f g n :
  exists2 k, k <= n & 
  \sum_(i < n) fmerge f g i = \sum_(i < k) f i + \sum_(i < n - k) g i.
5da
exists2 k : nat,
  k <= n &
  \sum_(i < n) fmerge f g i =
  \sum_(i < k) f i + \sum_(i < n - k) g i
Proof.
802
case: n => [|n]; first by exists 0; rewrite // !big_ord0.
5da
exists2 k : nat,
  k <= n.+1 &
  \sum_(i < n.+1) fmerge f g i =
  \sum_(i < k) f i + \sum_(i < n.+1 - k) g i
case: (sum_fmerge_aux_exist f g 0 0 n) => k kLn sE.
5ae35463c
sE:sum_fmerge_aux f g 0 0 n =
\sum_(l < k) f (0 + l) +
\sum_(l < n.+1 - k) g (0 + l)
809
by exists k; rewrite // -sum_fmerge_correct [LHS]sE.
Qed.

Lemma sum_fmerge_conv f g n : 
  increasing f -> increasing g ->
  \sum_(i < n) (fmerge f g) i  =
     conv (fun n => \sum_(i < n) f i) (fun n => \sum_(i < n) g i) n.
5da
increasing f ->
increasing g ->
\sum_(i < n) fmerge f g i =
conv (fun n : nat => \sum_(i < n) f i)
  (fun n : nat => \sum_(i < n) g i) n
Proof.
810
move=> fI gI.
6b8
\sum_(i < n) fmerge f g i =
conv (fun n : nat => \sum_(i < n) f i)
  (fun n : nat => \sum_(i < n) g i) n
apply/eqP; rewrite eqn_leq; apply/andP; split; last first.
6b8
conv (fun n : nat => \sum_(i < n) f i)
  (fun n : nat => \sum_(i < n) g i) n <=
\sum_(i < n) fmerge f g i
6b8
\sum_(i < n) fmerge f g i <=
conv (fun n : nat => \sum_(i < n) f i)
  (fun n : nat => \sum_(i < n) g i) n
  case: (sum_fmerge_exist f g n) => k kLn ->.
5ae1274425bf4a3
kLn:k <= n
conv (fun n : nat => \sum_(i < n) f i)
  (fun n : nat => \sum_(i < n) g i) n <=
\sum_(i < k) f i + \sum_(i < n - k) g i
81c
  by apply: (bigmin_inf _ (leqnn _)).
6b8
81e
apply/bigmin_leqP => k kLn.
822
\sum_(i < n) fmerge f g i <=
\sum_(i < k) f i + \sum_(i < n - k) g i
by apply: leq_sum_fmerge_conv.
Qed.

(* This is 3.2 *)
Lemma delta_conv f g : 
  convex f -> convex g -> delta (conv f g) =1 fmerge (delta f) (delta g).
5ad
convex f ->
convex g ->
delta (conv f g) =1 fmerge (delta f) (delta g)
Proof.
82d
move=> [fI dfI] [gI dgI] n.
5ae4425085bf
dgI:increasing (delta g)
127
delta (conv f g) n = fmerge (delta f) (delta g) n
rewrite -delta_fnorm; last by apply: increasing_conv.
834
delta (fnorm (conv f g)) n =
fmerge (delta f) (delta g) n
rewrite -(delta_ext (conv_fnorm _ _)) //.
834
delta (conv (fnorm f) (fnorm g)) n =
fmerge (delta f) (delta g) n
have/delta_ext-> : conv (fnorm f) (fnorm g) =1
         conv (fun n => \sum_(i < n) (delta (fnorm f)) i) 
              (fun n => \sum_(i < n) (delta (fnorm g)) i).
834
conv (fnorm f) (fnorm g) =1
conv (fun n : nat => \sum_(i < n) delta (fnorm f) i)
  (fun n : nat => \sum_(i < n) delta (fnorm g) i)
834
delta
  (conv
     (fun n : nat => \sum_(i < n) delta (fnorm f) i)
     (fun n : nat => \sum_(i < n) delta (fnorm g) i))
  n = fmerge (delta f) (delta g) n
  by apply: conv_ext => i; apply: sum_delta.
834
845
have/delta_ext-> :
  (conv (fun n : nat => \sum_(i < n) delta (fnorm f) i)
        (fun n : nat => \sum_(i < n) delta (fnorm g) i)) =1
  (fun n => \sum_(i < n) (fmerge (delta (fnorm f)) (delta (fnorm g))) i).
834
conv (fun n : nat => \sum_(i < n) delta (fnorm f) i)
  (fun n : nat => \sum_(i < n) delta (fnorm g) i) =1
(fun n : nat =>
 \sum_(i < n)
    fmerge (delta (fnorm f)) (delta (fnorm g)) i)
834
delta
  (fun n : nat =>
   \sum_(i < n)
      fmerge (delta (fnorm f)) (delta (fnorm g)) i) n =
fmerge (delta f) (delta g) n
  move=> k; rewrite -sum_fmerge_conv //.
5ae4425085bf835354
increasing (delta (fnorm f))
853
increasing (delta (fnorm g))
84e
    by apply: increasing_ext dfI => i; rewrite delta_fnorm.
853
857
84d
  by apply: increasing_ext dgI => i; rewrite delta_fnorm.
834
84f
rewrite /delta big_ord_recr /= addnC addnK.
834
fmerge (fun n : nat => fnorm f n.+1 - fnorm f n)
  (fun n : nat => fnorm g n.+1 - fnorm g n) n =
fmerge (fun n : nat => f n.+1 - f n)
  (fun n : nat => g n.+1 - g n) n
by apply: fmerge_aux_ext => i; apply: delta_fnorm.
Qed.

Lemma convex_conv f g : convex f -> convex g -> convex (conv f g).
5ad
convex f -> convex g -> convex (conv f g)
Proof.
863
move=> [fI dfI] [gI dgI]; split; first by apply: increasing_conv.
5ae4425085bf835
increasing (delta (conv f g))
apply: increasing_ext => [i|]; first by apply/sym_equal/delta_conv.
86a
increasing (fmerge (delta f) (delta g))
by apply: increasing_fmerge.
Qed.

End Convex.

Notation "\min_ ( i <= n ) F" := (bigmin (fun i => F) n)
 (at level 41, F at level 41, i, n at level 50,
  format "\min_ ( i  <=  n )  F").


(* Mimic AC match for leq_trans *)
Ltac is_num term :=
 match term with 
 | 0 => true 
 | S ?X => is_num X
 | _ => false
end.

Ltac split_term term :=
 match term with 
 | ?X * ?Y => match is_num X with true =>  constr:((X, Y))
              | false => 
              let v := once (split_term X) in constr:((fst v, snd v * Y)) 
              end
 | ?X => match is_num X with true => constr:((X, 1)) 
                             | _ => constr:((1, X)) end
 | _ => false
end.


Ltac delta_term n1 n2 t2 :=
  let n :=  constr:(n1 - n2) in
  let n1 := eval compute in n in
  let vt2 := eval lazy delta [fst snd] iota beta in t2 in 
  let r :=
    match n1 with 
    | 0 => constr:(0) 
    | 1 => constr:(t2) 
    | ?X  => 
    match vt2 with | 1 => X | _ => constr:(X * vt2) end
    end in
   eval lazy delta [fst snd] iota beta in r. 
    
Ltac delta_lterm2 n1 t1 lt2 :=
 match lt2 with 
 |  ?X2 + ?Y2 =>
     let v2 := split_term Y2 in
     let n2 := constr:(fst v2) in
     let t2 := constr:(snd v2) in
     let t := constr:((t1, t2)) in
     let vt := eval lazy delta [fst snd] iota beta in t in 
     match vt with 
     | (?X, ?X) => delta_term n1 n2 t2
     |  _  => delta_lterm2 n1 t1 X2
     end
 |   ?Y2 =>
     let v2 := split_term Y2 in
     let n2 := constr:(fst v2) in
     let t2 := constr:(snd v2) in 
     let t := constr:((t1, t2)) in
     let vt := eval lazy delta [fst snd] iota beta in t in 
     match vt with 
     | (?X, ?X) => delta_term n1 n2 t2
     |  _  => delta_term n1 0 t1
     end
end.

Ltac make_sum t1 t2 :=
  match t1 with 0 => t2 | _ => 
  match t2 with 0 => t1 | _ => constr:(t1 + t2) end end. 
  
Ltac delta_lterm1 lt1 lt2 :=
 match lt1 with 
 |  ?X1 + ?Y1 =>
     let v1 := split_term Y1 in
     let n1 := constr:(fst v1) in
     let t1 := constr:(snd v1) in 
     let r1 := delta_lterm1 X1 lt2 in
     let r2 := delta_lterm2 n1 t1 lt2 in make_sum r1 r2

 |   ?Y1 =>
     let v1 := split_term Y1 in
     let n1 := constr:(fst v1) in
     let t1 := constr:(snd v1) in delta_lterm2 n1 t1 lt2
end.

Ltac test t1 t2 := let xx := delta_lterm1 t1 t2 in pose kk := xx.

Ltac applyr H :=
  rewrite -?mul2n in H |- *;
  match goal with 
  H: is_true (leq _ ?X) |- is_true (leq _ ?Y) =>
    ring_simplify X Y in H;
    ring_simplify X Y; rewrite ?[nat_of_bin _]/= in H |- *
  end;
  let Z := fresh "Z" in
  match goal with 
  H: is_true (leq _ ?X1) |- is_true (leq _ ?Y1) =>
    let v := delta_lterm1 Y1 X1 in
    (try (rewrite [Z in _ <= Z](_ : _ = v + X1))); 
    [ apply: leq_trans (leq_add (leqnn _) H); rewrite {H}// ?(add0n,addn0) 
     | ring]
  end.
  
Ltac applyl H :=
  rewrite -?mul2n in H |- *;
  match goal with 
  H: is_true (leq ?X _) |- is_true (leq ?Y _) =>
    ring_simplify X Y; ring_simplify X Y in H;
    rewrite ?[nat_of_bin _]/= in H |- *
  end;
  let Z := fresh "Z" in
  match goal with 
  H: is_true (leq ?X1 _) |- is_true (leq ?Y1 _) =>
    let v := delta_lterm1 Y1 X1 in
    (try rewrite [Z in Z <= _](_ : Y1 = v + X1));
    [apply: leq_trans (leq_add (leqnn _) H) _;
     rewrite {H}// ?(add0n,addn0) | ring]
  end.

Ltac gsimpl :=
  rewrite -?mul2n in |- *;
  match goal with 
  |- is_true (leq ?X ?Y) =>
    ring_simplify X Y; rewrite ?[nat_of_bin _]/=
  end;
  let Z := fresh "Z" in
  match goal with 
    |- is_true (leq ?X1 ?Y1) =>
    let v := delta_lterm1 Y1 X1 in
    match v with 
    | 0 => 
    let v := delta_lterm1 X1 Y1 in
    let v1 := delta_lterm1 X1 v in
    let v2 := delta_lterm1 Y1 v1 in
    (try (rewrite [Z in _ <= Z](_ : Y1 = v2 + v1); last by ring));
    (try (rewrite [Z in Z <= _](_ : X1 = v + v1); last by ring));
    rewrite ?leq_add2r
    | _ => 
    let v1 := delta_lterm1 Y1 v in
    let v2 := delta_lterm1 X1 v1 in
    (try (rewrite [Z in _ <= Z](_ : Y1 = v + v1); last by ring));
    (try (rewrite [Z in Z <= _](_ : X1 = v2 + v1); last by ring));
    rewrite ?leq_add2r
  end
  end.
  
Ltac sring := rewrite -!mul2n; ring.
Ltac changel t :=
  let X := fresh "X" in 
  rewrite [X in X <= _](_ : _ = t); last by (ring || sring).
Ltac changer t := 
  let X := fresh "X" in 
  rewrite [X in _ <= X](_ : _ = t); last by (ring || sring).