Як довести, що кругова опора нежитлова?

Розглянемо наступне індуктивне визначення "ElProp" у coq:

Inductive El : Set :=
  | R1 : El
  | R2 : El
  | R3 : El.

Inductive ElProp : El -> Prop :=
  | C1 : ElProp R1 -> ElProp R2
  | C2 : ElProp R2 -> ElProp R1
  | C3 : ElProp R3.

Спостерігаючи, що "(ElProp R1)" нежитловий, я заявляю наступну теорему:

Theorem excircular : ElProp R1 -> 1>2.

Я очікую, що теорема буде дійсною, подібно до наступної теореми:

Theorem exfalso : False -> 1>2.

Оскільки в "Невірних" немає мешканців, перевернути "помилкові" достатньо, щоб довести "ексфалсо". Але як мені довести "ексклюзивний"? Взагалі, як ми можемо довести, що кругові пропозиції нежилі?

1

2 Відповіді

You should use False instead of 1>2 in the conclusion of the theorem. Using indirect ways of denoting an impossible proposition is an unnecessary complication. False is the impossible proposition used in the standard library.

Щоб довести, що ElProp R1 нежитлова, ви повинні довести, що ElProp R2 нежитлова, і навпаки. Вам потрібна індукція за ElProp . Індуктивна властивість полягає в тому, що є мешканець ElProp R1 або ElProp R2 . (Ви також можете працювати над доказом того, що неможливо побудувати об'єкт з C1 або C2 , але це важче, оскільки має різні типи.)

~(ElProp R1 \/ ElProp R2)

Щоб виконати індукцію над ElProp , вам потрібно працювати в загальному жителе ElProp . Він має тип ElProp R для деякого R: El . Ми хочемо довести, що для такого мешканця R не може бути R1 або R2 . Ось спосіб заявити це:

Lemma excircular : forall R, (R = R1 \/ R = R2) -> ~ElProp R.

Now let's prove the lemma. First, expand the ~ abbreviation for fun A => A -> False.

unfold not; intros.

У нас є гіпотеза типу ElProp R , ідеально підходить для індукції.

induction H0.

По-перше, справа C1 ; це індуктивний випадок: властивість, над якою ми працюємо над роботами для ElProp R1 , оскільки вона працює для параметра (який має тип ElProp R2 ), об'єднуючи все це разом з деякою простою логікою першого порядку. У нас є гіпотеза типу R2 = R1 \/R2 = R2 ; як тільки ми застосуємо IHElProp , мета стає R1 = R1 \/R1 = R2 . Я залишу це вручну як заняття. Вбудована тактика tauto робить коротку роботу цього випадку, а також симетричну справу для C2 .

tauto.
tauto.

Для випадку C3 ми повинні показати, що гіпотези суперечливі. У нас є одна гіпотеза R3 = R1 \/R3 = R2 . Кожна гілка диз'юнкції є неможливою рівністю, оскільки конструктори R1 , R2 і R3 відрізняються.

destruct H. discriminate. discriminate.
Qed.

Ось коротший спосіб довести цю лемму. Вся інформація, яку нам дійсно потрібно надати, - це використання індукції належних гіпотез, Coq може з'ясувати інше з деякими загальними натяками.

Lemma excircular : forall R, (R = R1 \/ R = R2) -> ~ElProp R.
Proof.
  unfold not; intros.
  induction H0; firstorder discriminate.
Qed.

Тепер ми можемо довести бажану мету. Розгорніть абревіатуру ~ , застосуйте excircular і дозвольте Coq заповнити подробиці.

Theorem excircular1 : ~ElProp R1.
Proof.
  intro. eapply excircular; eauto.
Qed.
4
додано

Я думаю, вам потрібна індукція тут, щоб допомогти вам показати, що немає терміна, як C2 (C1 (C2 (C1 ... ). Я також думаю, що вам потрібно посилити гіпотезу індукції, тому що ви не просто потрібно знати, що ElProp C1 нежитлова, але теж ElProp C2 .

Я довів це, використовуючи допоміжну лемму

Theorem excircular_help: forall y, forall x: (ElProp y), y = R3.

Спробуйте це і дайте мені знати, якщо ви застрягли.

4
додано
Дякую. Етап індексації ElProp допомогла мені закінчити доказ.
додано Автор brijwhiz, джерело