Логика: 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 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 *)

Инъекция здесь не работает, потому что она работает только в гипотезе.