even_Sn_not_even_n - применить одну гипотезу в другой - PullRequest
Новая
       25

even_Sn_not_even_n - применить одну гипотезу в другой

1 голос
/ 29 мая 2019

К сожалению, я снова застрял: 

Inductive even : nat > Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).
Proof.
  intros n. split.
  + intros H. unfold not. intros H1. induction H1 as [|n' E' IHn].
    - inversion H.
    - inversion_clear H. apply IHn in H0. apply H0.
  + intros H. induction n as [|n' IHn].
    - exfalso. apply H. apply ev_0.
    - apply evSS_inv'.

Вот результат: 

1 subgoal (ID 179)

n' : nat
H : ~ even (S n')
IHn : ~ even n' -> even (S n')
============================
even n'

Насколько я мог доказать это словами:

(n '+ 1) даже не согласно H. Следовательно, согласно IHn, неверно, что n 'не является четным (двойное отрицание): 

IHn : ~ ~ even n'

Разворачивая двойное отрицание, мы заключаем, что n' является четным.

Но как написать это в coq?

1 Ответ

2 голосов
/ 29 мая 2019

Обычный способ избавиться от двойного отрицания состоит в том, чтобы ввести аксиому «исключенная средняя», которая определяется под названием classic в Coq.Logic.Classical_Prop, и применить лемму NNPP.

Однако, в этом конкретном случае, вы можете использовать технику, названную отражением , показав, что Опора соответствует булевой функции (вы, возможно, помните функцию evenb, представленную ранее в книге).

(Предполагая, что вы находитесь в начале IndProp). В этой главе вы вскоре увидите следующее определение: 

Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ~ P) : reflect P false.

Вы можете доказать утверждение 

Lemma even_reflect : forall n : nat, reflect (even n) (evenb n).

, а затем используйте его для одновременного перемещения между Опорой и логическим значением (которые содержат ту же информацию, т. Е. (Не) ровность n). Это также означает, что вы можете выполнять классические рассуждения по этому конкретному свойству без использования аксиомы classic.

Я предлагаю завершить упражнения в разделе «Отражение» в IndProp, а затем попробовать следующие упражнения. ( Редактировать: Я загрузил полный ответ здесь .) 

(* Since `evenb` has a nontrivial recursion structure, you need the following lemma: *)
Lemma nat_ind2 :
  forall P : nat -> Prop,
  P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n.
Proof. fix IH 5. intros. destruct n as [| [| ]]; auto.
  apply H1. apply IH; auto. Qed.

(* This is covered in an earlier chapter *)
Lemma negb_involutive : forall x : bool, negb (negb x) = x.
Proof. intros []; auto. Qed.

(* This one too. *)
Lemma evenb_S : forall n : nat, evenb (S n) = negb (evenb n).
Proof. induction n.
  - auto.
  - rewrite IHn. simpl. destruct (evenb n); auto. Qed.

(* Exercises. *)
Lemma evenb_even : forall n : nat, evenb n = true -> even n.
Proof. induction n using nat_ind2.
  (* Fill in here *) Admitted.

Lemma evenb_odd : forall n : nat, evenb n = false -> ~ (even n).
Proof. induction n using nat_ind2.
  (* Fill in here *) Admitted.

Lemma even_reflect : forall n : nat, reflect (even n) (evenb n).
Proof. (* Fill in here. Hint: You don't need induction. *) Admitted.

Lemma even_iff_evenb : forall n, even n <-> evenb n = true.
Proof. (* Fill in here. Hint: use `reflect_iff` from IndProp. *) Admitted.

Theorem reflect_iff_false : forall P b, reflect P b -> (~ P <-> b = false).
Proof. (* Fill in here. *) Admitted.

Lemma n_even_iff_evenb : forall n, ~ (even n) <-> evenb n = false.
Proof. (* Fill in here. *) Admitted.

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).
Proof. (* Fill in here.
  Hint: Now you can convert all the (non-)evenness properties to booleans,
  and then work with boolean logic! *) Admitted.
...