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

Я пытаюсь доказать следующую лемму:

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» как истину и «даже 1» как ложь. Пробовал simpl, apply ev_0 in H. но выдают ошибку. Что делать?

Вы не показали нам определение even.

— 29.05.2019 00:25

@Perry Добавлено определение.

— 29.05.2019 06:24

coq logical-foundations

28.05.2019 23:59

Стоит ли изучать PHP в 2023-2024 годах?

Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...

Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией

В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.

Приемы CSS-макетирования - floats и Flexbox

Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...

Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest

В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...

Концепция локализации и ее применение в приложениях React ⚡️

Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...

Пользовательский скаляр GraphQL

Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...

1 082

Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

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

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 — это Prop, а не bool. Похоже, вы смешиваете типы True и False и логические значения true и false. Это совершенно разные вещи, и по логике Кока они не взаимозаменяемы. Короче говоря, even 0 не упрощается до true или True или чего-то еще. Это просто even 0. Если вы хотите показать, что even 0 является логически верным, вы должны построить значение этого типа.

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

(* 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.

29.05.2019 01:25