Where did lt_index go?

Link:: https://stackoverflow.com/q/38755038

Display all goals and responses

Question

I was using a lemma named lt_index in Coq, I remember it states that

n < 2 * m + 1 -> (n - 1) / 2 < m

Now, I can't use this lemma anymore, and when I do SearchAbout lt_index, coq answers with

Error: The reference lt_index was not found in the current environment.

My imports are as follows

Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Arith.

Did I miss something?

EDIT: Apparently, I dreamed about this lt_index lemma and never existed. Anyway, I came up with a proof to the same result, I added 1 <= n as precondition. Here it is

Lemma lt_solve : forall (n m : nat),
    1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m.forall n m : nat,
1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m
Proof.forall n m : nat,
1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m
  intros.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
(n - 1) / 2 < m assert (n <= n - 1 + 1).n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
n <= n - 1 + 1
n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
(n - 1) / 2 < m
  -n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
n <= n - 1 + 1 apply Nat.sub_add_le.
  -n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
(n - 1) / 2 < m inversion H1.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
(n - 1 + 1 - 1) / 2 < m
n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = n - 1 + 1
(n - 1) / 2 < m
    +n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
(n - 1 + 1 - 1) / 2 < m rewrite <-H2.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
(n - 1) / 2 < m rewrite H2 in H0.n, m: nat
H: 1 <= n
H0: n - 1 + 1 < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
(n - 1) / 2 < m
      rewrite plus_comm in H0.n, m: nat
H: 1 <= n
H0: 1 + (n - 1) < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
(n - 1) / 2 < m assert (2 * m + 1 = 1 + 2 * m).n, m: nat
H: 1 <= n
H0: 1 + (n - 1) < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
2 * m + 1 = 1 + 2 * m
n, m: nat
H: 1 <= n
H0: 1 + (n - 1) < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
(n - 1) / 2 < m
      *n, m: nat
H: 1 <= n
H0: 1 + (n - 1) < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
2 * m + 1 = 1 + 2 * m apply plus_comm.
      *n, m: nat
H: 1 <= n
H0: 1 + (n - 1) < 2 * m + 1
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
(n - 1) / 2 < m rewrite H3 in H0.n, m: nat
H: 1 <= n
H0: 1 + (n - 1) < 1 + 2 * m
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
(n - 1) / 2 < m apply plus_lt_reg_l in H0.n, m: nat
H: 1 <= n
H0: n - 1 < 2 * m
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
(n - 1) / 2 < m
        apply Nat.div_lt_upper_bound in H0.n, m: nat
H: 1 <= n
H0: (n - 1) / 2 < m
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
(n - 1) / 2 < m
n, m: nat
H: 1 <= n
H0: n - 1 < 2 * m
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
2 <> 0
        --n, m: nat
H: 1 <= n
H0: (n - 1) / 2 < m
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
(n - 1) / 2 < m trivial.
        --n, m: nat
H: 1 <= n
H0: n - 1 < 2 * m
H1: n <= n - 1 + 1
H2: n = n - 1 + 1
H3: 2 * m + 1 = 1 + 2 * m
2 <> 0 discriminate.
    +n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = n - 1 + 1
(n - 1) / 2 < m rewrite plus_comm in H2.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = 1 + (n - 1)
(n - 1) / 2 < m
      rewrite (le_plus_minus_r 1 n) in H2.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = n
(n - 1) / 2 < m
n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = 1 + (n - 1)
1 <= n
      *n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = n
(n - 1) / 2 < m eapply (le_lt_trans n m0 (S m0)) in H3.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n < S m0
H2: S m0 = n
(n - 1) / 2 < m
n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = n
m0 < S m0
        --n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n < S m0
H2: S m0 = n
(n - 1) / 2 < m rewrite H2 in H3.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n < n
H2: S m0 = n
(n - 1) / 2 < m contradict H3.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H2: S m0 = n
~ n < n apply lt_irrefl.
        --n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = n
m0 < S m0 apply lt_n_Sn.
      *n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
H1: n <= n - 1 + 1
m0: nat
H3: n <= m0
H2: S m0 = 1 + (n - 1)
1 <= n trivial.
Qed.

If you realize there is an improvement to this proof, I'd be glad to hear about it.

Answer (larsr)

While it is good to try to solve these kinds of problems by hand as an exercise, in the long run it can get tedious, if you really want to work on something else.

There are tactics that can help you to solve systems of equations with inequalities. You can for instance use the tactics lia from Psatz, or omega from Omega. The proof terms are not a pretty sight, but if that doesn't matter then why not.

Unfortunately they don't handle division, so they can't solve this system, but there is a lemma in the library that you can use to get rid of the /. I found it by doing Search ( _ / _ < _ ).

Require Import Coq.Numbers.Natural.Peano.NPeano.
(* this provides 'lia' for solving linear integer arithmetic *)
Require Import Psatz.

Lemma lt_solve : forall (n m : nat),
    1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m.forall n m : nat,
1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m
Proof.forall n m : nat,
1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m
  intros.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
(n - 1) / 2 < m apply Nat.div_lt_upper_bound; lia.
Qed.

Answer (Anton Trunov)

If you for some reason would like to get a "manual" solution, using the standard library, then here it is.

Require Import Coq.Arith.Arith.

Lemma lt_solve : forall (n m : nat),
    1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m.forall n m : nat,
1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m
Proof with auto.forall n m : nat,
1 <= n -> n < 2 * m + 1 -> (n - 1) / 2 < m
  intros.n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
(n - 1) / 2 < m apply Nat.div_lt_upper_bound...n, m: nat
H: 1 <= n
H0: n < 2 * m + 1
n - 1 < 2 * m destruct n.m: nat
H: 1 <= 0
H0: 0 < 2 * m + 1
0 - 1 < 2 * m
n, m: nat
H: 1 <= S n
H0: S n < 2 * m + 1
S n - 1 < 2 * m
  -m: nat
H: 1 <= 0
H0: 0 < 2 * m + 1
0 - 1 < 2 * m inversion H.
  -n, m: nat
H: 1 <= S n
H0: S n < 2 * m + 1
S n - 1 < 2 * m rewrite Nat.sub_succ, Nat.sub_0_r, (Nat.add_lt_mono_r _ _ 1).n, m: nat
H: 1 <= S n
H0: S n < 2 * m + 1
n + 1 < 2 * m + 1
    rewrite Nat.add_1_r...
Qed.

Q: Thanks @Anton, one question: why did you add Proof with auto at the very beginning of your proof? What is the role of with auto?

A: It's just a shortcut. The construction Proof with <tactic> works as follows. When you see ellipsis (...) ending a tactic t1, it's equivalent to turning it into t1; <tactic>. So rewrite Nat.add_1_r... behaves as rewrite Nat.add_1_r; auto.