Блог

У меня есть определение conat , которое может представлять как конечные, так и бесконечные значения, преобразование из nat , определение бесконечности и отношение бисимуляции:

 CoInductive conat : Set := O' | S' (n : conat).

Fixpoint toCo (n : nat) : conat := match n with
  | O => O'
  | S n' => S' (toCo n') end.

CoFixpoint inf : conat := S' inf.

CoInductive bisim : conat -> conat -> Prop :=
  | OO : bisim O' O'
  | SS : forall n m : conat, bisim n m -> bisim (S' n) (S' m).

Notation "x == y" := (bisim x y) (at level 70).
  

Я хочу доказать, что conat является либо конечным, либо бесконечным (я не уверен на 100%, что это правильная формулировка):

 (* This is the goal *)
Theorem fin_or_inf : forall n : conat, (exists m : nat, toCo m == n) / (n == inf).
  

Я не мог доказать это до сих пор, но я мог бы доказать другое утверждение, что, если a conat не является конечным, оно бесконечно (опять же, не на 100% уверен в формулировке):

 (* I have a proof for this *)
Theorem not_fin_then_inf : forall n : conat, ~ (exists m : nat, toCo m == n) -> (n == inf).
  

Я понятия не имею, как перейти от not_fin_then_inf к fin_or_inf , хотя.

1. Правильно ли мое определение fin_or_inf ?

2. Могу ли я доказать fin_or_inf , используя not_fin_then_inf или не используя его?

Кроме того, я обнаружил, что преодоление разрыва между двумя теоремами предполагает разрешимость бисимуляции (или ее расширения). Я думаю, что теорему о разрешимости можно сформулировать как

 Lemma bisim_dec : forall n m : conat, n == m / ~ (n == m).
  

3. Могу ли я доказать bisim_dec или любое подобное утверждение о бисимуляции?

Редактировать

Первоначальная мотивация для доказательства «либо конечного, либо бесконечного» заключалась в том, чтобы доказать коммутативность и ассоциативность coplus :

 CoFixpoint coplus (n m : conat) := match n with
  | O' => m
  | S' n' => S' (coplus n' m)
end.
Notation "x ~  y" := (coplus x y) (at level 50, left associativity).

Theorem coplus_comm : forall n m, n ~  m == m ~  n.
Theorem coplus_assoc : forall n m p, n ~  m ~  p == n ~  (m ~  p).
  

Выполнение того же способа, что и nat ‘s , не работает, потому что для этого требуется транзитивность == с леммой, аналогичной plus_n_Sm , что делает вызов cofix незащищенным. В противном случае мне придется уничтожить оба n и m , и тогда я застряну у цели n ~ S' m == m ~ S' n .

Если я выберу альтернативное определение coplus :

 CoFixpoint coplus (n m : conat) := match n, m with
  | O', O' => O'
  | O', S' m' => S' m'
  | S' n', O' => S' n'
  | S' n', S' m' => S' (S' (coplus n' m'))
end.
  

Тогда coplus_comm это легко, но coplus_assoc вместо этого становится почти невозможным доказать.

4. Могу ли я действительно доказать coplus_comm с помощью первого определения coplus или coplus_assoc со вторым?