Как доказать индуктивный шаг в coq?

Question

Coq новичок здесь, я недавно прошел самостоятельно через первые 7 глав " Логические основы ".

Я пытаюсь создать доказательство по индукциив Coq ∀ n>= 3, 2n+1 < 2^n.

я начинаю с destruct, удаляя ложные гипотезы, пока не достигну n = 3 .Затем я делаю индукцию на n , случай для n = 3 тривиален, но, как я могу доказать индуктивный шаг ??

Я вижу, как цель держится.Я могу доказать это с помощью анализа кейсов, используя destruct, но не смог показать его в общем виде.

Используемые мной функции из " Logical Foundations"и можно увидеть здесь .

Мои доказательства пока:

(* 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... *)

Answer 1

Важная часть, которая отсутствовала, делала индуктивную гипотезу общей. Я смог завершить доказательство, используя generalize dependent k..

Итак, доказательство выглядит так:

(* 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.

Answer 2

Ну, так как это домашняя работа, я не могу вам чем-то помочь. Просто позвольте мне записать лемму, которую вы ставите в математике, которая уже позволяет использовать нормальную запись:

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