(******************************************************************************)
(*                                                                            *)
(*                                  PHI                                       *)
(*                                                                            *)
(*   phi n = \sum_(i < n) 2 ^ troot n                                         *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

From mathcomp Require Import all_ssreflect.
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]
From hanoi Require Import triangular.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition phi n := foldr (addn \o (fun i => 2 ^ troot i)) 0 (iota 0 n).

Notation "'ϕ' n" := (phi n) (format "'ϕ' n", at level 0).

Compute zip (iota 0 11) (map phi (iota 0 11)).
= [:: (0, 0); (1, 1); (2, 3); (3, 5); (4, 9);
      (5, 13); (6, 17); (7, 25); (8, 33);
      (9, 41); (10, 49)]
: seq (nat * nat)

Lemma phiE n : phi n = \sum_(i < n) 2 ^ troot i.
n:nat
ϕ(n) = \sum_(i < n) 2 ^ ∇i
Proof.
3
rewrite -(@big_mkord _ _ _ _ predT (fun i => 2 ^ (troot i))).
5
ϕ(n) = \sum_(0 <= i < n | predT i) 2 ^ ∇i
rewrite unlock /reducebig /phi.
5
foldr (addn \o (fun i : nat => 2 ^ ∇i)) 0 (iota 0 n) =
foldr
  (applybig \o
     (fun i : nat => BigBody i addn (predT i) (2 ^ ∇i)))
  0 (index_iota 0 n)
by rewrite /index_iota subn0.
Qed.

Lemma phiS n : phi n.+1 = phi n + 2 ^ (troot n).
5
ϕ(n.+1) = ϕ(n) + 2 ^ ∇n
Proof.
12 by rewrite !phiE big_ord_recr. Qed.

Lemma phi_le m n : m <= n -> phi m <= phi n.
m, n:nat
m <= n -> ϕ(m) <= ϕ(n)
Proof.
17
elim: n m => [[] //|n IH m].
6
IH:forall m : nat, m <= n -> ϕ(m) <= ϕ(n)
m:nat
m <= n.+1 -> ϕ(m) <= ϕ(n.+1)
rewrite leq_eqVlt => /orP[/eqP->//|/IH /leq_trans->//].
20
ϕ(n) <= ϕ(n.+1)
by rewrite phiS leq_addr.
Qed.

Lemma phi_gt0 n : (0 < phi n) = (0 < n).
5
(0 < ϕ(n)) = (0 < n)
Proof.
29 by case: n. Qed.

Lemma phi_deltaD n p :
  p <= n.+1 -> phi (delta n + p) = 1 + (n + p) * 2 ^ n - 2 ^ n.
n, p:nat
p <= n.+1 -> ϕ(Δn + p) = 1 + (n + p) * 2 ^ n - 2 ^ n
Proof.
2e
elim: n p => [|n IHn]; first by case => // [] [|p].
6
IHn:forall p : nat, p <= n.+1 -> ϕ(Δn + p) = 1 + (n + p) * 2 ^ n - 2 ^ n
forall p : nat,
p <= n.+2 ->
ϕ(Δn.+1 + p) = 1 + (n.+1 + p) * 2 ^ n.+1 - 2 ^ n.+1
elim => [_|p IHp pLn].
37
ϕ(Δn.+1 + 0) = 1 + (n.+1 + 0) * 2 ^ n.+1 - 2 ^ n.+1
638
p:nat
IHp:p <= n.+2 -> ϕ(Δn.+1 + p) = 1 + (n.+1 + p) * 2 ^ n.+1 - 2 ^ n.+1
pLn:p < n.+2
ϕ(Δn.+1 + p.+1) =
1 + (n.+1 + p.+1) * 2 ^ n.+1 - 2 ^ n.+1
  rewrite !addn0 deltaS IHn // -addnBA; last first.
37
2 ^ n <= (n + n.+1) * 2 ^ n
37
1 + ((n + n.+1) * 2 ^ n - 2 ^ n) =
1 + n.+1 * 2 ^ n.+1 - 2 ^ n.+1
3f
    by rewrite -[X in X <= _]mul1n leq_mul2r addnS orbT.
37
4b
3e
  rewrite -[X in _ + (_ - X)]mul1n -mulnBl addnS subn1 /=.
37
1 + (n + n) * 2 ^ n = 1 + n.+1 * 2 ^ n.+1 - 2 ^ n.+1
3e
  rewrite addnn -muln2 -mulnA -expnS.
37
1 + n * 2 ^ n.+1 = 1 + n.+1 * 2 ^ n.+1 - 2 ^ n.+1
3e
  rewrite -{1}[n]subn0 -subSS mulnBl mul1n addnBA //.
37
2 ^ n.+1 <= n.+1 * 2 ^ n.+1
3e
  by rewrite -[X in X <= _]mul1n leq_mul2r orbT.
40
44
rewrite addnS phiS IHp 1?ltnW //.
40
1 + (n.+1 + p) * 2 ^ n.+1 - 2 ^ n.+1 +
2 ^ ∇(Δn.+1 + p) =
1 + (n.+1 + p.+1) * 2 ^ n.+1 - 2 ^ n.+1
rewrite (_ : troot _ = n.+1).
40
1 + (n.+1 + p) * 2 ^ n.+1 - 2 ^ n.+1 + 2 ^ n.+1 =
1 + (n.+1 + p.+1) * 2 ^ n.+1 - 2 ^ n.+1
40
∇(Δn.+1 + p) = n.+1
  rewrite subnK.
40
1 + (n.+1 + p) * 2 ^ n.+1 =
1 + (n.+1 + p.+1) * 2 ^ n.+1 - 2 ^ n.+1
40
2 ^ n.+1 <= 1 + (n.+1 + p) * 2 ^ n.+1
67
    by rewrite addnS mulSn [X in _ = _ + X - _]addnC addnA addnK.
40
6f
66
  by rewrite [_ + p]addSn mulSn addnC -addnA leq_addr.
40
68
by apply/eqP; rewrite trootE leq_addr [delta _.+2]deltaS ltn_add2l.
Qed.

Fact phi_simpl a n p q :
  0 < n -> a + (n + p) * 2 ^ q - 2 ^ q  = a + (n.-1 + p) * 2 ^ q.
a, n, p, q:nat
0 < n ->
a + (n + p) * 2 ^ q - 2 ^ q = a + (n.-1 + p) * 2 ^ q
Proof.
77
case: n => // n _.
a, p, q, n:nat
a + (n.+1 + p) * 2 ^ q - 2 ^ q =
a + (n.+1.-1 + p) * 2 ^ q
rewrite -addnBA; last by rewrite addSn mulSn leq_addr.
80
a + ((n.+1 + p) * 2 ^ q - 2 ^ q) =
a + (n.+1.-1 + p) * 2 ^ q
by rewrite [_ + p]addSn mulSn [2 ^ _ + _]addnC addnK.
Qed.

Fact phi_simpr a n p q :
  0 < p -> a + (n + p) * 2 ^ q - 2 ^ q  = a + (n + p.-1) * 2 ^ q.
79
0 < p ->
a + (n + p) * 2 ^ q - 2 ^ q = a + (n + p.-1) * 2 ^ q
Proof.
88 by move=> H; rewrite ![n + _]addnC phi_simpl. Qed.

Lemma phi_modE n : 
  phi n = 1 + (troot n + tmod n) * 2 ^ (troot n) - 2 ^ (troot n).
5
ϕ(n) = 1 + (∇n + tmod n) * 2 ^ ∇n - 2 ^ ∇n
Proof.
8d by rewrite {1}[n]tmodE phi_deltaD // ltnW // ltnS tmod_le. Qed.

Lemma phi_deltaE n : 
 phi (delta n) = 1 + n * 2 ^ n - 2 ^ n.
5
ϕ(Δn) = 1 + n * 2 ^ n - 2 ^ n
Proof.
92 by rewrite phi_modE troot_delta tmod_delta addn0. Qed.

Lemma phi_modSE n : 
 phi n.+1 = 1 + (troot n + tmod n) * 2 ^ (troot n).
5
ϕ(n.+1) = 1 + (∇n + tmod n) * 2 ^ ∇n
Proof.
97
rewrite phi_modE.
5
1 + (∇n.+1 + tmod n.+1) * 2 ^ ∇n.+1 - 2 ^ ∇n.+1 =
1 + (∇n + tmod n) * 2 ^ ∇n
have /orP[/andP[/eqP-> /eqP->]|
          /and3P[/eqP->/eqP->/eqP]->] := troot_mod_case n.
5
1 + (∇n + (tmod n).+1) * 2 ^ ∇n - 2 ^ ∇n =
1 + (∇n + tmod n) * 2 ^ ∇n
5
1 + ((∇n).+1 + 0) * 2 ^ (∇n).+1 - 2 ^ (∇n).+1 =
1 + (∇n + ∇n) * 2 ^ ∇n
  by rewrite addnS mulSn addnCA [2 ^ _ + _]addnC addnK.
5
a5
rewrite addn0 mulSn addnCA [2 ^ _ + _]addnC addnK.
5
1 + ∇n * 2 ^ (∇n).+1 = 1 + (∇n + ∇n) * 2 ^ ∇n
by rewrite expnS addnn -mul2n mulnCA mulnA.
Qed.

Lemma phi_odd n : odd (phi n) = (0 < n).
5
odd ϕ(n) = (0 < n)
Proof.
ae
case: n => // [] [|n] //.
5
odd ϕ(n.+2) = (0 < n.+2)
rewrite phi_modSE oddD oddM oddX orbF.
5
odd 1 (+) odd (∇n.+1 + tmod n.+1) && (∇n.+1 == 0) =
(0 < n.+2)
case: troot (troot_gt0 (isT : 0 < n.+1)) => // k.
n, k:nat
0 < k.+1 ->
odd 1 (+) odd (k.+1 + tmod n.+1) && (k.+1 == 0) =
(0 < n.+2)
by rewrite andbF.
Qed.

Definition g n m := (phi m).*2 + (2 ^ (n - m)).-1.

Definition gmin n := delta (troot n).-1 + tmod n.

Lemma gmin_gt0 n : 1 < n -> 0 < gmin n.
5
1 < n -> 0 < gmin n
Proof.
c1
case: n => [|[|[|n _]]] //.
5
0 < gmin n.+3
apply: leq_trans (leq_addr _ _).
5
0 < Δ(∇n.+3).-1
have /troot_le : 3 <= n.+3 by [].
5
∇3 <= ∇n.+3 -> 0 < Δ(∇n.+3).-1
rewrite -[troot 3]/(2).
5
1 < ∇n.+3 -> 0 < Δ(∇n.+3).-1
case: troot => //= m.
n, m:nat
1 < m.+1 -> 0 < Δm
by rewrite ltnS => /delta_le.
Qed.

Lemma gminE n : n = gmin n + troot n.
5
n = gmin n + ∇n
Proof.
dc
case: n => //= n.
5
n.+1 = gmin n.+1 + ∇n.+1
rewrite {1}[n.+1]tmodE /gmin.
5
Δ(∇n.+1) + tmod n.+1 = Δ(∇n.+1).-1 + tmod n.+1 + ∇n.+1
case: troot (troot_gt0 (isT : 0 < n.+1)) => //= t _.
n, t:nat
Δt.+1 + tmod n.+1 = Δt + tmod n.+1 + t.+1
by rewrite deltaS addnAC.
Qed.

Lemma gmin_le n : gmin n <= n.
5
gmin n <= n
Proof.
ef by rewrite {2}[n]gminE leq_addr. Qed.

Lemma gmin_lt n : 0 < n -> gmin n < n.
5
0 < n -> gmin n < n
Proof.
f4
case: n => // n _.
5
gmin n.+1 < n.+1
rewrite {2}[n.+1]gminE -[X in X < _]addn0 ltn_add2l.
5
0 < ∇n.+1
by apply: troot_gt0.
Qed.

Lemma gmin_root n : troot (gmin n) = troot n - (tmod n != troot n).
5
∇(gmin n) = ∇n - (tmod n != ∇n)
Proof.
101
have [/eqP mEt|mDt] := boolP (tmod n == troot n).
6
mEt:tmod n = ∇n
∇(gmin n) = ∇n - ~~ true
6
mDt:tmod n != ∇n
∇(gmin n) = ∇n - ~~ false
  rewrite /gmin -mEt subn0.
108
∇(Δ(tmod n).-1 + tmod n) = tmod n
10b
  by case: tmod => //= t; rewrite -deltaS troot_delta.
10d
10f
have mLt : tmod n < troot n by rewrite ltn_neqAle mDt tmod_le.
610e
mLt:tmod n < ∇n
10f
rewrite subn1.
11a
∇(gmin n) = (∇n).-1
apply/eqP; rewrite /gmin trootE.
11a
Δ(∇n).-1 <= Δ(∇n).-1 + tmod n < Δ(∇n).-1.+1
case: n {mDt}mLt => // [] [|] // n mLt.
6
mLt:tmod n.+2 < ∇n.+2
Δ(∇n.+2).-1 <= Δ(∇n.+2).-1 + tmod n.+2 <
Δ(∇n.+2).-1.+1
case: troot mLt => //= t mLt.
ec
mLt:tmod n.+2 < t.+1
Δt <= Δt + tmod n.+2 < Δt.+1
by rewrite leq_addr deltaS ltn_add2l.
Qed.

Lemma gmin_mod n : tmod (gmin n) = (tmod n != troot n) * tmod n.
5
tmod (gmin n) = (tmod n != ∇n) * tmod n
Proof.
131
have [/eqP mEt|mDt] := boolP (tmod n == troot n).
108
tmod (gmin n) = ~~ true * tmod n
10d
tmod (gmin n) = ~~ false * tmod n
  rewrite mul0n /gmin -mEt.
108
tmod (Δ(tmod n).-1 + tmod n) = 0
139
  case: (tmod n) => // t.
6109
t:nat
tmod (Δt.+1.-1 + t.+1) = 0
139
  by rewrite -deltaS tmod_delta.
10d
13b
have mLt : tmod n < troot n by rewrite ltn_neqAle mDt tmod_le.
11a
13b
by rewrite mul1n /tmod {1}/gmin gmin_root mDt subn1 addnC addnK.
Qed.

Lemma gmin_root_lt m n : m < gmin n -> troot m < troot n.
19
m < gmin n -> ∇m < ∇n
Proof.
14d
move=> mLg.
1a
mLg:m < gmin n
∇m < ∇n
have nP : 0 < n by case: n mLg.
1a155
nP:0 < n
156
case: leqP => //; rewrite leq_eqVlt => /orP[/eqP tnEtm| /ltn_root]; last first.
15a
n < m -> false
1a15515b
tnEtm:∇n = ∇m
false
  by rewrite ltnNge (leq_trans _ (gmin_le _)) // ltnW.
162
164
have /eqP tnEtg : troot n == troot (gmin n).
162
∇n == ∇(gmin n)
1a15515b163
tnEtg:∇n = ∇(gmin n)
164
  by rewrite eqn_leq {1}tnEtm !troot_le // ?gmin_le // ltnW.
16e
164
have: tmod m < tmod (gmin n) by rewrite ltn_mod // -tnEtg.
16e
tmod m < tmod (gmin n) -> false
suff : tmod (gmin n) = 0 by move->.
16e
tmod (gmin n) = 0
rewrite gmin_mod.
16e
(tmod n != ∇n) * tmod n = 0
have := gmin_root n; case: eqP => //.
16e
tmod n <> ∇n ->
∇(gmin n) = ∇n - ~~ false -> ~~ false * tmod n = 0
rewrite -tnEtg subn1 => _ F.
1a15515b16316f
F:∇n = (∇n).-1
~~ false * tmod n = 0
have := ltnn (troot n).
186
(∇n < ∇n) = false -> ~~ false * tmod n = 0
by rewrite -{2}(prednK (troot_gt0 nP)) -F leqnn.
Qed.
  
Lemma phi_gmin n : phi n = g n (gmin n).
5
ϕ(n) = g n (gmin n)
Proof.
18e
case: n => // n.
5
ϕ(n.+1) = g n.+1 (gmin n.+1)
rewrite {1}phi_modE /g /gmin.
5
1 + (∇n.+1 + tmod n.+1) * 2 ^ ∇n.+1 - 2 ^ ∇n.+1 =
ϕ(Δ(∇n.+1).-1 + tmod n.+1).*2 +
(2 ^ (n.+1 - (Δ(∇n.+1).-1 + tmod n.+1))).-1
rewrite phi_deltaD; last by rewrite prednK // tmod_le.
5
1 + (∇n.+1 + tmod n.+1) * 2 ^ ∇n.+1 - 2 ^ ∇n.+1 =
(1 + ((∇n.+1).-1 + tmod n.+1) * 2 ^ (∇n.+1).-1 -
 2 ^ (∇n.+1).-1).*2 +
(2 ^ (n.+1 - (Δ(∇n.+1).-1 + tmod n.+1))).-1
set x := troot _; set y := tmod _.
6
x:=∇n.+1:nat
y:=tmod n.+1:nat
1 + (x + y) * 2 ^ x - 2 ^ x =
(1 + (x.-1 + y) * 2 ^ x.-1 - 2 ^ x.-1).*2 +
(2 ^ (n.+1 - (Δx.-1 + y))).-1
rewrite phi_simpl //.
1a1
1 + (x.-1 + y) * 2 ^ x =
(1 + (x.-1 + y) * 2 ^ x.-1 - 2 ^ x.-1).*2 +
(2 ^ (n.+1 - (Δx.-1 + y))).-1
rewrite doubleB doubleD -!muln2 -!mulnA -!expnSr !prednK //.
1a1
1 + (x.-1 + y) * 2 ^ x =
1 * 2 + (x.-1 + y) * 2 ^ x - 2 ^ x +
(2 ^ (n.+1 - (Δx.-1 + y))).-1
have ->: n.+1 = delta x.-1 + x + y.
1a1
n.+1 = Δx.-1 + x + y
1a1
1 + (x.-1 + y) * 2 ^ x =
1 * 2 + (x.-1 + y) * 2 ^ x - 2 ^ x +
(2 ^ (Δx.-1 + x + y - (Δx.-1 + y))).-1
  by rewrite -{2}[x]prednK // -deltaS prednK // -tmodE.
1a1
1b3
rewrite [_ + x + y]addnAC [_ + x]addnC addnK.
1a1
1 + (x.-1 + y) * 2 ^ x =
1 * 2 + (x.-1 + y) * 2 ^ x - 2 ^ x + (2 ^ x).-1
rewrite {}/x {}/y.
5
1 + ((∇n.+1).-1 + tmod n.+1) * 2 ^ ∇n.+1 =
1 * 2 + ((∇n.+1).-1 + tmod n.+1) * 2 ^ ∇n.+1 -
2 ^ ∇n.+1 + (2 ^ ∇n.+1).-1
case: n => // [] [|n] //.
5
1 + ((∇n.+3).-1 + tmod n.+3) * 2 ^ ∇n.+3 =
1 * 2 + ((∇n.+3).-1 + tmod n.+3) * 2 ^ ∇n.+3 -
2 ^ ∇n.+3 + (2 ^ ∇n.+3).-1
rewrite phi_simpl //.
5
1 + ((∇n.+3).-1 + tmod n.+3) * 2 ^ ∇n.+3 =
1 * 2 + ((∇n.+3).-2 + tmod n.+3) * 2 ^ ∇n.+3 +
(2 ^ ∇n.+3).-1
rewrite -[_.-1]prednK // addSn.
5
(0 + ((∇n.+3).-2.+1 + tmod n.+3) * 2 ^ ∇n.+3).+1 =
1 * 2 + ((∇n.+3).-2.+1.-1 + tmod n.+3) * 2 ^ ∇n.+3 +
(2 ^ ∇n.+3).-1
case: expn (expn_gt0 2 (troot n.+3)) => // u __.
n, u:nat
__:(0 < u.+1) = (0 < 2) || (∇n.+3 == 0)
(0 + ((∇n.+3).-2.+1 + tmod n.+3) * u.+1).+1 =
1 * 2 + ((∇n.+3).-2.+1.-1 + tmod n.+3) * u.+1 +
u.+1.-1
by rewrite addSn mulSn add0n -addSn addnAC.
Qed.

Lemma gS n m : m.+1 < n -> g n m.+1 + 2 ^ (n - m.+1) = g n m + 2 ^ (troot m).+1.
d8
m.+1 < n ->
g n m.+1 + 2 ^ (n - m.+1) = g n m + 2 ^ (∇m).+1
Proof.
1d3
move=> H; rewrite /g !phi_modE.
d9
H:m.+1 < n
(1 + (∇m.+1 + tmod m.+1) * 2 ^ ∇m.+1 - 2 ^ ∇m.+1).*2 +
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(1 + (∇m + tmod m) * 2 ^ ∇m - 2 ^ ∇m).*2 +
(2 ^ (n - m)).-1 + 2 ^ (∇m).+1
rewrite phi_simpl; last by rewrite troot_gt0.
1da
(1 + ((∇m.+1).-1 + tmod m.+1) * 2 ^ ∇m.+1).*2 +
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(1 + (∇m + tmod m) * 2 ^ ∇m - 2 ^ ∇m).*2 +
(2 ^ (n - m)).-1 + 2 ^ (∇m).+1
rewrite -[n - m]prednK; last first.
1da
0 < n - m
1da
(1 + ((∇m.+1).-1 + tmod m.+1) * 2 ^ ∇m.+1).*2 +
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(1 + (∇m + tmod m) * 2 ^ ∇m - 2 ^ ∇m).*2 +
(2 ^ (n - m).-1.+1).-1 + 2 ^ (∇m).+1
  by rewrite subn_gt0 (leq_trans _ H).
1da
1e7
rewrite -subnS expnS mul2n -[(2 ^ _).*2]addnn.
1da
(1 + ((∇m.+1).-1 + tmod m.+1) * 2 ^ ∇m.+1).*2 +
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(1 + (∇m + tmod m) * 2 ^ ∇m - 2 ^ ∇m).*2 +
(2 ^ (n - m.+1) + 2 ^ (n - m.+1)).-1 + 2 ^ (∇m).+1
have := troot_mod_case m.
1da
(∇m.+1 == ∇m) && (tmod m.+1 == (tmod m).+1)
|| [&& ∇m.+1 == (∇m).+1, tmod m.+1 == 0
     & tmod m == ∇m] ->
(1 + ((∇m.+1).-1 + tmod m.+1) * 2 ^ ∇m.+1).*2 +
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(1 + (∇m + tmod m) * 2 ^ ∇m - 2 ^ ∇m).*2 +
(2 ^ (n - m.+1) + 2 ^ (n - m.+1)).-1 + 2 ^ (∇m).+1
case/orP=> [/andP[/eqP H1 /eqP H2]|/and3P[/eqP H1 /eqP H2 /eqP H3]].
d91db
H1:∇m.+1 = ∇m
H2:tmod m.+1 = (tmod m).+1
1ee
d91db
H1:∇m.+1 = (∇m).+1
H2:tmod m.+1 = 0
H3:tmod m = ∇m
1ee
  rewrite /g H1 H2 phi_simpl; last by rewrite -H1 troot_gt0.
1f6
(1 + ((∇m).-1 + (tmod m).+1) * 2 ^ ∇m).*2 +
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(1 + ((∇m).-1 + tmod m) * 2 ^ ∇m).*2 +
(2 ^ (n - m.+1) + 2 ^ (n - m.+1)).-1 + 2 ^ (∇m).+1
1f9
  rewrite addnS mulSnr !addnA doubleD -!addnA; congr (_ + _).
1f6
(2 ^ ∇m).*2 + ((2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1)) =
(2 ^ (n - m.+1) + 2 ^ (n - m.+1)).-1 + 2 ^ (∇m).+1
1f9
  rewrite -mul2n -expnS addnC; congr (_ + _).
1f6
(2 ^ (n - m.+1)).-1 + 2 ^ (n - m.+1) =
(2 ^ (n - m.+1) + 2 ^ (n - m.+1)).-1
1f9
  by case: (_ ^ _).
1fb
1ee
rewrite H1 H2 H3 addnn addn0 /=.
1fb
(1 + ∇m * 2 ^ (∇m).+1).*2 + (2 ^ (n - m.+1)).-1 +
2 ^ (n - m.+1) =
(1 + (∇m).*2 * 2 ^ ∇m - 2 ^ ∇m).*2 +
(2 ^ (n - m.+1) + 2 ^ (n - m.+1)).-1 + 2 ^ (∇m).+1
set x := troot _; set y := n - _.
d91db1fc1fd1fe
x:=∇m:nat
y:=n - m.+1:nat
(1 + x * 2 ^ x.+1).*2 + (2 ^ y).-1 + 2 ^ y =
(1 + x.*2 * 2 ^ x - 2 ^ x).*2 + (2 ^ y + 2 ^ y).-1 +
2 ^ x.+1
rewrite doubleB [in RHS]addnAC -[(2 ^ _).*2]mul2n -expnS subnK; last first.
215
2 ^ x.+1 <= (1 + x.*2 * 2 ^ x).*2
215
(1 + x * 2 ^ x.+1).*2 + (2 ^ y).-1 + 2 ^ y =
(1 + x.*2 * 2 ^ x).*2 + (2 ^ y + 2 ^ y).-1
  rewrite expnS mul2n leq_double.
215
2 ^ x <= 1 + x.*2 * 2 ^ x
21d
  by case: x => //= x; rewrite doubleS mulSnr addnA leq_addl.
215
21f
rewrite -[x.*2]muln2 -mulnA -expnS -addnA; congr (_ +_).
215
(2 ^ y).-1 + 2 ^ y = (2 ^ y + 2 ^ y).-1
by case: expn (expn_gt0 2 y).
Qed.

Lemma gS_minl n m : m < gmin n -> g n m.+1 <= g n m.
d8
m < gmin n -> g n m.+1 <= g n m
Proof.
22c
case: n => // n mLg.
1a
mLg:m < gmin n.+1
g n.+1 m.+1 <= g n.+1 m
have mLn : m < n.
233
m < n
1a234
mLn:m < n
235
   by rewrite -ltnS; apply: leq_trans (gmin_lt _).
23c
235
suff mtLm : m.+1 + troot m <= n.
1a23423d
mtLm:m.+1 + ∇m <= n
235
23c
m.+1 + ∇m <= n
  rewrite -(leq_add2r (2 ^ (n.+1 - m.+1))) (gS _) //.
244
g n.+1 m + 2 ^ (∇m).+1 <= g n.+1 m + 2 ^ (n.+1 - m.+1)
246
  by rewrite leq_add2l leq_pexp2l // ltn_subRL.
23c
248
rewrite (leq_trans (_ : _ <= gmin n.+1 + troot m)) //.
23c
m.+1 + ∇m <= gmin n.+1 + ∇m
23c
gmin n.+1 + ∇m <= n
  by rewrite leq_add2r.
23c
256
rewrite -ltnS -addnS.
23c
gmin n.+1 + (∇m).+1 <= n.+1
rewrite /gmin {3}[n.+1]tmodE addnAC leq_add2r.
23c
Δ(∇n.+1).-1 + (∇m).+1 <= Δ(∇n.+1)
have : 0 < troot n.+1 by apply troot_gt0.
23c
0 < ∇n.+1 -> Δ(∇n.+1).-1 + (∇m).+1 <= Δ(∇n.+1)
case E : troot => [|t] _ //=.
1a23423d144
E:∇n.+1 = t.+1
Δt + (∇m).+1 <= Δt.+1
rewrite deltaS -E leq_add2l.
269
∇m < ∇n.+1
by apply: gmin_root_lt.
Qed.

Lemma gS_minr n m : gmin n <= m -> m.+1 < n -> g n m <= g n m.+1.
d8
gmin n <= m -> m.+1 < n -> g n m <= g n m.+1
Proof.
271
move=> gLm mLn.
d9
gLm:gmin n <= m
mLn:m.+1 < n
g n m <= g n m.+1
suff mtLm : n <= m.+1 + (troot m).+1.
d927927a
mtLm:n <= m.+1 + (∇m).+1
27b
278
n <= m.+1 + (∇m).+1
  rewrite -(leq_add2r (2 ^ (n - m.+1))) (gS _) //.
27f
g n m + 2 ^ (n - m.+1) <= g n m + 2 ^ (∇m).+1
281
  by rewrite leq_add2l leq_pexp2l // leq_subLR.
278
283
rewrite [n]gminE addSnnS leq_add //.
278
∇n <= (∇m).+2
apply: leq_trans (_ : (troot (gmin n)).+2 <= _).
278
∇n <= (∇(gmin n)).+2
278
(∇(gmin n)).+1 < (∇m).+2
  rewrite gmin_root; case: eqP; first by rewrite subn0 ltnW.
278
tmod n <> ∇n -> ∇n <= (∇n - ~~ false).+2
293
  by rewrite subn1; case: troot.
278
295
by rewrite !ltnS troot_le.
Qed.
 
Lemma gmin_min n m : m < n -> g n (gmin n) <= g n m.
d8
m < n -> g n (gmin n) <= g n m
Proof.
29e
move=> mLn.
d923d
g n (gmin n) <= g n m
have [gLm|mLg] := leqP (gmin n) m.
d923d279
2a6
d923d155
2a6
  move: mLn; rewrite -(subnK gLm).
d9279
m - gmin n + gmin n < n ->
g n (gmin n) <= g n (m - gmin n + gmin n)
2ab
  elim: subn => // k IH H1.
d9279
k:nat
IH:k + gmin n < n ->
g n (gmin n) <= g n (k + gmin n)
H1:k.+1 + gmin n < n
g n (gmin n) <= g n (k.+1 + gmin n)
2ab
  rewrite addSn (leq_trans (IH _) (gS_minr _ _)) ?leq_addl //.
2b6
k + gmin n < n
2ab
  by apply: leq_trans H1; rewrite ltnS addSnnS leq_add2l.
2ad
2a6
rewrite -(subKn (ltnW mLg)).
2ad
g n (gmin n) <= g n (gmin n - (gmin n - m))
elim: (gmin n - m) (leq_subr m (gmin n)) => [|k IH kLm].
2ad
0 <= gmin n -> g n (gmin n) <= g n (gmin n - 0)
d923d1552b7
IH:k <= gmin n -> g n (gmin n) <= g n (gmin n - k)
kLm:k < gmin n
g n (gmin n) <= g n (gmin n - k.+1)
  by rewrite subn0.
2cc
2cf
apply: leq_trans (IH (ltnW kLm)) _.
2cc
g n (gmin n - k) <= g n (gmin n - k.+1)
rewrite -subSS subSn //.
2cc
g n (gmin n - k.+1).+1 <= g n (gmin n - k.+1)
by rewrite gS_minl // -subSn // subSS leq_subr.
Qed.

(* This is (2.1) *)
Lemma phi_leD a b : phi (a + b) <= (phi a).*2 + (2 ^ b).-1.
a, b:nat
ϕ(a + b) <= ϕ(a).*2 + (2 ^ b).-1
Proof.
2dc
case: b => [|b]; first by rewrite !addn0 -addnn leq_addr.
2de
ϕ(a + b.+1) <= ϕ(a).*2 + (2 ^ b.+1).-1
rewrite phi_gmin -{3}[b.+1](addnK a _) [b.+1 + a]addnC.
2de
g (a + b.+1) (gmin (a + b.+1)) <=
ϕ(a).*2 + (2 ^ (a + b.+1 - a)).-1
apply: gmin_min.
2de
a < a + b.+1
by rewrite -addSnnS leq_addr.
Qed.