How to prove the inductive step in coq?

2
votes

Coq beginner here, I recently went by myself through the first 7 chapters of "Logical Foundations".

I am trying to create a proof by induction in Coq of ∀ n>= 3, 2n+1 < 2^n.

I start with destruct removing the false hypotheses until reaching n=3. Then, I do induction on n, the case for n=3 is trivial but, how can I prove the inductive step??

I can see the goal holds. I can prove it by case analysis using destruct but, haven't been able to show it in a general form.

The functions I'm using are from "Logical Foundations" and can be seen here.

My proof so far:

(* n>=3, 2n+1 < 2^n *)
Theorem two_n_plus_one_leq_three_lt_wo_pow_n : forall n:nat,
    (blt_nat (two_n_plus_one n) (exp 2 n)) = true
       -> (bge_nat n 3) = true.   
Proof.
  intros n.
  destruct n.
  (* n = 0 *)
  compute.
  intros H.
  inversion H.

  destruct n.
  (* n = 1 *)
  compute.
  intros H.
  inversion H.  

  destruct n.
  (* n = 2 *)
  compute.
  intros H.
  inversion H.

  induction n as [ | k IHk].
  (* n = 3 *)
  - compute.
    reflexivity.
  - rewrite <- IHk.
    (* Inductive step... *)
2
coqinduction
It's not clear what you are trying to prove exactly. Proving n>= 3, 2n+1 < 2^n does not make any sense. According to the Coq code, you want to prove 2n+1 < 2^n -> n >=3. Shouldn't it be the other way around? – eponier
Just thought it might be worth mentioning that you can do all those destruct n's in one step if you do intros [|[|[|n]]]. Then based on what you've already written, intros [|[|[|n]]]; try (compute; intro H; inversion H). should be able to create and then immediately clear the n=0,1,2 cases. – tlon

2 Answers

1
votes

Well, as this is homework I cannot help you a lot. Just let me write down the lemma you pose in math-comp, which already allows for the use of a sane notation:

Theorem two_n_plus_one_leq_three_lt_wo_pow_n n :
  2*n.+1 < 2^n -> 3 <= n.
1
votes

The important part missing was making the inductive hypothesis general. I was able to complete the proof using generalize dependent k..

So the proof looks like this:

(* n ≥ 3, 2n + 1 < 2^n *)
Theorem two_n_plus_one_leq_three_lt_wo_pow_n : forall n:nat,
    (blt_nat (two_n_plus_one n) (exp 2 n)) = true
       -> (bge_nat n 3) = true.
Proof.
  intros n.
  destruct n.
  (* n = 0 *)
  compute.
  intros HF. (* Discard the cases where n is not >= 3 *)
  inversion HF.

  destruct n.
  (* n = 1 *)
  compute.
  intros HF.
  inversion HF.

  destruct n.
  (* n = 2 *)
  compute.
  intros HF.
  inversion HF.

  induction n as [ | k IHk].
  (* n = 3 *)
  - compute.
    reflexivity.
  (* n+1 inductive step *)
  - generalize dependent k.
    intros.
    compute.
    reflexivity.
Qed.