Добавление полного дизъюнктивной предположение в Coq

Question

В математике, мы часто поступают следующим образом: «Теперь давайте рассмотрим два случая, число k может быть even или odd Для even случае, можно сказать, exists k', 2k' = k ....»

Который расширяет общую идею рассуждения о целом наборе объектов путем разборки его на несколько дизъюнктных подмножеств, которые могут быть использованы для восстановления исходного набора.

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

Рассмотрим пример подражания для демонстрации:

forall n, Nat.Even n => P n.

Здесь мы можем естественно сделать inversion на Nat.Even n, чтобы получить n = 2*x (и автоматически-ложное предположение, что устранено n = 2*x + 1). Однако предположим, что мы имеем следующее:

forall n, P n

Как я могу заявить: "давайте рассмотрим even n с и odd n S". Должен ли я сначала показать, что мы разрешимы forall n : nat, even n \/ odd n? То есть, ввести новую (локальную или глобальную) лемму, в которой перечислены все необходимые подмножества? Каковы наилучшие методы?

Answer 1

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

ИМО, ключевым моментом является получение таких разрешительных гипотез «бесплатно». Например, вы можете реализовать odd : nat -> bool в качестве логической функции, как это делается в некоторых библиотеках, тогда вы получите бесплатное расщепление.

[править] Вы можете использовать некоторые немного более удобные методы для сопоставления с образцом, по enconding в соответствующих случаях, как inductives:

Require Import PeanoNat Nat Bool. 

CoInductive parity_spec (n : nat) : Type := 
| parity_spec_odd : odd n = true -> parity_spec n 
| parity_spec_even: even n = true -> parity_spec n 
. 

Lemma parityP n : parity_spec n. 
Proof. 
case (even n) eqn:H; [now right|left]. 
now rewrite <- Nat.negb_even, H. 
Qed. 

Lemma test n : even n = true \/ odd n = true. 
Proof. now case (parityP n); auto. Qed.