Как заставить coq упростить выражения внутри гипотезы импликации - PullRequest
Новая
       14

Как заставить coq упростить выражения внутри гипотезы импликации

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.
  + unfold not. intros H. induction n as [|n' E' IHn].
    -
Qed.

Вот что я получил в конце: 

1 subgoal (ID 173)

H : even 0 -> False
============================
even 1

Я хочу, чтобы coq оценил "четные 0" в true и "четные 1" в false. Я пытался simpl, apply ev_0 in H., но они дают ошибку. Что делать?

1 Ответ

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

Ответ на заголовок 

simpl in H.

Реальный ответ

Приведенный выше код не будет работать.

Определение even изКнига логических основ: 

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

even 0 - это опора, а не бул.Похоже, вы смешиваете типы True и False и логические значения true и false.Это совершенно разные вещи, и они не взаимозаменяемы по логике Кока.Короче говоря, even 0 не упрощается до true или True или чего-либо еще.Это просто even 0. Если вы хотите показать, что even 0 логически верно, вы должны построить значение этого типа.

Я не помню, какая тактика доступна в этот момент вНЧ, но вот некоторые возможности: 

(* Since you know `ev_0` is a value of type `even 0`,
   construct `False` from H and destruct it.
   This is an example of forward proof. *)
set (contra := H ev_0). destruct contra.

(* ... or, in one step: *)
destruct (H ev_0).

(* We all know `even 1` is logically false,
   so change the goal to `False` and work from there.
   This is an example of backward proof. *)
exfalso. apply H. apply ev_0.
...