Логика: evenb_double_conv - PullRequest
Новая
       76

Логика: evenb_double_conv

0 голосов
/ 05 мая 2019 
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 для «инъекции».Не отрицание примитивного равенства.

Что делать?

1 Ответ

0 голосов
/ 05 мая 2019

Нам нужно разбить 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 *)

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

...