NDefOps.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Import Bool. (* To get the orb and negb function *)
Require Import RelationPairs.
Require Export NStrongRec.

In this module, we derive generic implementations of usual operators just via the use of a recursion function.

Module NdefOpsProp (Import N : NAxiomsRecSig').
Include NStrongRecProp N.

Nullity Test

Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
  recursion a (fun _ _ => b) n.

Arguments if_zero [A] a b n.

Instance if_zero_wd (A : Type) :
 Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).A:Type
Proper (Logic.eq ==> Logic.eq ==> eq ==> Logic.eq)
  (if_zero (A:=A))
Proof.A:Type
Proper (Logic.eq ==> Logic.eq ==> eq ==> Logic.eq)
  (if_zero (A:=A))
unfold if_zero. (* TODO : solve_proper : SLOW + BUG *)A:Type
Proper (Logic.eq ==> Logic.eq ==> eq ==> Logic.eq)
  (fun (a b : A) (n : t) =>
   recursion a (fun (_ : t) (_ : A) => b) n)
f_equiv'.
Qed.

Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.forall (A : Type) (a b : A), if_zero a b 0 = a
Proof.forall (A : Type) (a b : A), if_zero a b 0 = a
unfold if_zero; intros; now rewrite recursion_0.
Qed.

Theorem if_zero_succ :
 forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b.forall (A : Type) (a b : A) (n : t),
if_zero a b (S n) = b
Proof.forall (A : Type) (a b : A) (n : t),
if_zero a b (S n) = b
intros; unfold if_zero.A:Type
a, b:A
n:t
recursion a (fun (_ : t) (_ : A) => b) (S n) = b
now rewrite recursion_succ.
Qed.

(*****************************************************)

Addition

Definition def_add (x y : N.t) := recursion y (fun _ => S) x.

Local Infix "+++" := def_add (at level 50, left associativity).

Instance def_add_wd : Proper (N.eq ==> N.eq ==> N.eq) def_add.Proper (eq ==> eq ==> eq) def_add
Proof.Proper (eq ==> eq ==> eq) def_add
unfold def_add.Proper (eq ==> eq ==> eq)
  (fun x y : t => recursion y (fun _ : t => S) x) f_equiv'.
Qed.

Theorem def_add_0_l : forall y, 0 +++ y == y.forall y : t, 0 +++ y == y
Proof.forall y : t, 0 +++ y == y
intro y.y:t
0 +++ y == y unfold def_add.y:t
recursion y (fun _ : t => S) 0 == y now rewrite recursion_0.
Qed.

Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y).forall x y : t, S x +++ y == S (x +++ y)
Proof.forall x y : t, S x +++ y == S (x +++ y)
intros x y; unfold def_add.x, y:t
recursion y (fun _ : t => S) (S x) ==
S (recursion y (fun _ : t => S) x)
rewrite recursion_succ; f_equiv'.
Qed.

Theorem def_add_add : forall n m, n +++ m == n + m.forall n m : t, n +++ m == n + m
Proof.forall n m : t, n +++ m == n + m
intros n m; induct n.m:t
0 +++ m == 0 + m
m:t
forall n : t, n +++ m == n + m -> S n +++ m == S n + m
now rewrite def_add_0_l, add_0_l.m:t
forall n : t, n +++ m == n + m -> S n +++ m == S n + m
intros n H.m, n:t
H:n +++ m == n + m
S n +++ m == S n + m now rewrite def_add_succ_l, add_succ_l, H.
Qed.

(*****************************************************)

Multiplication

Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y.

Local Infix "**" := def_mul (at level 40, left associativity).

Instance def_mul_wd : Proper (N.eq ==> N.eq ==> N.eq) def_mul.Proper (eq ==> eq ==> eq) def_mul
Proof.Proper (eq ==> eq ==> eq) def_mul
unfold def_mul. (* TODO : solve_proper SLOW + BUG *)Proper (eq ==> eq ==> eq)
  (fun x y : t =>
   recursion 0 (fun _ p : t => p +++ x) y)
f_equiv'.
Qed.

Theorem def_mul_0_r : forall x, x ** 0 == 0.forall x : t, x ** 0 == 0
Proof.forall x : t, x ** 0 == 0
intro.x:t
x ** 0 == 0 unfold def_mul.x:t
recursion 0 (fun _ p : t => p +++ x) 0 == 0 now rewrite recursion_0.
Qed.

Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x.forall x y : t, x ** S y == x ** y +++ x
Proof.forall x y : t, x ** S y == x ** y +++ x
intros x y; unfold def_mul.x, y:t
recursion 0 (fun _ p : t => p +++ x) (S y) ==
recursion 0 (fun _ p : t => p +++ x) y +++ x
rewrite recursion_succ; auto with *.x, y:t
Proper (eq ==> eq ==> eq) (fun _ p : t => p +++ x)
f_equiv'.
Qed.

Theorem def_mul_mul : forall n m, n ** m == n * m.forall n m : t, n ** m == n * m
Proof.forall n m : t, n ** m == n * m
intros n m; induct m.n:t
n ** 0 == n * 0
n:t
forall n0 : t,
n ** n0 == n * n0 -> n ** S n0 == n * S n0
now rewrite def_mul_0_r, mul_0_r.n:t
forall n0 : t,
n ** n0 == n * n0 -> n ** S n0 == n * S n0
intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH.
Qed.

(*****************************************************)

Order

Definition ltb (m : N.t) : N.t -> bool :=
recursion
  (if_zero false true)
  (fun _ f n => recursion false (fun n' _ => f n') n)
  m.

Local Infix "<<" := ltb (at level 70, no associativity).

Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb.Proper (eq ==> eq ==> Logic.eq) ltb
Proof.Proper (eq ==> eq ==> Logic.eq) ltb
unfold ltb.Proper (eq ==> eq ==> Logic.eq)
  (fun m : t =>
   recursion (if_zero false true)
     (fun (_ : t) (f : t -> bool) (n : t) =>
      recursion false
        (fun (n' : t) (_ : bool) => f n') n) m) f_equiv'.
Qed.

Theorem ltb_base : forall n, 0 << n = if_zero false true n.forall n : t, (0 << n) = if_zero false true n
Proof.forall n : t, (0 << n) = if_zero false true n
intro n; unfold ltb; now rewrite recursion_0.
Qed.

Theorem ltb_step :
  forall m n, S m << n = recursion false (fun n' _ => m << n') n.forall m n : t,
(S m << n) =
recursion false (fun (n' : t) (_ : bool) => m << n') n
Proof.forall m n : t,
(S m << n) =
recursion false (fun (n' : t) (_ : bool) => m << n') n
intros m n; unfold ltb at 1.m, n:t
recursion (if_zero false true)
  (fun (_ : t) (f : t -> bool) (n0 : t) =>
   recursion false (fun (n' : t) (_ : bool) => f n')
     n0) (S m) n =
recursion false (fun (n' : t) (_ : bool) => m << n') n
f_equiv.m, n:t
(Logic.eq ==> Logic.eq)%signature
  (recursion (if_zero false true)
     (fun (_ : t) (f : t -> bool) (n0 : t) =>
      recursion false
        (fun (n' : t) (_ : bool) => f n') n0) (S m))
  (recursion false
     (fun (n' : t) (_ : bool) => m << n'))
rewrite recursion_succ; f_equiv'.
Qed.

(* Above, we rewrite applications of function. Is it possible to rewrite
functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
lt_step n (recursion lt_base lt_step n)? *)

Theorem ltb_0 : forall n, n << 0 = false.forall n : t, (n << 0) = false
Proof.forall n : t, (n << 0) = false
cases n.(0 << 0) = false
forall n : t, (S n << 0) = false
rewrite ltb_base; now rewrite if_zero_0.forall n : t, (S n << 0) = false
intro n; rewrite ltb_step.n:t
recursion false (fun (n' : t) (_ : bool) => n << n') 0 =
false now rewrite recursion_0.
Qed.

Theorem ltb_0_succ : forall n, 0 << S n = true.forall n : t, (0 << S n) = true
Proof.forall n : t, (0 << S n) = true
intro n; rewrite ltb_base; now rewrite if_zero_succ.
Qed.

Theorem succ_ltb_mono : forall n m, (S n << S m) = (n << m).forall n m : t, (S n << S m) = (n << m)
Proof.forall n m : t, (S n << S m) = (n << m)
intros n m.n, m:t
(S n << S m) = (n << m)
rewrite ltb_step.n, m:t
recursion false (fun (n' : t) (_ : bool) => n << n')
  (S m) = (n << m) rewrite recursion_succ; f_equiv'.
Qed.

Theorem ltb_lt : forall n m, n << m = true <-> n < m.forall n m : t, (n << m) = true <-> n < m
Proof.forall n m : t, (n << m) = true <-> n < m
double_induct n m.forall m : t, (0 << m) = true <-> 0 < m
forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m
cases m.(0 << 0) = true <-> 0 < 0
forall n : t, (0 << S n) = true <-> 0 < S n
forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m
rewrite ltb_0.false = true <-> 0 < 0
forall n : t, (0 << S n) = true <-> 0 < S n
forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m split; intro H; [discriminate H | false_hyp H nlt_0_r].forall n : t, (0 << S n) = true <-> 0 < S n
forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m
intro n.n:t
(0 << S n) = true <-> 0 < S n
forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m rewrite ltb_0_succ.n:t
true = true <-> 0 < S n
forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m split; intro; [apply lt_0_succ | reflexivity].forall n : t, (S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m
intro n.n:t
(S n << 0) = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m rewrite ltb_0.n:t
false = true <-> S n < 0
forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m split; intro H; [discriminate | false_hyp H nlt_0_r].forall n m : t,
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m
intros n m.n, m:t
(n << m) = true <-> n < m ->
(S n << S m) = true <-> S n < S m rewrite succ_ltb_mono.n, m:t
(n << m) = true <-> n < m ->
(n << m) = true <-> S n < S m now rewrite <- succ_lt_mono.
Qed.

Theorem ltb_ge : forall n m, n << m = false <-> n >= m.forall n m : t, (n << m) = false <-> m <= n
Proof.forall n m : t, (n << m) = false <-> m <= n
intros.n, m:t
(n << m) = false <-> m <= n rewrite <- not_true_iff_false, ltb_lt.n, m:t
~ n < m <-> m <= n apply nlt_ge.
Qed.

(*****************************************************)

Even

Definition even (x : N.t) := recursion true (fun _ p => negb p) x.

Instance even_wd : Proper (N.eq==>Logic.eq) even.Proper (eq ==> Logic.eq) even
Proof.Proper (eq ==> Logic.eq) even
unfold even.Proper (eq ==> Logic.eq)
  (fun x : t =>
   recursion true (fun (_ : t) (p : bool) => negb p) x) f_equiv'.
Qed.

Theorem even_0 : even 0 = true.even 0 = true
Proof.even 0 = true
unfold even.recursion true (fun (_ : t) (p : bool) => negb p) 0 =
true
now rewrite recursion_0.
Qed.

Theorem even_succ : forall x, even (S x) = negb (even x).forall x : t, even (S x) = negb (even x)
Proof.forall x : t, even (S x) = negb (even x)
unfold even.forall x : t,
recursion true (fun (_ : t) (p : bool) => negb p)
  (S x) =
negb
  (recursion true (fun (_ : t) (p : bool) => negb p) x)
intro x; rewrite recursion_succ; f_equiv'.
Qed.

(*****************************************************)

Division by 2

Definition half_aux (x : N.t) : N.t * N.t :=
  recursion (0, 0) (fun _ p => let (x1, x2) := p in (S x2, x1)) x.

Definition half (x : N.t) := snd (half_aux x).

Instance half_aux_wd : Proper (N.eq ==> N.eq*N.eq) half_aux.Proper (eq ==> eq * eq) half_aux
Proof.Proper (eq ==> eq * eq) half_aux
intros x x' Hx.x, x':t
Hx:x == x'
(eq * eq)%signature (half_aux x) (half_aux x') unfold half_aux.x, x':t
Hx:x == x'
(eq * eq)%signature
  (recursion (0, 0)
     (fun (_ : t) (p : t * t) =>
      let (x1, x2) := p in (S x2, x1)) x)
  (recursion (0, 0)
     (fun (_ : t) (p : t * t) =>
      let (x1, x2) := p in (S x2, x1)) x')
f_equiv; trivial.x, x':t
Hx:x == x'
(eq ==> eq * eq ==> eq * eq)%signature
  (fun (_ : t) (p : t * t) =>
   let (x1, x2) := p in (S x2, x1))
  (fun (_ : t) (p : t * t) =>
   let (x1, x2) := p in (S x2, x1))
intros y y' Hy (u,v) (u',v') (Hu,Hv).x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
u, v, u', v':t
Hu:(eq @@1)%signature (u, v) (u', v')
Hv:(eq @@2)%signature (u, v) (u', v')
(eq * eq)%signature (S v, u) (S v', u') compute in *.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
u, v, u', v':t
Hu:u == u'
Hv:v == v'
S v == S v' /\ u == u'
rewrite Hu, Hv; auto with *.
Qed.

Instance half_wd : Proper (N.eq==>N.eq) half.Proper (eq ==> eq) half
Proof.Proper (eq ==> eq) half
unfold half.Proper (eq ==> eq) (fun x : t => snd (half_aux x)) f_equiv'.
Qed.

Lemma half_aux_0 : half_aux 0 = (0,0).half_aux 0 = (0, 0)
Proof.half_aux 0 = (0, 0)
unfold half_aux.recursion (0, 0)
  (fun (_ : t) (p : t * t) =>
   let (x1, x2) := p in (S x2, x1)) 0 = (0, 0) rewrite recursion_0; auto.
Qed.

Lemma half_aux_succ : forall x,
 half_aux (S x) = (S (snd (half_aux x)), fst (half_aux x)).forall x : t,
half_aux (S x) =
(S (snd (half_aux x)), fst (half_aux x))
Proof.forall x : t,
half_aux (S x) =
(S (snd (half_aux x)), fst (half_aux x))
intros.x:t
half_aux (S x) =
(S (snd (half_aux x)), fst (half_aux x))
remember (half_aux x) as h.x:t
h:(t * t)%type
Heqh:h = half_aux x
half_aux (S x) = (S (snd h), fst h)
destruct h as (f,s); simpl in *.x, f, s:t
Heqh:(f, s) = half_aux x
half_aux (S x) = (S s, f)
unfold half_aux in *.x, f, s:t
Heqh:(f, s) =
recursion (0, 0)
  (fun (_ : t) (p : t * t) =>
   let (x1, x2) := p in (S x2, x1)) x
recursion (0, 0)
  (fun (_ : t) (p : t * t) =>
   let (x1, x2) := p in (S x2, x1)) (S x) = (S s, f)
rewrite recursion_succ, <- Heqh; simpl; f_equiv'.
Qed.

Theorem half_aux_spec : forall n,
 n == fst (half_aux n) + snd (half_aux n).forall n : t, n == fst (half_aux n) + snd (half_aux n)
Proof.forall n : t, n == fst (half_aux n) + snd (half_aux n)
apply induction.Proper (eq ==> iff)
  (fun n : t =>
   n == fst (half_aux n) + snd (half_aux n))
0 == fst (half_aux 0) + snd (half_aux 0)
forall n : t,
n == fst (half_aux n) + snd (half_aux n) ->
S n == fst (half_aux (S n)) + snd (half_aux (S n))
intros x x' Hx.x, x':t
Hx:x == x'
x == fst (half_aux x) + snd (half_aux x) <->
x' == fst (half_aux x') + snd (half_aux x')
0 == fst (half_aux 0) + snd (half_aux 0)
forall n : t,
n == fst (half_aux n) + snd (half_aux n) ->
S n == fst (half_aux (S n)) + snd (half_aux (S n)) setoid_rewrite Hx; auto with *.0 == fst (half_aux 0) + snd (half_aux 0)
forall n : t,
n == fst (half_aux n) + snd (half_aux n) ->
S n == fst (half_aux (S n)) + snd (half_aux (S n))
rewrite half_aux_0; simpl; rewrite add_0_l; auto with *.forall n : t,
n == fst (half_aux n) + snd (half_aux n) ->
S n == fst (half_aux (S n)) + snd (half_aux (S n))
intros.n:t
H:n == fst (half_aux n) + snd (half_aux n)
S n == fst (half_aux (S n)) + snd (half_aux (S n))
rewrite half_aux_succ.n:t
H:n == fst (half_aux n) + snd (half_aux n)
S n ==
fst (S (snd (half_aux n)), fst (half_aux n)) +
snd (S (snd (half_aux n)), fst (half_aux n)) simpl.n:t
H:n == fst (half_aux n) + snd (half_aux n)
S n == S (snd (half_aux n)) + fst (half_aux n)
rewrite add_succ_l, add_comm; auto.n:t
H:n == fst (half_aux n) + snd (half_aux n)
S n == S (fst (half_aux n) + snd (half_aux n))
now f_equiv.
Qed.

Theorem half_aux_spec2 : forall n,
 fst (half_aux n) == snd (half_aux n) \/
 fst (half_aux n) == S (snd (half_aux n)).forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n))
Proof.forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n))
apply induction.Proper (eq ==> iff)
  (fun n : t =>
   fst (half_aux n) == snd (half_aux n) \/
   fst (half_aux n) == S (snd (half_aux n)))
fst (half_aux 0) == snd (half_aux 0) \/
fst (half_aux 0) == S (snd (half_aux 0))
forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n)) ->
fst (half_aux (S n)) == snd (half_aux (S n)) \/
fst (half_aux (S n)) == S (snd (half_aux (S n)))
intros x x' Hx.x, x':t
Hx:x == x'
fst (half_aux x) == snd (half_aux x) \/
fst (half_aux x) == S (snd (half_aux x)) <->
fst (half_aux x') == snd (half_aux x') \/
fst (half_aux x') == S (snd (half_aux x'))
fst (half_aux 0) == snd (half_aux 0) \/
fst (half_aux 0) == S (snd (half_aux 0))
forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n)) ->
fst (half_aux (S n)) == snd (half_aux (S n)) \/
fst (half_aux (S n)) == S (snd (half_aux (S n))) setoid_rewrite Hx; auto with *.fst (half_aux 0) == snd (half_aux 0) \/
fst (half_aux 0) == S (snd (half_aux 0))
forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n)) ->
fst (half_aux (S n)) == snd (half_aux (S n)) \/
fst (half_aux (S n)) == S (snd (half_aux (S n)))
rewrite half_aux_0; simpl.0 == 0 \/ 0 == S 0
forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n)) ->
fst (half_aux (S n)) == snd (half_aux (S n)) \/
fst (half_aux (S n)) == S (snd (half_aux (S n))) auto with *.forall n : t,
fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n)) ->
fst (half_aux (S n)) == snd (half_aux (S n)) \/
fst (half_aux (S n)) == S (snd (half_aux (S n)))
intros.n:t
H:fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n))
fst (half_aux (S n)) == snd (half_aux (S n)) \/
fst (half_aux (S n)) == S (snd (half_aux (S n)))
rewrite half_aux_succ; simpl.n:t
H:fst (half_aux n) == snd (half_aux n) \/
fst (half_aux n) == S (snd (half_aux n))
S (snd (half_aux n)) == fst (half_aux n) \/
S (snd (half_aux n)) == S (fst (half_aux n))
destruct H; auto with *.n:t
H:fst (half_aux n) == snd (half_aux n)
S (snd (half_aux n)) == fst (half_aux n) \/
S (snd (half_aux n)) == S (fst (half_aux n))
right; now f_equiv.
Qed.

Theorem half_0 : half 0 == 0.half 0 == 0
Proof.half 0 == 0
unfold half.snd (half_aux 0) == 0 rewrite half_aux_0; simpl; auto with *.
Qed.

Theorem half_1 : half 1 == 0.half 1 == 0
Proof.half 1 == 0
unfold half.snd (half_aux 1) == 0 rewrite one_succ, half_aux_succ, half_aux_0; simpl; auto with *.
Qed.

Theorem half_double : forall n,
 n == 2 * half n \/ n == 1 + 2 * half n.forall n : t, n == 2 * half n \/ n == 1 + 2 * half n
Proof.forall n : t, n == 2 * half n \/ n == 1 + 2 * half n
intros.n:t
n == 2 * half n \/ n == 1 + 2 * half n unfold half.n:t
n == 2 * snd (half_aux n) \/
n == 1 + 2 * snd (half_aux n)
nzsimpl'.n:t
n == snd (half_aux n) + snd (half_aux n) \/
n == S (snd (half_aux n) + snd (half_aux n))
destruct (half_aux_spec2 n) as [H|H]; [left|right].n:t
H:fst (half_aux n) == snd (half_aux n)
n == snd (half_aux n) + snd (half_aux n)
n:t
H:fst (half_aux n) == S (snd (half_aux n))
n == S (snd (half_aux n) + snd (half_aux n))
rewrite <- H at 1.n:t
H:fst (half_aux n) == snd (half_aux n)
n == fst (half_aux n) + snd (half_aux n)
n:t
H:fst (half_aux n) == S (snd (half_aux n))
n == S (snd (half_aux n) + snd (half_aux n)) apply half_aux_spec.n:t
H:fst (half_aux n) == S (snd (half_aux n))
n == S (snd (half_aux n) + snd (half_aux n))
rewrite <- add_succ_l.n:t
H:fst (half_aux n) == S (snd (half_aux n))
n == S (snd (half_aux n)) + snd (half_aux n) rewrite <- H at 1.n:t
H:fst (half_aux n) == S (snd (half_aux n))
n == fst (half_aux n) + snd (half_aux n) apply half_aux_spec.
Qed.

Theorem half_upper_bound : forall n, 2 * half n <= n.forall n : t, 2 * half n <= n
Proof.forall n : t, 2 * half n <= n
intros.n:t
2 * half n <= n
destruct (half_double n) as [E|E]; rewrite E at 2.n:t
E:n == 2 * half n
2 * half n <= 2 * half n
n:t
E:n == 1 + 2 * half n
2 * half n <= 1 + 2 * half n
apply le_refl.n:t
E:n == 1 + 2 * half n
2 * half n <= 1 + 2 * half n
nzsimpl.n:t
E:n == 1 + 2 * half n
2 * half n <= S (2 * half n)
apply le_le_succ_r, le_refl.
Qed.

Theorem half_lower_bound : forall n, n <= 1 + 2 * half n.forall n : t, n <= 1 + 2 * half n
Proof.forall n : t, n <= 1 + 2 * half n
intros.n:t
n <= 1 + 2 * half n
destruct (half_double n) as [E|E]; rewrite E at 1.n:t
E:n == 2 * half n
2 * half n <= 1 + 2 * half n
n:t
E:n == 1 + 2 * half n
1 + 2 * half n <= 1 + 2 * half n
nzsimpl.n:t
E:n == 2 * half n
2 * half n <= S (2 * half n)
n:t
E:n == 1 + 2 * half n
1 + 2 * half n <= 1 + 2 * half n
apply le_le_succ_r, le_refl.n:t
E:n == 1 + 2 * half n
1 + 2 * half n <= 1 + 2 * half n
apply le_refl.
Qed.

Theorem half_nz : forall n, 1 < n -> 0 < half n.forall n : t, 1 < n -> 0 < half n
Proof.forall n : t, 1 < n -> 0 < half n
intros n LT.n:t
LT:1 < n
0 < half n
assert (LE : 0 <= half n) by apply le_0_l.n:t
LT:1 < n
LE:0 <= half n
0 < half n
le_elim LE; auto.n:t
LT:1 < n
LE:0 == half n
0 < half n
destruct (half_double n) as [E|E];
 rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT.n:t
LT:1 < 0
LE:0 == half n
E:n == 0
0 < half n
n:t
LT:1 < 1
LE:0 == half n
E:n == 1
0 < half n
order'.n:t
LT:1 < 1
LE:0 == half n
E:n == 1
0 < half n
order.
Qed.

Theorem half_decrease : forall n, 0 < n -> half n < n.forall n : t, 0 < n -> half n < n
Proof.forall n : t, 0 < n -> half n < n
intros n LT.n:t
LT:0 < n
half n < n
destruct (half_double n) as [E|E]; rewrite E at 2; nzsimpl'.n:t
LT:0 < n
E:n == 2 * half n
half n < half n + half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n)
rewrite <- add_0_l at 1.n:t
LT:0 < n
E:n == 2 * half n
0 + half n < half n + half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n)
rewrite <- add_lt_mono_r.n:t
LT:0 < n
E:n == 2 * half n
0 < half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n)
assert (LE : 0 <= half n) by apply le_0_l.n:t
LT:0 < n
E:n == 2 * half n
LE:0 <= half n
0 < half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n)
le_elim LE; auto.n:t
LT:0 < n
E:n == 2 * half n
LE:0 == half n
0 < half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n)
rewrite <- LE, mul_0_r in E.n:t
LT:0 < n
E:n == 0
LE:0 == half n
0 < half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n) rewrite E in LT.n:t
LT:0 < 0
E:n == 0
LE:0 == half n
0 < half n
n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n) destruct (nlt_0_r _ LT).n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n + half n)
rewrite <- add_succ_l.n:t
LT:0 < n
E:n == 1 + 2 * half n
half n < S (half n) + half n
rewrite <- add_0_l at 1.n:t
LT:0 < n
E:n == 1 + 2 * half n
0 + half n < S (half n) + half n
rewrite <- add_lt_mono_r.n:t
LT:0 < n
E:n == 1 + 2 * half n
0 < S (half n)
apply lt_0_succ.
Qed.


(*****************************************************)

Power

Definition pow (n m : N.t) := recursion 1 (fun _ r => n*r) m.

Local Infix "^^" := pow (at level 30, right associativity).

Instance pow_wd : Proper (N.eq==>N.eq==>N.eq) pow.Proper (eq ==> eq ==> eq) pow
Proof.Proper (eq ==> eq ==> eq) pow
unfold pow.Proper (eq ==> eq ==> eq)
  (fun n m : t => recursion 1 (fun _ r : t => n * r) m) f_equiv'.
Qed.

Lemma pow_0 : forall n, n^^0 == 1.forall n : t, n ^^ 0 == 1
Proof.forall n : t, n ^^ 0 == 1
intros.n:t
n ^^ 0 == 1 unfold pow.n:t
recursion 1 (fun _ r : t => n * r) 0 == 1 rewrite recursion_0.n:t
1 == 1 auto with *.
Qed.

Lemma pow_succ : forall n m, n^^(S m) == n*(n^^m).forall n m : t, n ^^ S m == n * n ^^ m
Proof.forall n m : t, n ^^ S m == n * n ^^ m
intros.n, m:t
n ^^ S m == n * n ^^ m unfold pow.n, m:t
recursion 1 (fun _ r : t => n * r) (S m) ==
n * recursion 1 (fun _ r : t => n * r) m rewrite recursion_succ; f_equiv'.
Qed.


(*****************************************************)

Logarithm for the base 2

Definition log (x : N.t) : N.t :=
strong_rec 0
           (fun g x =>
              if x << 2 then 0
              else S (g (half x)))
           x.

Instance log_prewd :
 Proper ((N.eq==>N.eq)==>N.eq==>N.eq)
   (fun g x => if x<<2 then 0 else S (g (half x))).Proper ((eq ==> eq) ==> eq ==> eq)
  (fun (g : t -> t) (x : t) =>
   if x << 2 then 0 else S (g (half x)))
Proof.Proper ((eq ==> eq) ==> eq ==> eq)
  (fun (g : t -> t) (x : t) =>
   if x << 2 then 0 else S (g (half x)))
intros g g' Hg n n' Hn.g, g':t -> t
Hg:(eq ==> eq)%signature g g'
n, n':t
Hn:n == n'
(if n << 2 then 0 else S (g (half n))) ==
(if n' << 2 then 0 else S (g' (half n')))
rewrite Hn.g, g':t -> t
Hg:(eq ==> eq)%signature g g'
n, n':t
Hn:n == n'
(if n' << 2 then 0 else S (g (half n))) ==
(if n' << 2 then 0 else S (g' (half n')))
destruct (n' << 2); auto with *.g, g':t -> t
Hg:(eq ==> eq)%signature g g'
n, n':t
Hn:n == n'
S (g (half n)) == S (g' (half n'))
f_equiv.g, g':t -> t
Hg:(eq ==> eq)%signature g g'
n, n':t
Hn:n == n'
g (half n) == g' (half n') apply Hg.g, g':t -> t
Hg:(eq ==> eq)%signature g g'
n, n':t
Hn:n == n'
half n == half n' now f_equiv.
Qed.

Instance log_wd : Proper (N.eq==>N.eq) log.Proper (eq ==> eq) log
Proof.Proper (eq ==> eq) log
intros x x' Exx'.x, x':t
Exx':x == x'
log x == log x' unfold log.x, x':t
Exx':x == x'
strong_rec 0
  (fun (g : t -> t) (x0 : t) =>
   if x0 << 2 then 0 else S (g (half x0))) x ==
strong_rec 0
  (fun (g : t -> t) (x0 : t) =>
   if x0 << 2 then 0 else S (g (half x0))) x'
apply strong_rec_wd; f_equiv'.
Qed.

Lemma log_good_step : forall n h1 h2,
 (forall m, m < n -> h1 m == h2 m) ->
  (if n << 2 then 0 else S (h1 (half n))) ==
  (if n << 2 then 0 else S (h2 (half n))).forall (n : t) (h1 h2 : t -> t),
(forall m : t, m < n -> h1 m == h2 m) ->
(if n << 2 then 0 else S (h1 (half n))) ==
(if n << 2 then 0 else S (h2 (half n)))
Proof.forall (n : t) (h1 h2 : t -> t),
(forall m : t, m < n -> h1 m == h2 m) ->
(if n << 2 then 0 else S (h1 (half n))) ==
(if n << 2 then 0 else S (h2 (half n)))
intros n h1 h2 E.n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
(if n << 2 then 0 else S (h1 (half n))) ==
(if n << 2 then 0 else S (h2 (half n)))
destruct (n<<2) eqn:H.n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
H:(n << 2) = true
0 == 0
n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
H:(n << 2) = false
S (h1 (half n)) == S (h2 (half n))
auto with *.n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
H:(n << 2) = false
S (h1 (half n)) == S (h2 (half n))
f_equiv.n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
H:(n << 2) = false
h1 (half n) == h2 (half n) apply E, half_decrease.n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
H:(n << 2) = false
0 < n
rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.n:t
h1, h2:t -> t
E:forall m : t, m < n -> h1 m == h2 m
H:1 < n
0 < n
order'.
Qed.
Hint Resolve log_good_step : core.

Theorem log_init : forall n, n < 2 -> log n == 0.forall n : t, n < 2 -> log n == 0
Proof.forall n : t, n < 2 -> log n == 0
intros n Hn.n:t
Hn:n < 2
log n == 0 unfold log.n:t
Hn:n < 2
strong_rec 0
  (fun (g : t -> t) (x : t) =>
   if x << 2 then 0 else S (g (half x))) n == 0 rewrite strong_rec_fixpoint; auto with *.n:t
Hn:n < 2
(if n << 2
 then 0
 else
  S
    (strong_rec 0
       (fun (g : t -> t) (x : t) =>
        if x << 2 then 0 else S (g (half x))) (half n))) ==
0
replace (n << 2) with true; auto with *.n:t
Hn:n < 2
true = (n << 2)
symmetry.n:t
Hn:n < 2
(n << 2) = true now rewrite ltb_lt.
Qed.

Theorem log_step : forall n, 2 <= n -> log n == S (log (half n)).forall n : t, 2 <= n -> log n == S (log (half n))
Proof.forall n : t, 2 <= n -> log n == S (log (half n))
intros n Hn.n:t
Hn:2 <= n
log n == S (log (half n)) unfold log.n:t
Hn:2 <= n
strong_rec 0
  (fun (g : t -> t) (x : t) =>
   if x << 2 then 0 else S (g (half x))) n ==
S
  (strong_rec 0
     (fun (g : t -> t) (x : t) =>
      if x << 2 then 0 else S (g (half x))) (half n)) rewrite strong_rec_fixpoint; auto with *.n:t
Hn:2 <= n
(if n << 2
 then 0
 else
  S
    (strong_rec 0
       (fun (g : t -> t) (x : t) =>
        if x << 2 then 0 else S (g (half x))) (half n))) ==
S
  (strong_rec 0
     (fun (g : t -> t) (x : t) =>
      if x << 2 then 0 else S (g (half x))) (half n))
replace (n << 2) with false; auto with *.n:t
Hn:2 <= n
false = (n << 2)
symmetry.n:t
Hn:2 <= n
(n << 2) = false rewrite <- not_true_iff_false, ltb_lt, nlt_ge; auto.
Qed.

Theorem pow2_log : forall n, 0 < n -> half n < 2^^(log n) <= n.forall n : t, 0 < n -> half n < 2 ^^ log n <= n
Proof.forall n : t, 0 < n -> half n < 2 ^^ log n <= n
intro n; generalize (le_refl n).n:t
n <= n -> 0 < n -> half n < 2 ^^ log n <= n set (k:=n) at -2.n:t
k:=n:t
k <= n -> 0 < k -> half k < 2 ^^ log k <= k clearbody k.n, k:t
k <= n -> 0 < k -> half k < 2 ^^ log k <= k
revert k.n:t
forall k : t,
k <= n -> 0 < k -> half k < 2 ^^ log k <= k pattern n.n:t
(fun t0 : t =>
 forall k : t,
 k <= t0 -> 0 < k -> half k < 2 ^^ log k <= k) n apply induction; clear n.Proper (eq ==> iff)
  (fun t0 : t =>
   forall k : t,
   k <= t0 -> 0 < k -> half k < 2 ^^ log k <= k)
forall k : t,
k <= 0 -> 0 < k -> half k < 2 ^^ log k <= k
forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k
intros n n' Hn; setoid_rewrite Hn; auto with *.forall k : t,
k <= 0 -> 0 < k -> half k < 2 ^^ log k <= k
forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k
intros k Hk1 Hk2.k:t
Hk1:k <= 0
Hk2:0 < k
half k < 2 ^^ log k <= k
forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k
 le_elim Hk1.k:t
Hk1:k < 0
Hk2:0 < k
half k < 2 ^^ log k <= k
k:t
Hk1:k == 0
Hk2:0 < k
half k < 2 ^^ log k <= k
forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k destruct (nlt_0_r _ Hk1).k:t
Hk1:k == 0
Hk2:0 < k
half k < 2 ^^ log k <= k
forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k
 rewrite Hk1 in Hk2.k:t
Hk1:k == 0
Hk2:0 < 0
half k < 2 ^^ log k <= k
forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k destruct (nlt_0_r _ Hk2).forall n : t,
(forall k : t,
 k <= n -> 0 < k -> half k < 2 ^^ log k <= k) ->
forall k : t,
k <= S n -> 0 < k -> half k < 2 ^^ log k <= k

intros n IH k Hk1 Hk2.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
half k < 2 ^^ log k <= k
destruct (lt_ge_cases k 2) as [LT|LE].n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LT:k < 2
half k < 2 ^^ log k <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
(* base *)
rewrite log_init, pow_0 by auto.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LT:k < 2
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
rewrite <- le_succ_l, <- one_succ in Hk2.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 <= k
LT:k < 2
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
le_elim Hk2.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 < k
LT:k < 2
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 == k
LT:k < 2
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
rewrite two_succ, <- nle_gt, le_succ_l in LT.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 < k
LT:~ 1 < k
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 == k
LT:k < 2
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k destruct LT; auto.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 == k
LT:k < 2
half k < 1 <= k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
rewrite <- Hk2.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:1 == k
LT:k < 2
half 1 < 1 <= 1
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
rewrite half_1; auto using lt_0_1, le_refl.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 ^^ log k <= k
(* step *)
rewrite log_step, pow_succ by auto.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:2 <= k
half k < 2 * 2 ^^ log (half k) <= k
rewrite two_succ, le_succ_l in LE.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
half k < 2 * 2 ^^ log (half k) <= k
destruct (IH (half k)) as (IH1,IH2).n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
half k <= n
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
0 < half k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
IH1:half (half k) < 2 ^^ log (half k)
IH2:2 ^^ log (half k) <= half k
half k < 2 * 2 ^^ log (half k) <= k
 rewrite <- lt_succ_r.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
half k < S n
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
0 < half k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
IH1:half (half k) < 2 ^^ log (half k)
IH2:2 ^^ log (half k) <= half k
half k < 2 * 2 ^^ log (half k) <= k apply lt_le_trans with k; auto.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
half k < k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
0 < half k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
IH1:half (half k) < 2 ^^ log (half k)
IH2:2 ^^ log (half k) <= half k
half k < 2 * 2 ^^ log (half k) <= k
  now apply half_decrease.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
0 < half k
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
IH1:half (half k) < 2 ^^ log (half k)
IH2:2 ^^ log (half k) <= half k
half k < 2 * 2 ^^ log (half k) <= k
 apply half_nz; auto.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
IH1:half (half k) < 2 ^^ log (half k)
IH2:2 ^^ log (half k) <= half k
half k < 2 * 2 ^^ log (half k) <= k
set (K:=2^^log (half k)) in *; clearbody K.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
half k < 2 * K <= k
split.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
half k < 2 * K
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
rewrite <- le_succ_l in IH1.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:S (half (half k)) <= K
IH2:K <= half k
half k < 2 * K
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
apply mul_le_mono_l with (p:=2) in IH1.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:2 * S (half (half k)) <= 2 * K
IH2:K <= half k
half k < 2 * K
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
eapply lt_le_trans; eauto.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:2 * S (half (half k)) <= 2 * K
IH2:K <= half k
half k < 2 * S (half (half k))
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
nzsimpl'.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:2 * S (half (half k)) <= 2 * K
IH2:K <= half k
half k < S (S (half (half k) + half (half k)))
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
rewrite lt_succ_r.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:2 * S (half (half k)) <= 2 * K
IH2:K <= half k
half k <= S (half (half k) + half (half k))
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
eapply le_trans; [ eapply half_lower_bound | ].n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:2 * S (half (half k)) <= 2 * K
IH2:K <= half k
1 + 2 * half (half k) <=
S (half (half k) + half (half k))
n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
nzsimpl'; apply le_refl.n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= k
eapply le_trans; [ | eapply half_upper_bound ].n:t
IH:forall k0 : t,
k0 <= n -> 0 < k0 -> half k0 < 2 ^^ log k0 <= k0
k:t
Hk1:k <= S n
Hk2:0 < k
LE:1 < k
K:t
IH1:half (half k) < K
IH2:K <= half k
2 * K <= 2 * half k
apply mul_le_mono_l; auto.
Qed.

End NdefOpsProp.