Require Import Recdef.

From Typonomikon Require Import D1b.

Module MyNat.

Export D1b.MyNat.

Notation "n <= m" := (le n m).

Lemma le_0_l :
  forall n : nat, 0 <= n.

Lemma le_n_Sm :
  forall n m : nat, n <= m -> n <= S m.

Lemma le_Sn_m :
  forall n m : nat, S n <= m -> n <= m.

Lemma le_n_S :
  forall n m : nat, n <= m -> S n <= S m.

Lemma le_S_n :
  forall n m : nat, S n <= S m -> n <= m.

Lemma le_Sn_n :
  forall n : nat, ~ S n <= n.

Lemma le_refl :
  forall n : nat, n <= n.

Lemma le_trans :
  forall a b c : nat,
    a <= b -> b <= c -> a <= c.

Lemma le_antisym :
  forall n m : nat,
    n <= m -> m <= n -> n = m.

Lemma le_pred :
  forall n : nat, pred n <= n.

Lemma le_n_pred :
  forall n m : nat,
    n <= m -> pred n <= pred m.

Lemma no_le_pred_n :
  ~ forall n m : nat,
      pred n <= pred m -> n <= m.

Lemma le_add_l :
  forall a b c : nat,
    b <= c -> add a b <= add a c.

Lemma le_add_r :
  forall a b c : nat,
    a <= b -> add a c <= add b c.

Lemma le_add :
  forall a b c d : nat,
    a <= b -> c <= d -> add a c <= add b d.

Lemma le_sub_S_S :
  forall n m : nat,
    sub n (S m) <= sub n m.

Lemma le_sub_l :
  forall a b c : nat,
    b <= c -> sub a c <= sub a b.

Lemma le_sub_r :
  forall a b c : nat,
    a <= b -> sub a c <= sub b c.

Lemma le_mul_l :
  forall a b c : nat,
    b <= c -> mul a b <= mul a c.

Lemma le_mul_r :
  forall a b c : nat,
    a <= b -> mul a c <= mul b c.

Lemma le_mul :
  forall a b c d : nat,
    a <= b -> c <= d -> mul a c <= mul b d.

Lemma le_add_exists :
  forall n m : nat,
    n <= m -> exists k : nat, add n k = m.

Lemma le_pow_l :
  forall a b c : nat,
    a <> 0 -> b <= c -> pow a b <= pow a c.

Lemma le_pow_r :
  forall a b c : nat,
    a <= b -> pow a c <= pow b c.

Lemma sub'_0 :
  forall n m : nat,
    sub' n m = 0 -> n <= m.

Lemma sub'_S_l :
  forall n m : nat,
    m <= n -> sub' (S n) m = S (sub' n m).

Lemma le_sub'_l :
  forall n m : nat,
    sub' n m <= n.

Lemma sub'_inv :
  forall n m : nat,
    m <= n -> sub' n (sub' n m) = m.

Lemma min_le :
  forall n m : nat, n <= m -> min n m = n.

Lemma max_le :
  forall n m : nat, n <= m -> max n m = m.

Lemma sub_le_0 :
  forall n m : nat,
    n <= m -> sub n m = 0.

Lemma sub_sub_r :
  forall n m : nat,
    n <= m -> sub n (sub n m) = n.

Lemma sub_sub_r' :
  forall n m : nat,
    m <= n -> sub n (sub n m) = m.

Definition lt (n m : nat) : Prop := S n <= m.

Notation "n < m" := (lt n m).

Lemma lt_irrefl :
  forall n : nat, ~ n < n.

Lemma lt_trans :
  forall a b c : nat, a < b -> b < c -> a < c.

Lemma lt_asym :
  forall n m : nat, n < m -> ~ m < n.

Definition divides (k n : nat) : Prop :=
  exists m : nat, mul k m = n.

Lemma divides_0 :
  forall n : nat, divides n 0.

Lemma not_divides_0 :
  forall n : nat, n <> 0 -> ~ divides 0 n.

Lemma divides_1 :
  forall n : nat, divides 1 n.

Lemma divides_refl :
  forall n : nat, divides n n.

Lemma divides_trans :
  forall k n m : nat, divides k n -> divides n m -> divides k m.

Lemma divides_add :
  forall k n m : nat, divides k n -> divides k m -> divides k (add n m).

Lemma divides_mul_l :
  forall k n m : nat,
    divides k n -> divides k (mul n m).

Lemma divides_mul_r :
  forall k n m : nat,
    divides k m -> divides k (mul n m).

Lemma divides_le :
  ~ forall k n : nat, divides k n -> k <= n.

Definition prime (p : nat) : Prop :=
  forall k : nat, divides k p -> k = 1 \/ k = p.

Lemma double_not_prime :
  forall n : nat,
    n <> 1 -> ~ prime (mul 2 n).

Definition le' (n m : nat) : Prop :=
  exists k : nat, add k n = m.

Lemma le'_le :
  forall n m : nat,
    n <= m -> le' n m.

Lemma le_le' :
  forall n m : nat,
    le' n m -> n <= m.

Inductive divides' (n : nat) : nat -> Prop :=
| divides'_0 : divides' n 0
| divides'_add : forall m : nat, divides' n m -> divides' n (add n m).

Lemma divides_divides' :
  forall n m : nat,
    divides' n m -> divides n m.

Lemma divides'_divides :
  forall n m : nat,
    divides n m -> divides' n m.

Lemma leb_n :
  forall n : nat,
    leb n n = true.

Lemma leb_spec :
  forall n m : nat,
    n <= m <-> leb n m = true.

Lemma eqb_spec :
  forall n m : nat,
    n = m <-> eqb n m = true.

Lemma le_1_fac :
  forall n : nat, 1 <= fac n.

Lemma le_lin_fac :
  forall n : nat, n <= fac n.

Notation "4" := (S (S (S (S 0)))).

Lemma le_exp_fac :
  forall n : nat, 4 <= n -> pow 2 n <= fac n.

Lemma binom_spec :
  forall n k : nat,
    k <= n -> mul (fac k) (mul (fac (sub' n k)) (binom n k)) = fac n.

End MyNat.

Require Import Lia Arith.

Fixpoint root (n : nat) :=
match n with
| 0 => 0
| S n' =>
    let r := root n' in
      if Nat.ltb n (S r * S r)
      then r
      else S r
end.

Compute root 50.

Lemma root_spec :
  forall (n : nat) (r := root n),
    r * r <= n < (S r) * (S r).
Proof.
  induction n as [| n']; [now cbn; lia |].
  destruct IHn' as [H1 H2].
  cbn [root].
  now destruct (Nat.ltb_spec (S n') (S (root n') * S (root n'))); lia.
Qed.

Lemma le_diag_inv :
  forall n m : nat,
    n * n <= m * m -> n <= m.
Proof.
  intros n m Hle.
  apply Decidable.not_not; [admit |].
  intros Hlt.
  rewrite <- Nat.lt_nge in Hlt.
  assert (m * m < n * n).
  {
    now apply Nat.square_lt_mono_nonneg; [lia |].
  }
  lia.
Admitted.

Lemma lt_diag_inv :
  forall n m : nat,
    n * n < m * m -> n < m.
Proof.
  intros n m Hlt.
  apply Decidable.not_not; [admit |].
  intros Hle.
  rewrite <- Nat.le_ngt in Hle.
  assert (m * m <= n * n).
  {
    now apply Nat.square_le_mono_nonneg; [lia |].
  }
  lia.
Admitted.

Lemma root_spec' :
  forall (n : nat) (r := root (n * n)),
    r = n.
Proof.
  intros n r.
  pose proof (Hspec := root_spec (n * n)).
  assert (Hle : r <= n) by apply le_diag_inv, Hspec.
  assert (Hlt : n < S r) by apply lt_diag_inv, Hspec.
  lia.
Qed.

Section reverse.

Context
  (f : nat -> nat)
  (Hzero : f 0 = 0)
  (Hincreasing : forall m n, m < n -> f m < f n).

End reverse.