Coq: Доказательство conat является либо конечным, либо бесконечным - PullRequest
Новая
       18

Coq: Доказательство conat является либо конечным, либо бесконечным

2 голосов
/ 23 апреля 2019

У меня есть определение 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).

До сих пор я не мог доказать это, но я мог бы доказать другое утверждение, что, если 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).
Могу ли я доказать 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 * +, не работает, потому что требует транзитивности == с леммойаналогично 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 почти невозможно доказать.

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