coq - 逻辑：evenb_double_conv

Question

Theorem evenb_double_conv : forall n,
  exists k, n = if evenb n then double k
                else S (double k).
Proof.
  (* Hint: Use the [evenb_S] lemma from [Induction.v]. *)
  intros n. induction n as [|n' IHn'].
  - simpl. exists O. simpl. reflexivity.
  - rewrite -> evenb_S. destruct (evenb n') as [H1 | H2].
    + simpl.

我在这里卡住了：

n' : nat
IHn' : exists k : nat, n' = double k
============================
exists k : nat, S n' = S (double k)

我们可以使用归纳假设将 (double k) 重写为 n'，也可以对目标使用注入，然后应用归纳假设。

但我不能做这些，因为exists。

rewrite <- IHn'给出：

错误：找不到要重写的同类关系。

injection给出：

错误：Ltac 调用“注入”失败。不是否定的原始平等。

该怎么办？

Answer 1

我们需要exists用 destruct 打破假设：destruct IHn' as [k HE].

Theorem evenb_double_conv : forall n,
  exists k, n = if evenb n then double k
                else S (double k).
Proof.
  (* Hint: Use the [evenb_S] lemma from [Induction.v]. *)
  intros n. induction n as [|n' IHn'].
  - simpl. exists O. simpl. reflexivity.
  - rewrite -> evenb_S. destruct IHn' as [k HE].  destruct (evenb n').
    (* Now find out which k we need to insert into the goal for every branch *)

注入在这里不起作用，因为它只在假设中起作用。